Metamath Proof Explorer

Theorem mulgfval

Description: Group multiple (exponentiation) operation. For a shorter proof using ax-rep , see mulgfvalALT . (Contributed by Mario Carneiro, 11-Dec-2014) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 17-Aug-2023)

Ref Expression
Hypotheses mulgval.b ⊢B=BaseG
mulgval.p ⊢+˙=+G
mulgval.o ⊢0˙=0G
mulgval.i ⊢I=invg⁡G
mulgval.t ⊢·˙=⋅G
Assertion mulgfval ⊢·˙=n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n

Proof

Step Hyp Ref Expression
1 mulgval.b ⊢B=BaseG
2 mulgval.p ⊢+˙=+G
3 mulgval.o ⊢0˙=0G
4 mulgval.i ⊢I=invg⁡G
5 mulgval.t ⊢·˙=⋅G
6 eqidd ⊢w=G→ℤ=ℤ
7 fveq2 ⊢w=G→Basew=BaseG
8 7 1 eqtr4di ⊢w=G→Basew=B
9 fveq2 ⊢w=G→0w=0G
10 9 3 eqtr4di ⊢w=G→0w=0˙
11 fvex ⊢+w∈V
12 1z ⊢1∈ℤ
13 11 12 seqexw ⊢seq1+wℕ×x∈V
14 13 a1i ⊢w=G→seq1+wℕ×x∈V
15 id ⊢s=seq1+wℕ×x→s=seq1+wℕ×x
16 fveq2 ⊢w=G→+w=+G
17 16 2 eqtr4di ⊢w=G→+w=+˙
18 17 seqeq2d ⊢w=G→seq1+wℕ×x=seq1+˙ℕ×x
19 15 18 sylan9eqr ⊢w=G∧s=seq1+wℕ×x→s=seq1+˙ℕ×x
20 19 fveq1d ⊢w=G∧s=seq1+wℕ×x→s⁡n=seq1+˙ℕ×x⁡n
21 simpl ⊢w=G∧s=seq1+wℕ×x→w=G
22 21 fveq2d ⊢w=G∧s=seq1+wℕ×x→invg⁡w=invg⁡G
23 22 4 eqtr4di ⊢w=G∧s=seq1+wℕ×x→invg⁡w=I
24 19 fveq1d ⊢w=G∧s=seq1+wℕ×x→s⁡−n=seq1+˙ℕ×x⁡−n
25 23 24 fveq12d ⊢w=G∧s=seq1+wℕ×x→invg⁡w⁡s⁡−n=I⁡seq1+˙ℕ×x⁡−n
26 20 25 ifeq12d ⊢w=G∧s=seq1+wℕ×x→if0<ns⁡ninvg⁡w⁡s⁡−n=if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n
27 14 26 csbied ⊢w=G→⦋seq1+wℕ×x/s⦌if0<ns⁡ninvg⁡w⁡s⁡−n=if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n
28 10 27 ifeq12d ⊢w=G→ifn=00w⦋seq1+wℕ×x/s⦌if0<ns⁡ninvg⁡w⁡s⁡−n=ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n
29 6 8 28 mpoeq123dv ⊢w=G→n∈ℤ,x∈Basew⟼ifn=00w⦋seq1+wℕ×x/s⦌if0<ns⁡ninvg⁡w⁡s⁡−n=n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n
30 df-mulg ⊢⋅𝑔=w∈V⟼n∈ℤ,x∈Basew⟼ifn=00w⦋seq1+wℕ×x/s⦌if0<ns⁡ninvg⁡w⁡s⁡−n
31 zex ⊢ℤ∈V
32 1 fvexi ⊢B∈V
33 snex ⊢0˙∈V
34 2 fvexi ⊢+˙∈V
35 34 rnex ⊢ran⁡+˙∈V
36 35 32 unex ⊢ran⁡+˙∪B∈V
37 4 fvexi ⊢I∈V
38 37 rnex ⊢ran⁡I∈V
39 p0ex ⊢∅∈V
40 38 39 unex ⊢ran⁡I∪∅∈V
41 36 40 unex ⊢ran⁡+˙∪B∪ran⁡I∪∅∈V
42 33 41 unex ⊢0˙∪ran⁡+˙∪B∪ran⁡I∪∅∈V
43 ssun1 ⊢0˙⊆0˙∪ran⁡+˙∪B∪ran⁡I∪∅
44 3 fvexi ⊢0˙∈V
45 44 snid ⊢0˙∈0˙
46 43 45 sselii ⊢0˙∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
47 46 a1i ⊢n∈ℤ∧x∈B→0˙∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
48 ssun2 ⊢B⊆ran⁡+˙∪B
49 ssun1 ⊢ran⁡+˙∪B⊆ran⁡+˙∪B∪ran⁡I∪∅
50 48 49 sstri ⊢B⊆ran⁡+˙∪B∪ran⁡I∪∅
51 ssun2 ⊢ran⁡+˙∪B∪ran⁡I∪∅⊆0˙∪ran⁡+˙∪B∪ran⁡I∪∅
52 50 51 sstri ⊢B⊆0˙∪ran⁡+˙∪B∪ran⁡I∪∅
53 fveq2 ⊢n=1→seq1+˙ℕ×x⁡n=seq1+˙ℕ×x⁡1
54 53 adantl ⊢x∈B∧n=1→seq1+˙ℕ×x⁡n=seq1+˙ℕ×x⁡1
55 seq1 ⊢1∈ℤ→seq1+˙ℕ×x⁡1=ℕ×x⁡1
56 12 55 ax-mp ⊢seq1+˙ℕ×x⁡1=ℕ×x⁡1
57 1nn ⊢1∈ℕ
58 vex ⊢x∈V
59 58 fvconst2 ⊢1∈ℕ→ℕ×x⁡1=x
60 57 59 ax-mp ⊢ℕ×x⁡1=x
61 60 eleq1i ⊢ℕ×x⁡1∈B↔x∈B
62 61 biimpri ⊢x∈B→ℕ×x⁡1∈B
63 56 62 eqeltrid ⊢x∈B→seq1+˙ℕ×x⁡1∈B
64 63 adantr ⊢x∈B∧n=1→seq1+˙ℕ×x⁡1∈B
65 54 64 eqeltrd ⊢x∈B∧n=1→seq1+˙ℕ×x⁡n∈B
66 52 65 sselid ⊢x∈B∧n=1→seq1+˙ℕ×x⁡n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
67 66 ad4ant24 ⊢n∈ℤ∧x∈B∧n∈ℤ≥1∧n=1→seq1+˙ℕ×x⁡n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
68 zcn ⊢n∈ℤ→n∈ℂ
69 npcan1 ⊢n∈ℂ→n-1+1=n
70 68 69 syl ⊢n∈ℤ→n-1+1=n
71 70 fveq2d ⊢n∈ℤ→seq1+˙ℕ×x⁡n-1+1=seq1+˙ℕ×x⁡n
72 71 adantr ⊢n∈ℤ∧n−1∈ℤ≥1→seq1+˙ℕ×x⁡n-1+1=seq1+˙ℕ×x⁡n
73 seqp1 ⊢n−1∈ℤ≥1→seq1+˙ℕ×x⁡n-1+1=seq1+˙ℕ×x⁡n−1+˙ℕ×x⁡n-1+1
74 ssun1 ⊢ran⁡+˙⊆ran⁡+˙∪B
75 ssun2 ⊢∅⊆ran⁡I∪∅
76 unss12 ⊢ran⁡+˙⊆ran⁡+˙∪B∧∅⊆ran⁡I∪∅→ran⁡+˙∪∅⊆ran⁡+˙∪B∪ran⁡I∪∅
77 74 75 76 mp2an ⊢ran⁡+˙∪∅⊆ran⁡+˙∪B∪ran⁡I∪∅
78 77 51 sstri ⊢ran⁡+˙∪∅⊆0˙∪ran⁡+˙∪B∪ran⁡I∪∅
79 df-ov ⊢seq1+˙ℕ×x⁡n−1+˙ℕ×x⁡n-1+1=+˙⁡seq1+˙ℕ×x⁡n−1ℕ×x⁡n-1+1
80 fvrn0 ⊢+˙⁡seq1+˙ℕ×x⁡n−1ℕ×x⁡n-1+1∈ran⁡+˙∪∅
81 79 80 eqeltri ⊢seq1+˙ℕ×x⁡n−1+˙ℕ×x⁡n-1+1∈ran⁡+˙∪∅
82 78 81 sselii ⊢seq1+˙ℕ×x⁡n−1+˙ℕ×x⁡n-1+1∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
83 73 82 eqeltrdi ⊢n−1∈ℤ≥1→seq1+˙ℕ×x⁡n-1+1∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
84 83 adantl ⊢n∈ℤ∧n−1∈ℤ≥1→seq1+˙ℕ×x⁡n-1+1∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
85 72 84 eqeltrrd ⊢n∈ℤ∧n−1∈ℤ≥1→seq1+˙ℕ×x⁡n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
86 85 ad4ant14 ⊢n∈ℤ∧x∈B∧n∈ℤ≥1∧n−1∈ℤ≥1→seq1+˙ℕ×x⁡n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
87 uzm1 ⊢n∈ℤ≥1→n=1∨n−1∈ℤ≥1
88 87 adantl ⊢n∈ℤ∧x∈B∧n∈ℤ≥1→n=1∨n−1∈ℤ≥1
89 67 86 88 mpjaodan ⊢n∈ℤ∧x∈B∧n∈ℤ≥1→seq1+˙ℕ×x⁡n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
90 simpr ⊢n∈ℤ∧x∈B∧¬n∈ℤ≥1→¬n∈ℤ≥1
91 seqfn ⊢1∈ℤ→seq1+˙ℕ×xFnℤ≥1
92 12 91 ax-mp ⊢seq1+˙ℕ×xFnℤ≥1
93 92 fndmi ⊢dom⁡seq1+˙ℕ×x=ℤ≥1
94 93 eleq2i ⊢n∈dom⁡seq1+˙ℕ×x↔n∈ℤ≥1
95 90 94 sylnibr ⊢n∈ℤ∧x∈B∧¬n∈ℤ≥1→¬n∈dom⁡seq1+˙ℕ×x
96 ndmfv ⊢¬n∈dom⁡seq1+˙ℕ×x→seq1+˙ℕ×x⁡n=∅
97 95 96 syl ⊢n∈ℤ∧x∈B∧¬n∈ℤ≥1→seq1+˙ℕ×x⁡n=∅
98 ssun2 ⊢ran⁡I∪∅⊆ran⁡+˙∪B∪ran⁡I∪∅
99 75 98 sstri ⊢∅⊆ran⁡+˙∪B∪ran⁡I∪∅
100 99 51 sstri ⊢∅⊆0˙∪ran⁡+˙∪B∪ran⁡I∪∅
101 0ex ⊢∅∈V
102 101 snid ⊢∅∈∅
103 100 102 sselii ⊢∅∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
104 103 a1i ⊢n∈ℤ∧x∈B∧¬n∈ℤ≥1→∅∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
105 97 104 eqeltrd ⊢n∈ℤ∧x∈B∧¬n∈ℤ≥1→seq1+˙ℕ×x⁡n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
106 89 105 pm2.61dan ⊢n∈ℤ∧x∈B→seq1+˙ℕ×x⁡n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
107 98 51 sstri ⊢ran⁡I∪∅⊆0˙∪ran⁡+˙∪B∪ran⁡I∪∅
108 fvrn0 ⊢I⁡seq1+˙ℕ×x⁡−n∈ran⁡I∪∅
109 107 108 sselii ⊢I⁡seq1+˙ℕ×x⁡−n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
110 109 a1i ⊢n∈ℤ∧x∈B→I⁡seq1+˙ℕ×x⁡−n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
111 106 110 ifcld ⊢n∈ℤ∧x∈B→if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
112 47 111 ifcld ⊢n∈ℤ∧x∈B→ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
113 112 rgen2 ⊢∀n∈ℤ∀x∈Bifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n∈0˙∪ran⁡+˙∪B∪ran⁡I∪∅
114 31 32 42 113 mpoexw ⊢n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n∈V
115 29 30 114 fvmpt ⊢G∈V→⋅G=n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n
116 fvprc ⊢¬G∈V→⋅G=∅
117 eqid ⊢n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n=n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n
118 fvex ⊢seq1+˙ℕ×x⁡n∈V
119 fvex ⊢I⁡seq1+˙ℕ×x⁡−n∈V
120 118 119 ifex ⊢if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n∈V
121 44 120 ifex ⊢ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n∈V
122 117 121 fnmpoi ⊢n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−nFnℤ×B
123 fvprc ⊢¬G∈V→BaseG=∅
124 1 123 eqtrid ⊢¬G∈V→B=∅
125 124 xpeq2d ⊢¬G∈V→ℤ×B=ℤ×∅
126 xp0 ⊢ℤ×∅=∅
127 125 126 eqtrdi ⊢¬G∈V→ℤ×B=∅
128 127 fneq2d ⊢¬G∈V→n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−nFnℤ×B↔n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−nFn∅
129 122 128 mpbii ⊢¬G∈V→n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−nFn∅
130 fn0 ⊢n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−nFn∅↔n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n=∅
131 129 130 sylib ⊢¬G∈V→n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n=∅
132 116 131 eqtr4d ⊢¬G∈V→⋅G=n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n
133 115 132 pm2.61i ⊢⋅G=n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n
134 5 133 eqtri ⊢·˙=n∈ℤ,x∈B⟼ifn=00˙if0<nseq1+˙ℕ×x⁡nI⁡seq1+˙ℕ×x⁡−n