MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrptlem2 Structured version   Visualization version   GIF version

Theorem dchrptlem2 24971
Description: Lemma for dchrpt 24973. (Contributed by Mario Carneiro, 28-Apr-2016.)
Hypotheses
Ref Expression
dchrpt.g 𝐺 = (DChr‘𝑁)
dchrpt.z 𝑍 = (ℤ/nℤ‘𝑁)
dchrpt.d 𝐷 = (Base‘𝐺)
dchrpt.b 𝐵 = (Base‘𝑍)
dchrpt.1 1 = (1r𝑍)
dchrpt.n (𝜑𝑁 ∈ ℕ)
dchrpt.n1 (𝜑𝐴1 )
dchrpt.u 𝑈 = (Unit‘𝑍)
dchrpt.h 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)
dchrpt.m · = (.g𝐻)
dchrpt.s 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊𝑘))))
dchrpt.au (𝜑𝐴𝑈)
dchrpt.w (𝜑𝑊 ∈ Word 𝑈)
dchrpt.2 (𝜑𝐻dom DProd 𝑆)
dchrpt.3 (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
dchrpt.p 𝑃 = (𝐻dProj𝑆)
dchrpt.o 𝑂 = (od‘𝐻)
dchrpt.t 𝑇 = (-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))
dchrpt.i (𝜑𝐼 ∈ dom 𝑊)
dchrpt.4 (𝜑 → ((𝑃𝐼)‘𝐴) ≠ 1 )
dchrpt.5 𝑋 = (𝑢𝑈 ↦ (℩𝑚 ∈ ℤ (((𝑃𝐼)‘𝑢) = (𝑚 · (𝑊𝐼)) ∧ = (𝑇𝑚))))
Assertion
Ref Expression
dchrptlem2 (𝜑 → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
Distinct variable groups:   ,𝑘,𝑚,𝑛,𝑥, 1   𝑢,,𝐴,𝑘,𝑚,𝑛,𝑥   ,𝐼,𝑘,𝑚,𝑢   𝑥,𝐵   𝑥,𝐺   ,𝐻,𝑘,𝑚,𝑛,𝑢,𝑥   𝑥,𝑁   ,𝑊,𝑘,𝑚,𝑛,𝑢,𝑥   · ,,𝑘,𝑚,𝑛,𝑢,𝑥   𝑥,𝑋   𝑃,,𝑚,𝑢   𝑆,,𝑘,𝑚,𝑛,𝑢,𝑥   ,𝑍,𝑘,𝑚,𝑛,𝑢,𝑥   𝑥,𝐷   𝜑,,𝑘,𝑚,𝑛,𝑥   𝑇,,𝑚,𝑢   𝑈,,𝑚,𝑢,𝑥
Allowed substitution hints:   𝜑(𝑢)   𝐵(𝑢,,𝑘,𝑚,𝑛)   𝐷(𝑢,,𝑘,𝑚,𝑛)   𝑃(𝑥,𝑘,𝑛)   𝑇(𝑥,𝑘,𝑛)   𝑈(𝑘,𝑛)   1 (𝑢)   𝐺(𝑢,,𝑘,𝑚,𝑛)   𝐼(𝑥,𝑛)   𝑁(𝑢,,𝑘,𝑚,𝑛)   𝑂(𝑥,𝑢,,𝑘,𝑚,𝑛)   𝑋(𝑢,,𝑘,𝑚,𝑛)

Proof of Theorem dchrptlem2
Dummy variables 𝑎 𝑏 𝑣 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dchrpt.g . . 3 𝐺 = (DChr‘𝑁)
2 dchrpt.z . . 3 𝑍 = (ℤ/nℤ‘𝑁)
3 dchrpt.b . . 3 𝐵 = (Base‘𝑍)
4 dchrpt.u . . 3 𝑈 = (Unit‘𝑍)
5 dchrpt.n . . 3 (𝜑𝑁 ∈ ℕ)
6 dchrpt.d . . 3 𝐷 = (Base‘𝐺)
7 fveq2 6178 . . 3 (𝑣 = 𝑥 → (𝑋𝑣) = (𝑋𝑥))
8 fveq2 6178 . . 3 (𝑣 = 𝑦 → (𝑋𝑣) = (𝑋𝑦))
9 fveq2 6178 . . 3 (𝑣 = (𝑥(.r𝑍)𝑦) → (𝑋𝑣) = (𝑋‘(𝑥(.r𝑍)𝑦)))
10 fveq2 6178 . . 3 (𝑣 = (1r𝑍) → (𝑋𝑣) = (𝑋‘(1r𝑍)))
11 dchrpt.2 . . . . . . . . 9 (𝜑𝐻dom DProd 𝑆)
12 zex 11371 . . . . . . . . . . . . 13 ℤ ∈ V
1312mptex 6471 . . . . . . . . . . . 12 (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊𝑘))) ∈ V
1413rnex 7085 . . . . . . . . . . 11 ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊𝑘))) ∈ V
15 dchrpt.s . . . . . . . . . . 11 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊𝑘))))
1614, 15dmmpti 6010 . . . . . . . . . 10 dom 𝑆 = dom 𝑊
1716a1i 11 . . . . . . . . 9 (𝜑 → dom 𝑆 = dom 𝑊)
18 dchrpt.p . . . . . . . . 9 𝑃 = (𝐻dProj𝑆)
19 dchrpt.i . . . . . . . . 9 (𝜑𝐼 ∈ dom 𝑊)
2011, 17, 18, 19dpjf 18437 . . . . . . . 8 (𝜑 → (𝑃𝐼):(𝐻 DProd 𝑆)⟶(𝑆𝐼))
21 dchrpt.3 . . . . . . . . 9 (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
2221feq2d 6018 . . . . . . . 8 (𝜑 → ((𝑃𝐼):(𝐻 DProd 𝑆)⟶(𝑆𝐼) ↔ (𝑃𝐼):𝑈⟶(𝑆𝐼)))
2320, 22mpbid 222 . . . . . . 7 (𝜑 → (𝑃𝐼):𝑈⟶(𝑆𝐼))
2423ffvelrnda 6345 . . . . . 6 ((𝜑𝑣𝑈) → ((𝑃𝐼)‘𝑣) ∈ (𝑆𝐼))
2519adantr 481 . . . . . . 7 ((𝜑𝑣𝑈) → 𝐼 ∈ dom 𝑊)
26 oveq1 6642 . . . . . . . . . . 11 (𝑛 = 𝑎 → (𝑛 · (𝑊𝑘)) = (𝑎 · (𝑊𝑘)))
2726cbvmptv 4741 . . . . . . . . . 10 (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝑘)))
28 fveq2 6178 . . . . . . . . . . . 12 (𝑘 = 𝐼 → (𝑊𝑘) = (𝑊𝐼))
2928oveq2d 6651 . . . . . . . . . . 11 (𝑘 = 𝐼 → (𝑎 · (𝑊𝑘)) = (𝑎 · (𝑊𝐼)))
3029mpteq2dv 4736 . . . . . . . . . 10 (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼))))
3127, 30syl5eq 2666 . . . . . . . . 9 (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼))))
3231rneqd 5342 . . . . . . . 8 (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼))))
3332, 15, 14fvmpt3i 6274 . . . . . . 7 (𝐼 ∈ dom 𝑊 → (𝑆𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼))))
3425, 33syl 17 . . . . . 6 ((𝜑𝑣𝑈) → (𝑆𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼))))
3524, 34eleqtrd 2701 . . . . 5 ((𝜑𝑣𝑈) → ((𝑃𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼))))
36 eqid 2620 . . . . . 6 (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼)))
37 ovex 6663 . . . . . 6 (𝑎 · (𝑊𝐼)) ∈ V
3836, 37elrnmpti 5365 . . . . 5 (((𝑃𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊𝐼))) ↔ ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))
3935, 38sylib 208 . . . 4 ((𝜑𝑣𝑈) → ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))
40 dchrpt.1 . . . . . 6 1 = (1r𝑍)
41 dchrpt.n1 . . . . . 6 (𝜑𝐴1 )
42 dchrpt.h . . . . . 6 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)
43 dchrpt.m . . . . . 6 · = (.g𝐻)
44 dchrpt.au . . . . . 6 (𝜑𝐴𝑈)
45 dchrpt.w . . . . . 6 (𝜑𝑊 ∈ Word 𝑈)
46 dchrpt.o . . . . . 6 𝑂 = (od‘𝐻)
47 dchrpt.t . . . . . 6 𝑇 = (-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))
48 dchrpt.4 . . . . . 6 (𝜑 → ((𝑃𝐼)‘𝐴) ≠ 1 )
49 dchrpt.5 . . . . . 6 𝑋 = (𝑢𝑈 ↦ (℩𝑚 ∈ ℤ (((𝑃𝐼)‘𝑢) = (𝑚 · (𝑊𝐼)) ∧ = (𝑇𝑚))))
501, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49dchrptlem1 24970 . . . . 5 (((𝜑𝑣𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))) → (𝑋𝑣) = (𝑇𝑎))
51 neg1cn 11109 . . . . . . . . 9 -1 ∈ ℂ
52 2re 11075 . . . . . . . . . . 11 2 ∈ ℝ
535nnnn0d 11336 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ0)
542zncrng 19874 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ0𝑍 ∈ CRing)
55 crngring 18539 . . . . . . . . . . . . . 14 (𝑍 ∈ CRing → 𝑍 ∈ Ring)
5653, 54, 553syl 18 . . . . . . . . . . . . 13 (𝜑𝑍 ∈ Ring)
574, 42unitgrp 18648 . . . . . . . . . . . . 13 (𝑍 ∈ Ring → 𝐻 ∈ Grp)
5856, 57syl 17 . . . . . . . . . . . 12 (𝜑𝐻 ∈ Grp)
592, 3znfi 19889 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
605, 59syl 17 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ Fin)
613, 4unitss 18641 . . . . . . . . . . . . 13 𝑈𝐵
62 ssfi 8165 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ 𝑈𝐵) → 𝑈 ∈ Fin)
6360, 61, 62sylancl 693 . . . . . . . . . . . 12 (𝜑𝑈 ∈ Fin)
64 wrdf 13293 . . . . . . . . . . . . . 14 (𝑊 ∈ Word 𝑈𝑊:(0..^(#‘𝑊))⟶𝑈)
6545, 64syl 17 . . . . . . . . . . . . 13 (𝜑𝑊:(0..^(#‘𝑊))⟶𝑈)
66 fdm 6038 . . . . . . . . . . . . . . 15 (𝑊:(0..^(#‘𝑊))⟶𝑈 → dom 𝑊 = (0..^(#‘𝑊)))
6765, 66syl 17 . . . . . . . . . . . . . 14 (𝜑 → dom 𝑊 = (0..^(#‘𝑊)))
6819, 67eleqtrd 2701 . . . . . . . . . . . . 13 (𝜑𝐼 ∈ (0..^(#‘𝑊)))
6965, 68ffvelrnd 6346 . . . . . . . . . . . 12 (𝜑 → (𝑊𝐼) ∈ 𝑈)
704, 42unitgrpbas 18647 . . . . . . . . . . . . 13 𝑈 = (Base‘𝐻)
7170, 46odcl2 17963 . . . . . . . . . . . 12 ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊𝐼) ∈ 𝑈) → (𝑂‘(𝑊𝐼)) ∈ ℕ)
7258, 63, 69, 71syl3anc 1324 . . . . . . . . . . 11 (𝜑 → (𝑂‘(𝑊𝐼)) ∈ ℕ)
73 nndivre 11041 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ (𝑂‘(𝑊𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊𝐼))) ∈ ℝ)
7452, 72, 73sylancr 694 . . . . . . . . . 10 (𝜑 → (2 / (𝑂‘(𝑊𝐼))) ∈ ℝ)
7574recnd 10053 . . . . . . . . 9 (𝜑 → (2 / (𝑂‘(𝑊𝐼))) ∈ ℂ)
76 cxpcl 24401 . . . . . . . . 9 ((-1 ∈ ℂ ∧ (2 / (𝑂‘(𝑊𝐼))) ∈ ℂ) → (-1↑𝑐(2 / (𝑂‘(𝑊𝐼)))) ∈ ℂ)
7751, 75, 76sylancr 694 . . . . . . . 8 (𝜑 → (-1↑𝑐(2 / (𝑂‘(𝑊𝐼)))) ∈ ℂ)
7847, 77syl5eqel 2703 . . . . . . 7 (𝜑𝑇 ∈ ℂ)
7978ad2antrr 761 . . . . . 6 (((𝜑𝑣𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))) → 𝑇 ∈ ℂ)
8051a1i 11 . . . . . . . . 9 (𝜑 → -1 ∈ ℂ)
81 neg1ne0 11111 . . . . . . . . . 10 -1 ≠ 0
8281a1i 11 . . . . . . . . 9 (𝜑 → -1 ≠ 0)
8380, 82, 75cxpne0d 24440 . . . . . . . 8 (𝜑 → (-1↑𝑐(2 / (𝑂‘(𝑊𝐼)))) ≠ 0)
8447neeq1i 2855 . . . . . . . 8 (𝑇 ≠ 0 ↔ (-1↑𝑐(2 / (𝑂‘(𝑊𝐼)))) ≠ 0)
8583, 84sylibr 224 . . . . . . 7 (𝜑𝑇 ≠ 0)
8685ad2antrr 761 . . . . . 6 (((𝜑𝑣𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))) → 𝑇 ≠ 0)
87 simprl 793 . . . . . 6 (((𝜑𝑣𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))) → 𝑎 ∈ ℤ)
8879, 86, 87expclzd 12996 . . . . 5 (((𝜑𝑣𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))) → (𝑇𝑎) ∈ ℂ)
8950, 88eqeltrd 2699 . . . 4 (((𝜑𝑣𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))) → (𝑋𝑣) ∈ ℂ)
9039, 89rexlimddv 3031 . . 3 ((𝜑𝑣𝑈) → (𝑋𝑣) ∈ ℂ)
91 simprl 793 . . . . 5 ((𝜑 ∧ (𝑥𝑈𝑦𝑈)) → 𝑥𝑈)
9239ralrimiva 2963 . . . . . 6 (𝜑 → ∀𝑣𝑈𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))
9392adantr 481 . . . . 5 ((𝜑 ∧ (𝑥𝑈𝑦𝑈)) → ∀𝑣𝑈𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)))
94 fveq2 6178 . . . . . . . 8 (𝑣 = 𝑥 → ((𝑃𝐼)‘𝑣) = ((𝑃𝐼)‘𝑥))
9594eqeq1d 2622 . . . . . . 7 (𝑣 = 𝑥 → (((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) ↔ ((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼))))
9695rexbidv 3048 . . . . . 6 (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼))))
9796rspcv 3300 . . . . 5 (𝑥𝑈 → (∀𝑣𝑈𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) → ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼))))
9891, 93, 97sylc 65 . . . 4 ((𝜑 ∧ (𝑥𝑈𝑦𝑈)) → ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)))
99 simprr 795 . . . . 5 ((𝜑 ∧ (𝑥𝑈𝑦𝑈)) → 𝑦𝑈)
100 fveq2 6178 . . . . . . . . 9 (𝑣 = 𝑦 → ((𝑃𝐼)‘𝑣) = ((𝑃𝐼)‘𝑦))
101100eqeq1d 2622 . . . . . . . 8 (𝑣 = 𝑦 → (((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) ↔ ((𝑃𝐼)‘𝑦) = (𝑎 · (𝑊𝐼))))
102101rexbidv 3048 . . . . . . 7 (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑦) = (𝑎 · (𝑊𝐼))))
103 oveq1 6642 . . . . . . . . 9 (𝑎 = 𝑏 → (𝑎 · (𝑊𝐼)) = (𝑏 · (𝑊𝐼)))
104103eqeq2d 2630 . . . . . . . 8 (𝑎 = 𝑏 → (((𝑃𝐼)‘𝑦) = (𝑎 · (𝑊𝐼)) ↔ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))
105104cbvrexv 3167 . . . . . . 7 (∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑦) = (𝑎 · (𝑊𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼)))
106102, 105syl6bb 276 . . . . . 6 (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))
107106rspcv 3300 . . . . 5 (𝑦𝑈 → (∀𝑣𝑈𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) → ∃𝑏 ∈ ℤ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))
10899, 93, 107sylc 65 . . . 4 ((𝜑 ∧ (𝑥𝑈𝑦𝑈)) → ∃𝑏 ∈ ℤ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼)))
109 reeanv 3102 . . . . 5 (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))
11078ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝑇 ∈ ℂ)
11185ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝑇 ≠ 0)
112 simprll 801 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝑎 ∈ ℤ)
113 simprlr 802 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝑏 ∈ ℤ)
114 expaddz 12887 . . . . . . . . 9 (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇𝑎) · (𝑇𝑏)))
115110, 111, 112, 113, 114syl22anc 1325 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇𝑎) · (𝑇𝑏)))
116 simpll 789 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝜑)
11756ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝑍 ∈ Ring)
11891adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝑥𝑈)
11999adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝑦𝑈)
120 eqid 2620 . . . . . . . . . . 11 (.r𝑍) = (.r𝑍)
1214, 120unitmulcl 18645 . . . . . . . . . 10 ((𝑍 ∈ Ring ∧ 𝑥𝑈𝑦𝑈) → (𝑥(.r𝑍)𝑦) ∈ 𝑈)
122117, 118, 119, 121syl3anc 1324 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑥(.r𝑍)𝑦) ∈ 𝑈)
123112, 113zaddcld 11471 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑎 + 𝑏) ∈ ℤ)
124 simprrl 803 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → ((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)))
125 simprrr 804 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼)))
126124, 125oveq12d 6653 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (((𝑃𝐼)‘𝑥)(.r𝑍)((𝑃𝐼)‘𝑦)) = ((𝑎 · (𝑊𝐼))(.r𝑍)(𝑏 · (𝑊𝐼))))
12711, 17, 18, 19dpjghm 18443 . . . . . . . . . . . . 13 (𝜑 → (𝑃𝐼) ∈ ((𝐻s (𝐻 DProd 𝑆)) GrpHom 𝐻))
12821oveq2d 6651 . . . . . . . . . . . . . . 15 (𝜑 → (𝐻s (𝐻 DProd 𝑆)) = (𝐻s 𝑈))
129 ovex 6663 . . . . . . . . . . . . . . . . 17 ((mulGrp‘𝑍) ↾s 𝑈) ∈ V
13042, 129eqeltri 2695 . . . . . . . . . . . . . . . 16 𝐻 ∈ V
13170ressid 15916 . . . . . . . . . . . . . . . 16 (𝐻 ∈ V → (𝐻s 𝑈) = 𝐻)
132130, 131ax-mp 5 . . . . . . . . . . . . . . 15 (𝐻s 𝑈) = 𝐻
133128, 132syl6eq 2670 . . . . . . . . . . . . . 14 (𝜑 → (𝐻s (𝐻 DProd 𝑆)) = 𝐻)
134133oveq1d 6650 . . . . . . . . . . . . 13 (𝜑 → ((𝐻s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻))
135127, 134eleqtrd 2701 . . . . . . . . . . . 12 (𝜑 → (𝑃𝐼) ∈ (𝐻 GrpHom 𝐻))
136135ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑃𝐼) ∈ (𝐻 GrpHom 𝐻))
137 fvex 6188 . . . . . . . . . . . . . 14 (Unit‘𝑍) ∈ V
1384, 137eqeltri 2695 . . . . . . . . . . . . 13 𝑈 ∈ V
139 eqid 2620 . . . . . . . . . . . . . . 15 (mulGrp‘𝑍) = (mulGrp‘𝑍)
140139, 120mgpplusg 18474 . . . . . . . . . . . . . 14 (.r𝑍) = (+g‘(mulGrp‘𝑍))
14142, 140ressplusg 15974 . . . . . . . . . . . . 13 (𝑈 ∈ V → (.r𝑍) = (+g𝐻))
142138, 141ax-mp 5 . . . . . . . . . . . 12 (.r𝑍) = (+g𝐻)
14370, 142, 142ghmlin 17646 . . . . . . . . . . 11 (((𝑃𝐼) ∈ (𝐻 GrpHom 𝐻) ∧ 𝑥𝑈𝑦𝑈) → ((𝑃𝐼)‘(𝑥(.r𝑍)𝑦)) = (((𝑃𝐼)‘𝑥)(.r𝑍)((𝑃𝐼)‘𝑦)))
144136, 118, 119, 143syl3anc 1324 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → ((𝑃𝐼)‘(𝑥(.r𝑍)𝑦)) = (((𝑃𝐼)‘𝑥)(.r𝑍)((𝑃𝐼)‘𝑦)))
14558ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → 𝐻 ∈ Grp)
14669ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑊𝐼) ∈ 𝑈)
14770, 43, 142mulgdir 17554 . . . . . . . . . . 11 ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊𝐼)) = ((𝑎 · (𝑊𝐼))(.r𝑍)(𝑏 · (𝑊𝐼))))
148145, 112, 113, 146, 147syl13anc 1326 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → ((𝑎 + 𝑏) · (𝑊𝐼)) = ((𝑎 · (𝑊𝐼))(.r𝑍)(𝑏 · (𝑊𝐼))))
149126, 144, 1483eqtr4d 2664 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → ((𝑃𝐼)‘(𝑥(.r𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊𝐼)))
1501, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49dchrptlem1 24970 . . . . . . . . 9 (((𝜑 ∧ (𝑥(.r𝑍)𝑦) ∈ 𝑈) ∧ ((𝑎 + 𝑏) ∈ ℤ ∧ ((𝑃𝐼)‘(𝑥(.r𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊𝐼)))) → (𝑋‘(𝑥(.r𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏)))
151116, 122, 123, 149, 150syl22anc 1325 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑋‘(𝑥(.r𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏)))
1521, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49dchrptlem1 24970 . . . . . . . . . 10 (((𝜑𝑥𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)))) → (𝑋𝑥) = (𝑇𝑎))
153116, 118, 112, 124, 152syl22anc 1325 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑋𝑥) = (𝑇𝑎))
1541, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49dchrptlem1 24970 . . . . . . . . . 10 (((𝜑𝑦𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼)))) → (𝑋𝑦) = (𝑇𝑏))
155116, 119, 113, 125, 154syl22anc 1325 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑋𝑦) = (𝑇𝑏))
156153, 155oveq12d 6653 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → ((𝑋𝑥) · (𝑋𝑦)) = ((𝑇𝑎) · (𝑇𝑏)))
157115, 151, 1563eqtr4d 2664 . . . . . . 7 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))))) → (𝑋‘(𝑥(.r𝑍)𝑦)) = ((𝑋𝑥) · (𝑋𝑦)))
158157expr 642 . . . . . 6 (((𝜑 ∧ (𝑥𝑈𝑦𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))) → (𝑋‘(𝑥(.r𝑍)𝑦)) = ((𝑋𝑥) · (𝑋𝑦))))
159158rexlimdvva 3034 . . . . 5 ((𝜑 ∧ (𝑥𝑈𝑦𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))) → (𝑋‘(𝑥(.r𝑍)𝑦)) = ((𝑋𝑥) · (𝑋𝑦))))
160109, 159syl5bir 233 . . . 4 ((𝜑 ∧ (𝑥𝑈𝑦𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑥) = (𝑎 · (𝑊𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃𝐼)‘𝑦) = (𝑏 · (𝑊𝐼))) → (𝑋‘(𝑥(.r𝑍)𝑦)) = ((𝑋𝑥) · (𝑋𝑦))))
16198, 108, 160mp2and 714 . . 3 ((𝜑 ∧ (𝑥𝑈𝑦𝑈)) → (𝑋‘(𝑥(.r𝑍)𝑦)) = ((𝑋𝑥) · (𝑋𝑦)))
162 id 22 . . . . 5 (𝜑𝜑)
163 eqid 2620 . . . . . . 7 (1r𝑍) = (1r𝑍)
1644, 1631unit 18639 . . . . . 6 (𝑍 ∈ Ring → (1r𝑍) ∈ 𝑈)
16556, 164syl 17 . . . . 5 (𝜑 → (1r𝑍) ∈ 𝑈)
166 0zd 11374 . . . . 5 (𝜑 → 0 ∈ ℤ)
167 eqid 2620 . . . . . . . 8 (0g𝐻) = (0g𝐻)
168167, 167ghmid 17647 . . . . . . 7 ((𝑃𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃𝐼)‘(0g𝐻)) = (0g𝐻))
169135, 168syl 17 . . . . . 6 (𝜑 → ((𝑃𝐼)‘(0g𝐻)) = (0g𝐻))
1704, 42, 163unitgrpid 18650 . . . . . . . 8 (𝑍 ∈ Ring → (1r𝑍) = (0g𝐻))
17156, 170syl 17 . . . . . . 7 (𝜑 → (1r𝑍) = (0g𝐻))
172171fveq2d 6182 . . . . . 6 (𝜑 → ((𝑃𝐼)‘(1r𝑍)) = ((𝑃𝐼)‘(0g𝐻)))
17370, 167, 43mulg0 17527 . . . . . . 7 ((𝑊𝐼) ∈ 𝑈 → (0 · (𝑊𝐼)) = (0g𝐻))
17469, 173syl 17 . . . . . 6 (𝜑 → (0 · (𝑊𝐼)) = (0g𝐻))
175169, 172, 1743eqtr4d 2664 . . . . 5 (𝜑 → ((𝑃𝐼)‘(1r𝑍)) = (0 · (𝑊𝐼)))
1761, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49dchrptlem1 24970 . . . . 5 (((𝜑 ∧ (1r𝑍) ∈ 𝑈) ∧ (0 ∈ ℤ ∧ ((𝑃𝐼)‘(1r𝑍)) = (0 · (𝑊𝐼)))) → (𝑋‘(1r𝑍)) = (𝑇↑0))
177162, 165, 166, 175, 176syl22anc 1325 . . . 4 (𝜑 → (𝑋‘(1r𝑍)) = (𝑇↑0))
17878exp0d 12985 . . . 4 (𝜑 → (𝑇↑0) = 1)
179177, 178eqtrd 2654 . . 3 (𝜑 → (𝑋‘(1r𝑍)) = 1)
1801, 2, 3, 4, 5, 6, 7, 8, 9, 10, 90, 161, 179dchrelbasd 24945 . 2 (𝜑 → (𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0)) ∈ 𝐷)
18161, 44sseldi 3593 . . . . 5 (𝜑𝐴𝐵)
182 eleq1 2687 . . . . . . 7 (𝑣 = 𝐴 → (𝑣𝑈𝐴𝑈))
183 fveq2 6178 . . . . . . 7 (𝑣 = 𝐴 → (𝑋𝑣) = (𝑋𝐴))
184182, 183ifbieq1d 4100 . . . . . 6 (𝑣 = 𝐴 → if(𝑣𝑈, (𝑋𝑣), 0) = if(𝐴𝑈, (𝑋𝐴), 0))
185 eqid 2620 . . . . . 6 (𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0)) = (𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0))
186 fvex 6188 . . . . . . 7 (𝑋𝑣) ∈ V
187 c0ex 10019 . . . . . . 7 0 ∈ V
188186, 187ifex 4147 . . . . . 6 if(𝑣𝑈, (𝑋𝑣), 0) ∈ V
189184, 185, 188fvmpt3i 6274 . . . . 5 (𝐴𝐵 → ((𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0))‘𝐴) = if(𝐴𝑈, (𝑋𝐴), 0))
190181, 189syl 17 . . . 4 (𝜑 → ((𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0))‘𝐴) = if(𝐴𝑈, (𝑋𝐴), 0))
19144iftrued 4085 . . . 4 (𝜑 → if(𝐴𝑈, (𝑋𝐴), 0) = (𝑋𝐴))
192190, 191eqtrd 2654 . . 3 (𝜑 → ((𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0))‘𝐴) = (𝑋𝐴))
193 fveq2 6178 . . . . . . . 8 (𝑣 = 𝐴 → ((𝑃𝐼)‘𝑣) = ((𝑃𝐼)‘𝐴))
194193eqeq1d 2622 . . . . . . 7 (𝑣 = 𝐴 → (((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) ↔ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼))))
195194rexbidv 3048 . . . . . 6 (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼))))
196195rspcv 3300 . . . . 5 (𝐴𝑈 → (∀𝑣𝑈𝑎 ∈ ℤ ((𝑃𝐼)‘𝑣) = (𝑎 · (𝑊𝐼)) → ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼))))
19744, 92, 196sylc 65 . . . 4 (𝜑 → ∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))
1981, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49dchrptlem1 24970 . . . . . . . 8 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (𝑋𝐴) = (𝑇𝑎))
19947oveq1i 6645 . . . . . . . 8 (𝑇𝑎) = ((-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))↑𝑎)
200198, 199syl6eq 2670 . . . . . . 7 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (𝑋𝐴) = ((-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))↑𝑎))
20148ad2antrr 761 . . . . . . . 8 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → ((𝑃𝐼)‘𝐴) ≠ 1 )
20258ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → 𝐻 ∈ Grp)
20369ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (𝑊𝐼) ∈ 𝑈)
204 simprl 793 . . . . . . . . . . 11 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → 𝑎 ∈ ℤ)
20570, 46, 43, 167oddvds 17947 . . . . . . . . . . 11 ((𝐻 ∈ Grp ∧ (𝑊𝐼) ∈ 𝑈𝑎 ∈ ℤ) → ((𝑂‘(𝑊𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊𝐼)) = (0g𝐻)))
206202, 203, 204, 205syl3anc 1324 . . . . . . . . . 10 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → ((𝑂‘(𝑊𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊𝐼)) = (0g𝐻)))
20772ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (𝑂‘(𝑊𝐼)) ∈ ℕ)
208 root1eq1 24477 . . . . . . . . . . 11 (((𝑂‘(𝑊𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) → (((-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊𝐼)) ∥ 𝑎))
209207, 204, 208syl2anc 692 . . . . . . . . . 10 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (((-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊𝐼)) ∥ 𝑎))
210 simprr 795 . . . . . . . . . . 11 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))
21140, 171syl5eq 2666 . . . . . . . . . . . 12 (𝜑1 = (0g𝐻))
212211ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → 1 = (0g𝐻))
213210, 212eqeq12d 2635 . . . . . . . . . 10 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (((𝑃𝐼)‘𝐴) = 1 ↔ (𝑎 · (𝑊𝐼)) = (0g𝐻)))
214206, 209, 2133bitr4d 300 . . . . . . . . 9 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (((-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))↑𝑎) = 1 ↔ ((𝑃𝐼)‘𝐴) = 1 ))
215214necon3bid 2835 . . . . . . . 8 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (((-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃𝐼)‘𝐴) ≠ 1 ))
216201, 215mpbird 247 . . . . . . 7 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → ((-1↑𝑐(2 / (𝑂‘(𝑊𝐼))))↑𝑎) ≠ 1)
217200, 216eqnetrd 2858 . . . . . 6 (((𝜑𝐴𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)))) → (𝑋𝐴) ≠ 1)
218217rexlimdvaa 3028 . . . . 5 ((𝜑𝐴𝑈) → (∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)) → (𝑋𝐴) ≠ 1))
21944, 218mpdan 701 . . . 4 (𝜑 → (∃𝑎 ∈ ℤ ((𝑃𝐼)‘𝐴) = (𝑎 · (𝑊𝐼)) → (𝑋𝐴) ≠ 1))
220197, 219mpd 15 . . 3 (𝜑 → (𝑋𝐴) ≠ 1)
221192, 220eqnetrd 2858 . 2 (𝜑 → ((𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0))‘𝐴) ≠ 1)
222 fveq1 6177 . . . 4 (𝑥 = (𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0)) → (𝑥𝐴) = ((𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0))‘𝐴))
223222neeq1d 2850 . . 3 (𝑥 = (𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0)) → ((𝑥𝐴) ≠ 1 ↔ ((𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0))‘𝐴) ≠ 1))
224223rspcev 3304 . 2 (((𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0)) ∈ 𝐷 ∧ ((𝑣𝐵 ↦ if(𝑣𝑈, (𝑋𝑣), 0))‘𝐴) ≠ 1) → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
225180, 221, 224syl2anc 692 1 (𝜑 → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  Vcvv 3195  wss 3567  ifcif 4077   class class class wbr 4644  cmpt 4720  dom cdm 5104  ran crn 5105  cio 5837  wf 5872  cfv 5876  (class class class)co 6635  Fincfn 7940  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926  -cneg 10252   / cdiv 10669  cn 11005  2c2 11055  0cn0 11277  cz 11362  ..^cfzo 12449  cexp 12843  #chash 13100  Word cword 13274  cdvds 14964  Basecbs 15838  s cress 15839  +gcplusg 15922  .rcmulr 15923  0gc0g 16081  Grpcgrp 17403  .gcmg 17521   GrpHom cghm 17638  odcod 17925   DProd cdprd 18373  dProjcdpj 18374  mulGrpcmgp 18470  1rcur 18482  Ringcrg 18528  CRingccrg 18529  Unitcui 18620  ℤ/nczn 19832  𝑐ccxp 24283  DChrcdchr 24938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-addf 10000  ax-mulf 10001
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-tpos 7337  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-omul 7550  df-er 7727  df-ec 7729  df-qs 7733  df-map 7844  df-pm 7845  df-ixp 7894  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-fi 8302  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-acn 8753  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ioo 12164  df-ioc 12165  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-mod 12652  df-seq 12785  df-exp 12844  df-fac 13044  df-bc 13073  df-hash 13101  df-word 13282  df-shft 13788  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-limsup 14183  df-clim 14200  df-rlim 14201  df-sum 14398  df-ef 14779  df-sin 14781  df-cos 14782  df-pi 14784  df-dvds 14965  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-sets 15845  df-ress 15846  df-plusg 15935  df-mulr 15936  df-starv 15937  df-sca 15938  df-vsca 15939  df-ip 15940  df-tset 15941  df-ple 15942  df-ds 15945  df-unif 15946  df-hom 15947  df-cco 15948  df-rest 16064  df-topn 16065  df-0g 16083  df-gsum 16084  df-topgen 16085  df-pt 16086  df-prds 16089  df-xrs 16143  df-qtop 16148  df-imas 16149  df-qus 16150  df-xps 16151  df-mre 16227  df-mrc 16228  df-acs 16230  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-mhm 17316  df-submnd 17317  df-grp 17406  df-minusg 17407  df-sbg 17408  df-mulg 17522  df-subg 17572  df-nsg 17573  df-eqg 17574  df-ghm 17639  df-gim 17682  df-cntz 17731  df-oppg 17757  df-od 17929  df-lsm 18032  df-pj1 18033  df-cmn 18176  df-abl 18177  df-dprd 18375  df-dpj 18376  df-mgp 18471  df-ur 18483  df-ring 18530  df-cring 18531  df-oppr 18604  df-dvdsr 18622  df-unit 18623  df-rnghom 18696  df-subrg 18759  df-lmod 18846  df-lss 18914  df-lsp 18953  df-sra 19153  df-rgmod 19154  df-lidl 19155  df-rsp 19156  df-2idl 19213  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-fbas 19724  df-fg 19725  df-cnfld 19728  df-zring 19800  df-zrh 19833  df-zn 19836  df-top 20680  df-topon 20697  df-topsp 20718  df-bases 20731  df-cld 20804  df-ntr 20805  df-cls 20806  df-nei 20883  df-lp 20921  df-perf 20922  df-cn 21012  df-cnp 21013  df-haus 21100  df-tx 21346  df-hmeo 21539  df-fil 21631  df-fm 21723  df-flim 21724  df-flf 21725  df-xms 22106  df-ms 22107  df-tms 22108  df-cncf 22662  df-limc 23611  df-dv 23612  df-log 24284  df-cxp 24285  df-dchr 24939
This theorem is referenced by:  dchrptlem3  24972
  Copyright terms: Public domain W3C validator