| Step | Hyp | Ref | 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 6905 | . . 3
⊢ (𝑣 = 𝑥 → (𝑋‘𝑣) = (𝑋‘𝑥)) | 
| 8 |  | fveq2 6905 | . . 3
⊢ (𝑣 = 𝑦 → (𝑋‘𝑣) = (𝑋‘𝑦)) | 
| 9 |  | fveq2 6905 | . . 3
⊢ (𝑣 = (𝑥(.r‘𝑍)𝑦) → (𝑋‘𝑣) = (𝑋‘(𝑥(.r‘𝑍)𝑦))) | 
| 10 |  | fveq2 6905 | . . 3
⊢ (𝑣 = (1r‘𝑍) → (𝑋‘𝑣) = (𝑋‘(1r‘𝑍))) | 
| 11 |  | dchrpt.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐻dom DProd 𝑆) | 
| 12 |  | zex 12624 | . . . . . . . . . . . . 13
⊢ ℤ
∈ V | 
| 13 | 12 | mptex 7244 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V | 
| 14 | 13 | rnex 7933 | . . . . . . . . . . 11
⊢ ran
(𝑛 ∈ ℤ ↦
(𝑛 · (𝑊‘𝑘))) ∈ V | 
| 15 |  | dchrpt.s | . . . . . . . . . . 11
⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘)))) | 
| 16 | 14, 15 | dmmpti 6711 | . . . . . . . . . 10
⊢ dom 𝑆 = dom 𝑊 | 
| 17 | 16 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → dom 𝑆 = dom 𝑊) | 
| 18 |  | dchrpt.p | . . . . . . . . 9
⊢ 𝑃 = (𝐻dProj𝑆) | 
| 19 |  | dchrpt.i | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ dom 𝑊) | 
| 20 | 11, 17, 18, 19 | dpjf 20078 | . . . . . . . 8
⊢ (𝜑 → (𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼)) | 
| 21 |  | dchrpt.3 | . . . . . . . . 9
⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈) | 
| 22 | 21 | feq2d 6721 | . . . . . . . 8
⊢ (𝜑 → ((𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼) ↔ (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼))) | 
| 23 | 20, 22 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼)) | 
| 24 | 23 | ffvelcdmda 7103 | . . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ (𝑆‘𝐼)) | 
| 25 | 19 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝐼 ∈ dom 𝑊) | 
| 26 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑎 → (𝑛 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝑘))) | 
| 27 | 26 | cbvmptv 5254 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) | 
| 28 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐼 → (𝑊‘𝑘) = (𝑊‘𝐼)) | 
| 29 | 28 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐼 → (𝑎 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝐼))) | 
| 30 | 29 | mpteq2dv 5243 | . . . . . . . . . 10
⊢ (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) | 
| 31 | 27, 30 | eqtrid 2788 | . . . . . . . . 9
⊢ (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) | 
| 32 | 31 | rneqd 5948 | . . . . . . . 8
⊢ (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) | 
| 33 | 32, 15, 14 | fvmpt3i 7020 | . . . . . . 7
⊢ (𝐼 ∈ dom 𝑊 → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) | 
| 34 | 25, 33 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) | 
| 35 | 24, 34 | eleqtrd 2842 | . . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) | 
| 36 |  | eqid 2736 | . . . . . 6
⊢ (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) | 
| 37 |  | ovex 7465 | . . . . . 6
⊢ (𝑎 · (𝑊‘𝐼)) ∈ V | 
| 38 | 36, 37 | elrnmpti 5972 | . . . . 5
⊢ (((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) | 
| 39 | 35, 38 | sylib 218 | . . . 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
⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) | 
| 50 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 27309 | . . . . 5
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) = (𝑇↑𝑎)) | 
| 51 |  | neg1cn 12381 | . . . . . . . . 9
⊢ -1 ∈
ℂ | 
| 52 |  | 2re 12341 | . . . . . . . . . . 11
⊢ 2 ∈
ℝ | 
| 53 | 5 | nnnn0d 12589 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 54 | 2 | zncrng 21564 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) | 
| 55 |  | crngring 20243 | . . . . . . . . . . . . . 14
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) | 
| 56 | 53, 54, 55 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ Ring) | 
| 57 | 4, 42 | unitgrp 20384 | . . . . . . . . . . . . 13
⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp) | 
| 58 | 56, 57 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ Grp) | 
| 59 | 2, 3 | znfi 21579 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) | 
| 60 | 5, 59 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ Fin) | 
| 61 | 3, 4 | unitss 20377 | . . . . . . . . . . . . 13
⊢ 𝑈 ⊆ 𝐵 | 
| 62 |  | ssfi 9214 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin) | 
| 63 | 60, 61, 62 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ Fin) | 
| 64 |  | wrdf 14558 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(♯‘𝑊))⟶𝑈) | 
| 65 | 45, 64 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑈) | 
| 66 | 65 | fdmd 6745 | . . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 67 | 19, 66 | eleqtrd 2842 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊))) | 
| 68 | 65, 67 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈) | 
| 69 | 4, 42 | unitgrpbas 20383 | . . . . . . . . . . . . 13
⊢ 𝑈 = (Base‘𝐻) | 
| 70 | 69, 46 | odcl2 19584 | . . . . . . . . . . . 12
⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) | 
| 71 | 58, 63, 68, 70 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) | 
| 72 |  | nndivre 12308 | . . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ) | 
| 73 | 52, 71, 72 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ) | 
| 74 | 73 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) | 
| 75 |  | cxpcl 26717 | . . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ) | 
| 76 | 51, 74, 75 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ) | 
| 77 | 47, 76 | eqeltrid 2844 | . . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℂ) | 
| 78 | 77 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ∈ ℂ) | 
| 79 | 51 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℂ) | 
| 80 |  | neg1ne0 12383 | . . . . . . . . . 10
⊢ -1 ≠
0 | 
| 81 | 80 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → -1 ≠
0) | 
| 82 | 79, 81, 74 | cxpne0d 26756 | . . . . . . . 8
⊢ (𝜑 →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0) | 
| 83 | 47 | neeq1i 3004 | . . . . . . . 8
⊢ (𝑇 ≠ 0 ↔
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0) | 
| 84 | 82, 83 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → 𝑇 ≠ 0) | 
| 85 | 84 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ≠ 0) | 
| 86 |  | simprl 770 | . . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ) | 
| 87 | 78, 85, 86 | expclzd 14192 | . . . . 5
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑇↑𝑎) ∈ ℂ) | 
| 88 | 50, 87 | eqeltrd 2840 | . . . 4
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) ∈ ℂ) | 
| 89 | 39, 88 | rexlimddv 3160 | . . 3
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑋‘𝑣) ∈ ℂ) | 
| 90 |  | fveqeq2 6914 | . . . . . 6
⊢ (𝑣 = 𝑥 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) | 
| 91 | 90 | rexbidv 3178 | . . . . 5
⊢ (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) | 
| 92 | 39 | ralrimiva 3145 | . . . . . 6
⊢ (𝜑 → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) | 
| 93 | 92 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) | 
| 94 |  | simprl 770 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈) | 
| 95 | 91, 93, 94 | rspcdva 3622 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))) | 
| 96 |  | fveqeq2 6914 | . . . . . . 7
⊢ (𝑣 = 𝑦 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)))) | 
| 97 | 96 | rexbidv 3178 | . . . . . 6
⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)))) | 
| 98 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝑎 · (𝑊‘𝐼)) = (𝑏 · (𝑊‘𝐼))) | 
| 99 | 98 | eqeq2d 2747 | . . . . . . 7
⊢ (𝑎 = 𝑏 → (((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) | 
| 100 | 99 | cbvrexvw 3237 | . . . . . 6
⊢
(∃𝑎 ∈
ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) | 
| 101 | 97, 100 | bitrdi 287 | . . . . 5
⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) | 
| 102 |  | simprr 772 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) | 
| 103 | 101, 93, 102 | rspcdva 3622 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) | 
| 104 |  | reeanv 3228 | . . . . 5
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) | 
| 105 | 77 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ∈ ℂ) | 
| 106 | 84 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ≠ 0) | 
| 107 |  | simprll 778 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑎 ∈ ℤ) | 
| 108 |  | simprlr 779 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑏 ∈ ℤ) | 
| 109 |  | expaddz 14148 | . . . . . . . . 9
⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) | 
| 110 | 105, 106,
107, 108, 109 | syl22anc 838 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) | 
| 111 |  | simpll 766 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝜑) | 
| 112 | 56 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑍 ∈ Ring) | 
| 113 | 94 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑥 ∈ 𝑈) | 
| 114 | 102 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑦 ∈ 𝑈) | 
| 115 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(.r‘𝑍) = (.r‘𝑍) | 
| 116 | 4, 115 | unitmulcl 20381 | . . . . . . . . . 10
⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) | 
| 117 | 112, 113,
114, 116 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) | 
| 118 | 107, 108 | zaddcld 12728 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑎 + 𝑏) ∈ ℤ) | 
| 119 |  | simprrl 780 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))) | 
| 120 |  | simprrr 781 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) | 
| 121 | 119, 120 | oveq12d 7450 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) | 
| 122 | 11, 17, 18, 19 | dpjghm 20084 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃‘𝐼) ∈ ((𝐻 ↾s (𝐻 DProd 𝑆)) GrpHom 𝐻)) | 
| 123 | 21 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻 ↾s (𝐻 DProd 𝑆)) = (𝐻 ↾s 𝑈)) | 
| 124 | 42 | ovexi 7466 | . . . . . . . . . . . . . . . 16
⊢ 𝐻 ∈ V | 
| 125 | 69 | ressid 17291 | . . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ V → (𝐻 ↾s 𝑈) = 𝐻) | 
| 126 | 124, 125 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ (𝐻 ↾s 𝑈) = 𝐻 | 
| 127 | 123, 126 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻 ↾s (𝐻 DProd 𝑆)) = 𝐻) | 
| 128 | 127 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐻 ↾s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻)) | 
| 129 | 122, 128 | eleqtrd 2842 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻)) | 
| 130 | 129 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻)) | 
| 131 | 4 | fvexi 6919 | . . . . . . . . . . . . 13
⊢ 𝑈 ∈ V | 
| 132 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) | 
| 133 | 132, 115 | mgpplusg 20142 | . . . . . . . . . . . . . 14
⊢
(.r‘𝑍) = (+g‘(mulGrp‘𝑍)) | 
| 134 | 42, 133 | ressplusg 17335 | . . . . . . . . . . . . 13
⊢ (𝑈 ∈ V →
(.r‘𝑍) =
(+g‘𝐻)) | 
| 135 | 131, 134 | ax-mp 5 | . . . . . . . . . . . 12
⊢
(.r‘𝑍) = (+g‘𝐻) | 
| 136 | 69, 135, 135 | ghmlin 19240 | . . . . . . . . . . 11
⊢ (((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦))) | 
| 137 | 130, 113,
114, 136 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦))) | 
| 138 | 58 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝐻 ∈ Grp) | 
| 139 | 68 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑊‘𝐼) ∈ 𝑈) | 
| 140 | 69, 43, 135 | mulgdir 19125 | . . . . . . . . . . 11
⊢ ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊‘𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) | 
| 141 | 138, 107,
108, 139, 140 | syl13anc 1373 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) | 
| 142 | 121, 137,
141 | 3eqtr4d 2786 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼))) | 
| 143 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 27309 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) ∧ ((𝑎 + 𝑏) ∈ ℤ ∧ ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼)))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏))) | 
| 144 | 111, 117,
118, 142, 143 | syl22anc 838 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏))) | 
| 145 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 27309 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑥) = (𝑇↑𝑎)) | 
| 146 | 111, 113,
107, 119, 145 | syl22anc 838 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑥) = (𝑇↑𝑎)) | 
| 147 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 27309 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) → (𝑋‘𝑦) = (𝑇↑𝑏)) | 
| 148 | 111, 114,
108, 120, 147 | syl22anc 838 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑦) = (𝑇↑𝑏)) | 
| 149 | 146, 148 | oveq12d 7450 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) | 
| 150 | 110, 144,
149 | 3eqtr4d 2786 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) | 
| 151 | 150 | expr 456 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) | 
| 152 | 151 | rexlimdvva 3212 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) | 
| 153 | 104, 152 | biimtrrid 243 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) | 
| 154 | 95, 103, 153 | mp2and 699 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) | 
| 155 |  | id 22 | . . . . 5
⊢ (𝜑 → 𝜑) | 
| 156 |  | eqid 2736 | . . . . . . 7
⊢
(1r‘𝑍) = (1r‘𝑍) | 
| 157 | 4, 156 | 1unit 20375 | . . . . . 6
⊢ (𝑍 ∈ Ring →
(1r‘𝑍)
∈ 𝑈) | 
| 158 | 56, 157 | syl 17 | . . . . 5
⊢ (𝜑 → (1r‘𝑍) ∈ 𝑈) | 
| 159 |  | 0zd 12627 | . . . . 5
⊢ (𝜑 → 0 ∈
ℤ) | 
| 160 |  | eqid 2736 | . . . . . . . 8
⊢
(0g‘𝐻) = (0g‘𝐻) | 
| 161 | 160, 160 | ghmid 19241 | . . . . . . 7
⊢ ((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃‘𝐼)‘(0g‘𝐻)) = (0g‘𝐻)) | 
| 162 | 129, 161 | syl 17 | . . . . . 6
⊢ (𝜑 → ((𝑃‘𝐼)‘(0g‘𝐻)) = (0g‘𝐻)) | 
| 163 | 4, 42, 156 | unitgrpid 20386 | . . . . . . . 8
⊢ (𝑍 ∈ Ring →
(1r‘𝑍) =
(0g‘𝐻)) | 
| 164 | 56, 163 | syl 17 | . . . . . . 7
⊢ (𝜑 → (1r‘𝑍) = (0g‘𝐻)) | 
| 165 | 164 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → ((𝑃‘𝐼)‘(1r‘𝑍)) = ((𝑃‘𝐼)‘(0g‘𝐻))) | 
| 166 | 69, 160, 43 | mulg0 19093 | . . . . . . 7
⊢ ((𝑊‘𝐼) ∈ 𝑈 → (0 · (𝑊‘𝐼)) = (0g‘𝐻)) | 
| 167 | 68, 166 | syl 17 | . . . . . 6
⊢ (𝜑 → (0 · (𝑊‘𝐼)) = (0g‘𝐻)) | 
| 168 | 162, 165,
167 | 3eqtr4d 2786 | . . . . 5
⊢ (𝜑 → ((𝑃‘𝐼)‘(1r‘𝑍)) = (0 · (𝑊‘𝐼))) | 
| 169 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 27309 | . . . . 5
⊢ (((𝜑 ∧ (1r‘𝑍) ∈ 𝑈) ∧ (0 ∈ ℤ ∧ ((𝑃‘𝐼)‘(1r‘𝑍)) = (0 · (𝑊‘𝐼)))) → (𝑋‘(1r‘𝑍)) = (𝑇↑0)) | 
| 170 | 155, 158,
159, 168, 169 | syl22anc 838 | . . . 4
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = (𝑇↑0)) | 
| 171 | 77 | exp0d 14181 | . . . 4
⊢ (𝜑 → (𝑇↑0) = 1) | 
| 172 | 170, 171 | eqtrd 2776 | . . 3
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = 1) | 
| 173 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
89, 154, 172 | dchrelbasd 27284 | . 2
⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷) | 
| 174 | 61, 44 | sselid 3980 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝐵) | 
| 175 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑣 = 𝐴 → (𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈)) | 
| 176 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑣 = 𝐴 → (𝑋‘𝑣) = (𝑋‘𝐴)) | 
| 177 | 175, 176 | ifbieq1d 4549 | . . . . . 6
⊢ (𝑣 = 𝐴 → if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) | 
| 178 |  | eqid 2736 | . . . . . 6
⊢ (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) | 
| 179 |  | fvex 6918 | . . . . . . 7
⊢ (𝑋‘𝑣) ∈ V | 
| 180 |  | c0ex 11256 | . . . . . . 7
⊢ 0 ∈
V | 
| 181 | 179, 180 | ifex 4575 | . . . . . 6
⊢ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) ∈ V | 
| 182 | 177, 178,
181 | fvmpt3i 7020 | . . . . 5
⊢ (𝐴 ∈ 𝐵 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) | 
| 183 | 174, 182 | syl 17 | . . . 4
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) | 
| 184 | 44 | iftrued 4532 | . . . 4
⊢ (𝜑 → if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0) = (𝑋‘𝐴)) | 
| 185 | 183, 184 | eqtrd 2776 | . . 3
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = (𝑋‘𝐴)) | 
| 186 |  | fveqeq2 6914 | . . . . . 6
⊢ (𝑣 = 𝐴 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) | 
| 187 | 186 | rexbidv 3178 | . . . . 5
⊢ (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) | 
| 188 | 187, 92, 44 | rspcdva 3622 | . . . 4
⊢ (𝜑 → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))) | 
| 189 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 27309 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = (𝑇↑𝑎)) | 
| 190 | 47 | oveq1i 7442 | . . . . . . . 8
⊢ (𝑇↑𝑎) = ((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) | 
| 191 | 189, 190 | eqtrdi 2792 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = ((-1↑𝑐(2 /
(𝑂‘(𝑊‘𝐼))))↑𝑎)) | 
| 192 | 48 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) ≠ 1 ) | 
| 193 | 58 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝐻 ∈ Grp) | 
| 194 | 68 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑊‘𝐼) ∈ 𝑈) | 
| 195 |  | simprl 770 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ) | 
| 196 | 69, 46, 43, 160 | oddvds 19566 | . . . . . . . . . . 11
⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ 𝑎 ∈ ℤ) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) | 
| 197 | 193, 194,
195, 196 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) | 
| 198 | 71 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) | 
| 199 |  | root1eq1 26799 | . . . . . . . . . . 11
⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎)) | 
| 200 | 198, 195,
199 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎)) | 
| 201 |  | simprr 772 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))) | 
| 202 | 40, 164 | eqtrid 2788 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 =
(0g‘𝐻)) | 
| 203 | 202 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 1 =
(0g‘𝐻)) | 
| 204 | 201, 203 | eqeq12d 2752 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((𝑃‘𝐼)‘𝐴) = 1 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) | 
| 205 | 197, 200,
204 | 3bitr4d 311 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ ((𝑃‘𝐼)‘𝐴) = 1 )) | 
| 206 | 205 | necon3bid 2984 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃‘𝐼)‘𝐴) ≠ 1 )) | 
| 207 | 192, 206 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((-1↑𝑐(2
/ (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1) | 
| 208 | 191, 207 | eqnetrd 3007 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) ≠ 1) | 
| 209 | 208 | rexlimdvaa 3155 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑈) → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1)) | 
| 210 | 44, 209 | mpdan 687 | . . . 4
⊢ (𝜑 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1)) | 
| 211 | 188, 210 | mpd 15 | . . 3
⊢ (𝜑 → (𝑋‘𝐴) ≠ 1) | 
| 212 | 185, 211 | eqnetrd 3007 | . 2
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) | 
| 213 |  | fveq1 6904 | . . . 4
⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → (𝑥‘𝐴) = ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴)) | 
| 214 | 213 | neeq1d 2999 | . . 3
⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → ((𝑥‘𝐴) ≠ 1 ↔ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1)) | 
| 215 | 214 | rspcev 3621 | . 2
⊢ (((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷 ∧ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) | 
| 216 | 173, 212,
215 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |