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 6191 |
. . 3
⊢ (𝑣 = 𝑥 → (𝑋‘𝑣) = (𝑋‘𝑥)) |
8 | | fveq2 6191 |
. . 3
⊢ (𝑣 = 𝑦 → (𝑋‘𝑣) = (𝑋‘𝑦)) |
9 | | fveq2 6191 |
. . 3
⊢ (𝑣 = (𝑥(.r‘𝑍)𝑦) → (𝑋‘𝑣) = (𝑋‘(𝑥(.r‘𝑍)𝑦))) |
10 | | fveq2 6191 |
. . 3
⊢ (𝑣 = (1r‘𝑍) → (𝑋‘𝑣) = (𝑋‘(1r‘𝑍))) |
11 | | dchrpt.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻dom DProd 𝑆) |
12 | | zex 11386 |
. . . . . . . . . . . . 13
⊢ ℤ
∈ V |
13 | 12 | mptex 6486 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V |
14 | 13 | rnex 7100 |
. . . . . . . . . . 11
⊢ ran
(𝑛 ∈ ℤ ↦
(𝑛 · (𝑊‘𝑘))) ∈ V |
15 | | dchrpt.s |
. . . . . . . . . . 11
⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘)))) |
16 | 14, 15 | dmmpti 6023 |
. . . . . . . . . 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 18456 |
. . . . . . . 8
⊢ (𝜑 → (𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼)) |
21 | | dchrpt.3 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈) |
22 | 21 | feq2d 6031 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼) ↔ (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼))) |
23 | 20, 22 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼)) |
24 | 23 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ (𝑆‘𝐼)) |
25 | 19 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝐼 ∈ dom 𝑊) |
26 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑎 → (𝑛 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝑘))) |
27 | 26 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) |
28 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐼 → (𝑊‘𝑘) = (𝑊‘𝐼)) |
29 | 28 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐼 → (𝑎 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝐼))) |
30 | 29 | mpteq2dv 4745 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
31 | 27, 30 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
32 | 31 | rneqd 5353 |
. . . . . . . 8
⊢ (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
33 | 32, 15, 14 | fvmpt3i 6287 |
. . . . . . 7
⊢ (𝐼 ∈ dom 𝑊 → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
34 | 25, 33 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
35 | 24, 34 | eleqtrd 2703 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
36 | | eqid 2622 |
. . . . . 6
⊢ (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) |
37 | | ovex 6678 |
. . . . . 6
⊢ (𝑎 · (𝑊‘𝐼)) ∈ V |
38 | 36, 37 | elrnmpti 5376 |
. . . . 5
⊢ (((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) |
39 | 35, 38 | sylib 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
⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
50 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 24989 |
. . . . 5
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) = (𝑇↑𝑎)) |
51 | | neg1cn 11124 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
52 | | 2re 11090 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
53 | 5 | nnnn0d 11351 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
54 | 2 | zncrng 19893 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
55 | | crngring 18558 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ Ring) |
57 | 4, 42 | unitgrp 18667 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ Grp) |
59 | 2, 3 | znfi 19908 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) |
60 | 5, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ Fin) |
61 | 3, 4 | unitss 18660 |
. . . . . . . . . . . . 13
⊢ 𝑈 ⊆ 𝐵 |
62 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin) |
63 | 60, 61, 62 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ Fin) |
64 | | wrdf 13310 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(#‘𝑊))⟶𝑈) |
65 | 45, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊:(0..^(#‘𝑊))⟶𝑈) |
66 | | fdm 6051 |
. . . . . . . . . . . . . . 15
⊢ (𝑊:(0..^(#‘𝑊))⟶𝑈 → dom 𝑊 = (0..^(#‘𝑊))) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑊 = (0..^(#‘𝑊))) |
68 | 19, 67 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ (0..^(#‘𝑊))) |
69 | 65, 68 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈) |
70 | 4, 42 | unitgrpbas 18666 |
. . . . . . . . . . . . 13
⊢ 𝑈 = (Base‘𝐻) |
71 | 70, 46 | odcl2 17982 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
72 | 58, 63, 69, 71 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
73 | | nndivre 11056 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ) |
74 | 52, 72, 73 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ) |
75 | 74 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) |
76 | | cxpcl 24420 |
. . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ) |
77 | 51, 75, 76 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ) |
78 | 47, 77 | syl5eqel 2705 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℂ) |
79 | 78 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ∈ ℂ) |
80 | 51 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℂ) |
81 | | neg1ne0 11126 |
. . . . . . . . . 10
⊢ -1 ≠
0 |
82 | 81 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -1 ≠
0) |
83 | 80, 82, 75 | cxpne0d 24459 |
. . . . . . . 8
⊢ (𝜑 →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0) |
84 | 47 | neeq1i 2858 |
. . . . . . . 8
⊢ (𝑇 ≠ 0 ↔
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0) |
85 | 83, 84 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ≠ 0) |
86 | 85 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ≠ 0) |
87 | | simprl 794 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ) |
88 | 79, 86, 87 | expclzd 13013 |
. . . . 5
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑇↑𝑎) ∈ ℂ) |
89 | 50, 88 | eqeltrd 2701 |
. . . 4
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) ∈ ℂ) |
90 | 39, 89 | rexlimddv 3035 |
. . 3
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑋‘𝑣) ∈ ℂ) |
91 | | simprl 794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈) |
92 | 39 | ralrimiva 2966 |
. . . . . 6
⊢ (𝜑 → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) |
93 | 92 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) |
94 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑣 = 𝑥 → ((𝑃‘𝐼)‘𝑣) = ((𝑃‘𝐼)‘𝑥)) |
95 | 94 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑣 = 𝑥 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) |
96 | 95 | rexbidv 3052 |
. . . . . 6
⊢ (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) |
97 | 96 | rspcv 3305 |
. . . . 5
⊢ (𝑥 ∈ 𝑈 → (∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) |
98 | 91, 93, 97 | sylc 65 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))) |
99 | | simprr 796 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
100 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → ((𝑃‘𝐼)‘𝑣) = ((𝑃‘𝐼)‘𝑦)) |
101 | 100 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)))) |
102 | 101 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)))) |
103 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝑎 · (𝑊‘𝐼)) = (𝑏 · (𝑊‘𝐼))) |
104 | 103 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) |
105 | 104 | cbvrexv 3172 |
. . . . . . 7
⊢
(∃𝑎 ∈
ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) |
106 | 102, 105 | syl6bb 276 |
. . . . . 6
⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) |
107 | 106 | rspcv 3305 |
. . . . 5
⊢ (𝑦 ∈ 𝑈 → (∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) |
108 | 99, 93, 107 | sylc 65 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) |
109 | | reeanv 3107 |
. . . . 5
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) |
110 | 78 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ∈ ℂ) |
111 | 85 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ≠ 0) |
112 | | simprll 802 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑎 ∈ ℤ) |
113 | | simprlr 803 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑏 ∈ ℤ) |
114 | | expaddz 12904 |
. . . . . . . . 9
⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) |
115 | 110, 111,
112, 113, 114 | syl22anc 1327 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) |
116 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝜑) |
117 | 56 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑍 ∈ Ring) |
118 | 91 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑥 ∈ 𝑈) |
119 | 99 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑦 ∈ 𝑈) |
120 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.r‘𝑍) = (.r‘𝑍) |
121 | 4, 120 | unitmulcl 18664 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) |
122 | 117, 118,
119, 121 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) |
123 | 112, 113 | zaddcld 11486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑎 + 𝑏) ∈ ℤ) |
124 | | simprrl 804 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))) |
125 | | simprrr 805 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) |
126 | 124, 125 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) |
127 | 11, 17, 18, 19 | dpjghm 18462 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃‘𝐼) ∈ ((𝐻 ↾s (𝐻 DProd 𝑆)) GrpHom 𝐻)) |
128 | 21 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻 ↾s (𝐻 DProd 𝑆)) = (𝐻 ↾s 𝑈)) |
129 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
⊢
((mulGrp‘𝑍)
↾s 𝑈)
∈ V |
130 | 42, 129 | eqeltri 2697 |
. . . . . . . . . . . . . . . 16
⊢ 𝐻 ∈ V |
131 | 70 | ressid 15935 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ V → (𝐻 ↾s 𝑈) = 𝐻) |
132 | 130, 131 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 ↾s 𝑈) = 𝐻 |
133 | 128, 132 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻 ↾s (𝐻 DProd 𝑆)) = 𝐻) |
134 | 133 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐻 ↾s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻)) |
135 | 127, 134 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻)) |
136 | 135 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻)) |
137 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢
(Unit‘𝑍)
∈ V |
138 | 4, 137 | eqeltri 2697 |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈ V |
139 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
140 | 139, 120 | mgpplusg 18493 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑍) = (+g‘(mulGrp‘𝑍)) |
141 | 42, 140 | ressplusg 15993 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ V →
(.r‘𝑍) =
(+g‘𝐻)) |
142 | 138, 141 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(.r‘𝑍) = (+g‘𝐻) |
143 | 70, 142, 142 | ghmlin 17665 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦))) |
144 | 136, 118,
119, 143 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦))) |
145 | 58 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝐻 ∈ Grp) |
146 | 69 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑊‘𝐼) ∈ 𝑈) |
147 | 70, 43, 142 | mulgdir 17573 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊‘𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) |
148 | 145, 112,
113, 146, 147 | syl13anc 1328 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) |
149 | 126, 144,
148 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼))) |
150 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 24989 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) ∧ ((𝑎 + 𝑏) ∈ ℤ ∧ ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼)))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏))) |
151 | 116, 122,
123, 149, 150 | syl22anc 1327 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏))) |
152 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 24989 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑥) = (𝑇↑𝑎)) |
153 | 116, 118,
112, 124, 152 | syl22anc 1327 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑥) = (𝑇↑𝑎)) |
154 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 24989 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) → (𝑋‘𝑦) = (𝑇↑𝑏)) |
155 | 116, 119,
113, 125, 154 | syl22anc 1327 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑦) = (𝑇↑𝑏)) |
156 | 153, 155 | oveq12d 6668 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) |
157 | 115, 151,
156 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
158 | 157 | expr 643 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
159 | 158 | rexlimdvva 3038 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
160 | 109, 159 | syl5bir 233 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
161 | 98, 108, 160 | mp2and 715 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
162 | | id 22 |
. . . . 5
⊢ (𝜑 → 𝜑) |
163 | | eqid 2622 |
. . . . . . 7
⊢
(1r‘𝑍) = (1r‘𝑍) |
164 | 4, 163 | 1unit 18658 |
. . . . . 6
⊢ (𝑍 ∈ Ring →
(1r‘𝑍)
∈ 𝑈) |
165 | 56, 164 | syl 17 |
. . . . 5
⊢ (𝜑 → (1r‘𝑍) ∈ 𝑈) |
166 | | 0zd 11389 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
167 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝐻) = (0g‘𝐻) |
168 | 167, 167 | ghmid 17666 |
. . . . . . 7
⊢ ((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃‘𝐼)‘(0g‘𝐻)) = (0g‘𝐻)) |
169 | 135, 168 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑃‘𝐼)‘(0g‘𝐻)) = (0g‘𝐻)) |
170 | 4, 42, 163 | unitgrpid 18669 |
. . . . . . . 8
⊢ (𝑍 ∈ Ring →
(1r‘𝑍) =
(0g‘𝐻)) |
171 | 56, 170 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑍) = (0g‘𝐻)) |
172 | 171 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → ((𝑃‘𝐼)‘(1r‘𝑍)) = ((𝑃‘𝐼)‘(0g‘𝐻))) |
173 | 70, 167, 43 | mulg0 17546 |
. . . . . . 7
⊢ ((𝑊‘𝐼) ∈ 𝑈 → (0 · (𝑊‘𝐼)) = (0g‘𝐻)) |
174 | 69, 173 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0 · (𝑊‘𝐼)) = (0g‘𝐻)) |
175 | 169, 172,
174 | 3eqtr4d 2666 |
. . . . 5
⊢ (𝜑 → ((𝑃‘𝐼)‘(1r‘𝑍)) = (0 · (𝑊‘𝐼))) |
176 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 24989 |
. . . . 5
⊢ (((𝜑 ∧ (1r‘𝑍) ∈ 𝑈) ∧ (0 ∈ ℤ ∧ ((𝑃‘𝐼)‘(1r‘𝑍)) = (0 · (𝑊‘𝐼)))) → (𝑋‘(1r‘𝑍)) = (𝑇↑0)) |
177 | 162, 165,
166, 175, 176 | syl22anc 1327 |
. . . 4
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = (𝑇↑0)) |
178 | 78 | exp0d 13002 |
. . . 4
⊢ (𝜑 → (𝑇↑0) = 1) |
179 | 177, 178 | eqtrd 2656 |
. . 3
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = 1) |
180 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
90, 161, 179 | dchrelbasd 24964 |
. 2
⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷) |
181 | 61, 44 | sseldi 3601 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
182 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → (𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈)) |
183 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → (𝑋‘𝑣) = (𝑋‘𝐴)) |
184 | 182, 183 | ifbieq1d 4109 |
. . . . . 6
⊢ (𝑣 = 𝐴 → if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) |
185 | | eqid 2622 |
. . . . . 6
⊢ (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) |
186 | | fvex 6201 |
. . . . . . 7
⊢ (𝑋‘𝑣) ∈ V |
187 | | c0ex 10034 |
. . . . . . 7
⊢ 0 ∈
V |
188 | 186, 187 | ifex 4156 |
. . . . . 6
⊢ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) ∈ V |
189 | 184, 185,
188 | fvmpt3i 6287 |
. . . . 5
⊢ (𝐴 ∈ 𝐵 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) |
190 | 181, 189 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) |
191 | 44 | iftrued 4094 |
. . . 4
⊢ (𝜑 → if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0) = (𝑋‘𝐴)) |
192 | 190, 191 | eqtrd 2656 |
. . 3
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = (𝑋‘𝐴)) |
193 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑣 = 𝐴 → ((𝑃‘𝐼)‘𝑣) = ((𝑃‘𝐼)‘𝐴)) |
194 | 193 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) |
195 | 194 | rexbidv 3052 |
. . . . . 6
⊢ (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) |
196 | 195 | rspcv 3305 |
. . . . 5
⊢ (𝐴 ∈ 𝑈 → (∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) |
197 | 44, 92, 196 | sylc 65 |
. . . 4
⊢ (𝜑 → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))) |
198 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 24989 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = (𝑇↑𝑎)) |
199 | 47 | oveq1i 6660 |
. . . . . . . 8
⊢ (𝑇↑𝑎) = ((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) |
200 | 198, 199 | syl6eq 2672 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = ((-1↑𝑐(2 /
(𝑂‘(𝑊‘𝐼))))↑𝑎)) |
201 | 48 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) ≠ 1 ) |
202 | 58 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝐻 ∈ Grp) |
203 | 69 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑊‘𝐼) ∈ 𝑈) |
204 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ) |
205 | 70, 46, 43, 167 | oddvds 17966 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ 𝑎 ∈ ℤ) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) |
206 | 202, 203,
204, 205 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) |
207 | 72 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
208 | | root1eq1 24496 |
. . . . . . . . . . 11
⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎)) |
209 | 207, 204,
208 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎)) |
210 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))) |
211 | 40, 171 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 =
(0g‘𝐻)) |
212 | 211 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 1 =
(0g‘𝐻)) |
213 | 210, 212 | eqeq12d 2637 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((𝑃‘𝐼)‘𝐴) = 1 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) |
214 | 206, 209,
213 | 3bitr4d 300 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ ((𝑃‘𝐼)‘𝐴) = 1 )) |
215 | 214 | necon3bid 2838 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃‘𝐼)‘𝐴) ≠ 1 )) |
216 | 201, 215 | mpbird 247 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((-1↑𝑐(2
/ (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1) |
217 | 200, 216 | eqnetrd 2861 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) ≠ 1) |
218 | 217 | rexlimdvaa 3032 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑈) → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1)) |
219 | 44, 218 | mpdan 702 |
. . . 4
⊢ (𝜑 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1)) |
220 | 197, 219 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑋‘𝐴) ≠ 1) |
221 | 192, 220 | eqnetrd 2861 |
. 2
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) |
222 | | fveq1 6190 |
. . . 4
⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → (𝑥‘𝐴) = ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴)) |
223 | 222 | neeq1d 2853 |
. . 3
⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → ((𝑥‘𝐴) ≠ 1 ↔ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1)) |
224 | 223 | rspcev 3309 |
. 2
⊢ (((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷 ∧ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
225 | 180, 221,
224 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |