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

Theorem frgpup3lem 18236
 Description: The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
Hypotheses
Ref Expression
frgpup.b 𝐵 = (Base‘𝐻)
frgpup.n 𝑁 = (invg𝐻)
frgpup.t 𝑇 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
frgpup.h (𝜑𝐻 ∈ Grp)
frgpup.i (𝜑𝐼𝑉)
frgpup.a (𝜑𝐹:𝐼𝐵)
frgpup.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
frgpup.r = ( ~FG𝐼)
frgpup.g 𝐺 = (freeGrp‘𝐼)
frgpup.x 𝑋 = (Base‘𝐺)
frgpup.e 𝐸 = ran (𝑔𝑊 ↦ ⟨[𝑔] , (𝐻 Σg (𝑇𝑔))⟩)
frgpup.u 𝑈 = (varFGrp𝐼)
frgpup3.k (𝜑𝐾 ∈ (𝐺 GrpHom 𝐻))
frgpup3.e (𝜑 → (𝐾𝑈) = 𝐹)
Assertion
Ref Expression
frgpup3lem (𝜑𝐾 = 𝐸)
Distinct variable groups:   𝑦,𝑔,𝑧   𝑔,𝐻   𝑦,𝐹,𝑧   𝑦,𝑁,𝑧   𝐵,𝑔,𝑦,𝑧   𝑇,𝑔   ,𝑔   𝜑,𝑔,𝑦,𝑧   𝑦,𝐼,𝑧   𝑔,𝑊
Allowed substitution hints:   (𝑦,𝑧)   𝑇(𝑦,𝑧)   𝑈(𝑦,𝑧,𝑔)   𝐸(𝑦,𝑧,𝑔)   𝐹(𝑔)   𝐺(𝑦,𝑧,𝑔)   𝐻(𝑦,𝑧)   𝐼(𝑔)   𝐾(𝑦,𝑧,𝑔)   𝑁(𝑔)   𝑉(𝑦,𝑧,𝑔)   𝑊(𝑦,𝑧)   𝑋(𝑦,𝑧,𝑔)

Proof of Theorem frgpup3lem
Dummy variables 𝑎 𝑡 𝑛 𝑖 𝑗 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgpup3.k . . 3 (𝜑𝐾 ∈ (𝐺 GrpHom 𝐻))
2 frgpup.x . . . 4 𝑋 = (Base‘𝐺)
3 frgpup.b . . . 4 𝐵 = (Base‘𝐻)
42, 3ghmf 17711 . . 3 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋𝐵)
5 ffn 6083 . . 3 (𝐾:𝑋𝐵𝐾 Fn 𝑋)
61, 4, 53syl 18 . 2 (𝜑𝐾 Fn 𝑋)
7 frgpup.n . . . 4 𝑁 = (invg𝐻)
8 frgpup.t . . . 4 𝑇 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
9 frgpup.h . . . 4 (𝜑𝐻 ∈ Grp)
10 frgpup.i . . . 4 (𝜑𝐼𝑉)
11 frgpup.a . . . 4 (𝜑𝐹:𝐼𝐵)
12 frgpup.w . . . 4 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
13 frgpup.r . . . 4 = ( ~FG𝐼)
14 frgpup.g . . . 4 𝐺 = (freeGrp‘𝐼)
15 frgpup.e . . . 4 𝐸 = ran (𝑔𝑊 ↦ ⟨[𝑔] , (𝐻 Σg (𝑇𝑔))⟩)
163, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpup1 18234 . . 3 (𝜑𝐸 ∈ (𝐺 GrpHom 𝐻))
172, 3ghmf 17711 . . 3 (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋𝐵)
18 ffn 6083 . . 3 (𝐸:𝑋𝐵𝐸 Fn 𝑋)
1916, 17, 183syl 18 . 2 (𝜑𝐸 Fn 𝑋)
20 eqid 2651 . . . . . . . . 9 (freeMnd‘(𝐼 × 2𝑜)) = (freeMnd‘(𝐼 × 2𝑜))
2114, 20, 13frgpval 18217 . . . . . . . 8 (𝐼𝑉𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
2210, 21syl 17 . . . . . . 7 (𝜑𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
23 2on 7613 . . . . . . . . . . 11 2𝑜 ∈ On
24 xpexg 7002 . . . . . . . . . . 11 ((𝐼𝑉 ∧ 2𝑜 ∈ On) → (𝐼 × 2𝑜) ∈ V)
2510, 23, 24sylancl 695 . . . . . . . . . 10 (𝜑 → (𝐼 × 2𝑜) ∈ V)
26 wrdexg 13347 . . . . . . . . . 10 ((𝐼 × 2𝑜) ∈ V → Word (𝐼 × 2𝑜) ∈ V)
27 fvi 6294 . . . . . . . . . 10 (Word (𝐼 × 2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
2825, 26, 273syl 18 . . . . . . . . 9 (𝜑 → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
2912, 28syl5eq 2697 . . . . . . . 8 (𝜑𝑊 = Word (𝐼 × 2𝑜))
30 eqid 2651 . . . . . . . . . 10 (Base‘(freeMnd‘(𝐼 × 2𝑜))) = (Base‘(freeMnd‘(𝐼 × 2𝑜)))
3120, 30frmdbas 17436 . . . . . . . . 9 ((𝐼 × 2𝑜) ∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
3225, 31syl 17 . . . . . . . 8 (𝜑 → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
3329, 32eqtr4d 2688 . . . . . . 7 (𝜑𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
34 fvex 6239 . . . . . . . . 9 ( ~FG𝐼) ∈ V
3513, 34eqeltri 2726 . . . . . . . 8 ∈ V
3635a1i 11 . . . . . . 7 (𝜑 ∈ V)
37 fvexd 6241 . . . . . . 7 (𝜑 → (freeMnd‘(𝐼 × 2𝑜)) ∈ V)
3822, 33, 36, 37qusbas 16252 . . . . . 6 (𝜑 → (𝑊 / ) = (Base‘𝐺))
3938, 2syl6reqr 2704 . . . . 5 (𝜑𝑋 = (𝑊 / ))
40 eqimss 3690 . . . . 5 (𝑋 = (𝑊 / ) → 𝑋 ⊆ (𝑊 / ))
4139, 40syl 17 . . . 4 (𝜑𝑋 ⊆ (𝑊 / ))
4241sselda 3636 . . 3 ((𝜑𝑎𝑋) → 𝑎 ∈ (𝑊 / ))
43 eqid 2651 . . . 4 (𝑊 / ) = (𝑊 / )
44 fveq2 6229 . . . . 5 ([𝑡] = 𝑎 → (𝐾‘[𝑡] ) = (𝐾𝑎))
45 fveq2 6229 . . . . 5 ([𝑡] = 𝑎 → (𝐸‘[𝑡] ) = (𝐸𝑎))
4644, 45eqeq12d 2666 . . . 4 ([𝑡] = 𝑎 → ((𝐾‘[𝑡] ) = (𝐸‘[𝑡] ) ↔ (𝐾𝑎) = (𝐸𝑎)))
47 simpr 476 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑡𝑊)
4829adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑊 = Word (𝐼 × 2𝑜))
4947, 48eleqtrd 2732 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝑡 ∈ Word (𝐼 × 2𝑜))
50 wrdf 13342 . . . . . . . . . . . . 13 (𝑡 ∈ Word (𝐼 × 2𝑜) → 𝑡:(0..^(#‘𝑡))⟶(𝐼 × 2𝑜))
5149, 50syl 17 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑡:(0..^(#‘𝑡))⟶(𝐼 × 2𝑜))
5251ffvelrnda 6399 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (𝑡𝑛) ∈ (𝐼 × 2𝑜))
53 elxp2 5166 . . . . . . . . . . 11 ((𝑡𝑛) ∈ (𝐼 × 2𝑜) ↔ ∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
5452, 53sylib 208 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → ∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
55 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝐹𝑦) = (𝐹𝑖))
5655fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝑁‘(𝐹𝑦)) = (𝑁‘(𝐹𝑖)))
5755, 56ifeq12d 4139 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))) = if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
58 eqeq1 2655 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅))
5958ifbid 4141 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
60 fvex 6239 . . . . . . . . . . . . . . . . 17 (𝐹𝑖) ∈ V
61 fvex 6239 . . . . . . . . . . . . . . . . 17 (𝑁‘(𝐹𝑖)) ∈ V
6260, 61ifex 4189 . . . . . . . . . . . . . . . 16 if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) ∈ V
6357, 59, 8, 62ovmpt2 6838 . . . . . . . . . . . . . . 15 ((𝑖𝐼𝑗 ∈ 2𝑜) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
6463adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
65 elpri 4230 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {∅, 1𝑜} → (𝑗 = ∅ ∨ 𝑗 = 1𝑜))
66 df2o3 7618 . . . . . . . . . . . . . . . . 17 2𝑜 = {∅, 1𝑜}
6765, 66eleq2s 2748 . . . . . . . . . . . . . . . 16 (𝑗 ∈ 2𝑜 → (𝑗 = ∅ ∨ 𝑗 = 1𝑜))
68 frgpup3.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝑈) = 𝐹)
6968adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝐾𝑈) = 𝐹)
7069fveq1d 6231 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐹𝑖))
71 frgpup.u . . . . . . . . . . . . . . . . . . . . . . 23 𝑈 = (varFGrp𝐼)
7213, 71, 14, 2vrgpf 18227 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝑉𝑈:𝐼𝑋)
7310, 72syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:𝐼𝑋)
74 fvco3 6314 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈:𝐼𝑋𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7573, 74sylan 487 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7670, 75eqtr3d 2687 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
7776adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
78 iftrue 4125 . . . . . . . . . . . . . . . . . . 19 (𝑗 = ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
7978adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
80 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅)
8180opeq2d 4440 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, ∅⟩)
8281s1eqd 13417 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, ∅⟩”⟩)
8382eceq1d 7826 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, ∅⟩”⟩] )
8413, 71vrgpval 18226 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8510, 84sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8685adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8783, 86eqtr4d 2688 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = (𝑈𝑖))
8887fveq2d 6233 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘(𝑈𝑖)))
8977, 79, 883eqtr4d 2695 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
9076fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝑁‘(𝐾‘(𝑈𝑖))))
911adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
9273ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) ∈ 𝑋)
93 eqid 2651 . . . . . . . . . . . . . . . . . . . . . 22 (invg𝐺) = (invg𝐺)
942, 93, 7ghminv 17714 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈𝑖) ∈ 𝑋) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9591, 92, 94syl2anc 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9690, 95eqtr4d 2688 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
9796adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
98 1n0 7620 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ≠ ∅
99 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 = 1𝑜)
10099neeq1d 2882 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝑗 ≠ ∅ ↔ 1𝑜 ≠ ∅))
10198, 100mpbiri 248 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 ≠ ∅)
102 ifnefalse 4131 . . . . . . . . . . . . . . . . . . 19 (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
103101, 102syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10499opeq2d 4440 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, 1𝑜⟩)
105104s1eqd 13417 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, 1𝑜⟩”⟩)
106105eceq1d 7826 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
10713, 71, 14, 93vrgpinv 18228 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
10810, 107sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
109108adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
110106, 109eqtr4d 2688 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → [⟨“⟨𝑖, 𝑗⟩”⟩] = ((invg𝐺)‘(𝑈𝑖)))
111110fveq2d 6233 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
11297, 103, 1113eqtr4d 2695 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11389, 112jaodan 843 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1𝑜)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11467, 113sylan2 490 . . . . . . . . . . . . . . 15 (((𝜑𝑖𝐼) ∧ 𝑗 ∈ 2𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
115114anasss 680 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11664, 115eqtrd 2685 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
117 fveq2 6229 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑇‘⟨𝑖, 𝑗⟩))
118 df-ov 6693 . . . . . . . . . . . . . . 15 (𝑖𝑇𝑗) = (𝑇‘⟨𝑖, 𝑗⟩)
119117, 118syl6eqr 2703 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑖𝑇𝑗))
120 s1eq 13416 . . . . . . . . . . . . . . . 16 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ⟨“(𝑡𝑛)”⟩ = ⟨“⟨𝑖, 𝑗⟩”⟩)
121120eceq1d 7826 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → [⟨“(𝑡𝑛)”⟩] = [⟨“⟨𝑖, 𝑗⟩”⟩] )
122121fveq2d 6233 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝐾‘[⟨“(𝑡𝑛)”⟩] ) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
123119, 122eqeq12d 2666 . . . . . . . . . . . . 13 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ((𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ) ↔ (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] )))
124116, 123syl5ibrcom 237 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
125124rexlimdvva 3067 . . . . . . . . . . 11 (𝜑 → (∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
126125ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
12754, 126mpd 15 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
128127mpteq2dva 4777 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡𝑛))) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
1293, 7, 8, 9, 10, 11frgpuptf 18229 . . . . . . . . . 10 (𝜑𝑇:(𝐼 × 2𝑜)⟶𝐵)
130129adantr 480 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝑇:(𝐼 × 2𝑜)⟶𝐵)
131 fcompt 6440 . . . . . . . . 9 ((𝑇:(𝐼 × 2𝑜)⟶𝐵𝑡:(0..^(#‘𝑡))⟶(𝐼 × 2𝑜)) → (𝑇𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
132130, 51, 131syl2anc 694 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
13352s1cld 13419 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ Word (𝐼 × 2𝑜))
13429ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → 𝑊 = Word (𝐼 × 2𝑜))
135133, 134eleqtrrd 2733 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ 𝑊)
13614, 13, 12, 2frgpeccl 18220 . . . . . . . . . 10 (⟨“(𝑡𝑛)”⟩ ∈ 𝑊 → [⟨“(𝑡𝑛)”⟩] 𝑋)
137135, 136syl 17 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → [⟨“(𝑡𝑛)”⟩] 𝑋)
13851feqmptd 6288 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝑡 = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑡𝑛)))
13910adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝐼𝑉)
140139, 23, 24sylancl 695 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → (𝐼 × 2𝑜) ∈ V)
141 eqid 2651 . . . . . . . . . . . . 13 (varFMnd‘(𝐼 × 2𝑜)) = (varFMnd‘(𝐼 × 2𝑜))
142141vrmdfval 17440 . . . . . . . . . . . 12 ((𝐼 × 2𝑜) ∈ V → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦ ⟨“𝑤”⟩))
143140, 142syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦ ⟨“𝑤”⟩))
144 s1eq 13416 . . . . . . . . . . 11 (𝑤 = (𝑡𝑛) → ⟨“𝑤”⟩ = ⟨“(𝑡𝑛)”⟩)
14552, 138, 143, 144fmptco 6436 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ ⟨“(𝑡𝑛)”⟩))
146 eqidd 2652 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] ))
147 eceq1 7825 . . . . . . . . . 10 (𝑤 = ⟨“(𝑡𝑛)”⟩ → [𝑤] = [⟨“(𝑡𝑛)”⟩] )
148135, 145, 146, 147fmptco 6436 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ [⟨“(𝑡𝑛)”⟩] ))
1491adantr 480 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
150149, 4syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → 𝐾:𝑋𝐵)
151150feqmptd 6288 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝐾 = (𝑤𝑋 ↦ (𝐾𝑤)))
152 fveq2 6229 . . . . . . . . 9 (𝑤 = [⟨“(𝑡𝑛)”⟩] → (𝐾𝑤) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
153137, 148, 151, 152fmptco 6436 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
154128, 132, 1533eqtr4d 2695 . . . . . . 7 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
155154oveq2d 6706 . . . . . 6 ((𝜑𝑡𝑊) → (𝐻 Σg (𝑇𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
1563, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpupval 18233 . . . . . 6 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐻 Σg (𝑇𝑡)))
157 ghmmhm 17717 . . . . . . . 8 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻))
158149, 157syl 17 . . . . . . 7 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻))
159141vrmdf 17442 . . . . . . . . . . 11 ((𝐼 × 2𝑜) ∈ V → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜))
160140, 159syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜))
16148feq3d 6070 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊 ↔ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜)))
162160, 161mpbird 247 . . . . . . . . 9 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊)
163 wrdco 13623 . . . . . . . . 9 ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊)
16449, 162, 163syl2anc 694 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊)
16533adantr 480 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
166165mpteq1d 4771 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ))
167 eqid 2651 . . . . . . . . . . . . 13 (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] )
16820, 30, 14, 13, 167frgpmhm 18224 . . . . . . . . . . . 12 (𝐼𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
169139, 168syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
170166, 169eqeltrd 2730 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
17130, 2mhmf 17387 . . . . . . . . . 10 ((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋)
172170, 171syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋)
173165feq2d 6069 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ):𝑊𝑋 ↔ (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋))
174172, 173mpbird 247 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋)
175 wrdco 13623 . . . . . . . 8 ((((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊 ∧ (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋)
176164, 174, 175syl2anc 694 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋)
1772gsumwmhm 17429 . . . . . . 7 ((𝐾 ∈ (𝐺 MndHom 𝐻) ∧ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
178158, 176, 177syl2anc 694 . . . . . 6 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
179155, 156, 1783eqtr4d 2695 . . . . 5 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
18020, 141frmdgsum 17446 . . . . . . . . 9 (((𝐼 × 2𝑜) ∈ V ∧ 𝑡 ∈ Word (𝐼 × 2𝑜)) → ((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = 𝑡)
181140, 49, 180syl2anc 694 . . . . . . . 8 ((𝜑𝑡𝑊) → ((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = 𝑡)
182181fveq2d 6233 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = ((𝑤𝑊 ↦ [𝑤] )‘𝑡))
183 wrdco 13623 . . . . . . . . . 10 ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜)) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word Word (𝐼 × 2𝑜))
18449, 160, 183syl2anc 694 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word Word (𝐼 × 2𝑜))
18532adantr 480 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
186 wrdeq 13359 . . . . . . . . . 10 ((Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜) → Word (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word Word (𝐼 × 2𝑜))
187185, 186syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → Word (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word Word (𝐼 × 2𝑜))
188184, 187eleqtrrd 2733 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2𝑜))))
18930gsumwmhm 17429 . . . . . . . 8 (((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺) ∧ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2𝑜)))) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
190170, 188, 189syl2anc 694 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
19112, 13efger 18177 . . . . . . . . 9 Er 𝑊
192191a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → Er 𝑊)
193 fvex 6239 . . . . . . . . . 10 ( I ‘Word (𝐼 × 2𝑜)) ∈ V
19412, 193eqeltri 2726 . . . . . . . . 9 𝑊 ∈ V
195194a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → 𝑊 ∈ V)
196 eqid 2651 . . . . . . . 8 (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] )
197192, 195, 196divsfval 16254 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘𝑡) = [𝑡] )
198182, 190, 1973eqtr3d 2693 . . . . . 6 ((𝜑𝑡𝑊) → (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = [𝑡] )
199198fveq2d 6233 . . . . 5 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐾‘[𝑡] ))
200179, 199eqtr2d 2686 . . . 4 ((𝜑𝑡𝑊) → (𝐾‘[𝑡] ) = (𝐸‘[𝑡] ))
20143, 46, 200ectocld 7857 . . 3 ((𝜑𝑎 ∈ (𝑊 / )) → (𝐾𝑎) = (𝐸𝑎))
20242, 201syldan 486 . 2 ((𝜑𝑎𝑋) → (𝐾𝑎) = (𝐸𝑎))
2036, 19, 202eqfnfvd 6354 1 (𝜑𝐾 = 𝐸)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∃wrex 2942  Vcvv 3231   ⊆ wss 3607  ∅c0 3948  ifcif 4119  {cpr 4212  ⟨cop 4216   ↦ cmpt 4762   I cid 5052   × cxp 5141  ran crn 5144   ∘ ccom 5147  Oncon0 5761   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  1𝑜c1o 7598  2𝑜c2o 7599   Er wer 7784  [cec 7785   / cqs 7786  0cc0 9974  ..^cfzo 12504  #chash 13157  Word cword 13323  ⟨“cs1 13326  Basecbs 15904   Σg cgsu 16148   /s cqus 16212   MndHom cmhm 17380  freeMndcfrmd 17431  varFMndcvrmd 17432  Grpcgrp 17469  invgcminusg 17470   GrpHom cghm 17704   ~FG cefg 18165  freeGrpcfrgp 18166  varFGrpcvrgp 18167 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-ot 4219  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-ec 7789  df-qs 7793  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-xnn0 11402  df-z 11416  df-dec 11532  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-word 13331  df-lsw 13332  df-concat 13333  df-s1 13334  df-substr 13335  df-splice 13336  df-reverse 13337  df-s2 13639  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-0g 16149  df-gsum 16150  df-imas 16215  df-qus 16216  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-mhm 17382  df-submnd 17383  df-frmd 17433  df-vrmd 17434  df-grp 17472  df-minusg 17473  df-ghm 17705  df-efg 18168  df-frgp 18169  df-vrgp 18170 This theorem is referenced by:  frgpup3  18237
 Copyright terms: Public domain W3C validator