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

Theorem frgpup3lem 18388
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 17863 . . 3 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋𝐵)
5 ffn 6204 . . 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 18386 . . 3 (𝜑𝐸 ∈ (𝐺 GrpHom 𝐻))
172, 3ghmf 17863 . . 3 (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋𝐵)
18 ffn 6204 . . 3 (𝐸:𝑋𝐵𝐸 Fn 𝑋)
1916, 17, 183syl 18 . 2 (𝜑𝐸 Fn 𝑋)
20 eqid 2758 . . . . . . . . 9 (freeMnd‘(𝐼 × 2𝑜)) = (freeMnd‘(𝐼 × 2𝑜))
2114, 20, 13frgpval 18369 . . . . . . . 8 (𝐼𝑉𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
2210, 21syl 17 . . . . . . 7 (𝜑𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
23 2on 7735 . . . . . . . . . . 11 2𝑜 ∈ On
24 xpexg 7123 . . . . . . . . . . 11 ((𝐼𝑉 ∧ 2𝑜 ∈ On) → (𝐼 × 2𝑜) ∈ V)
2510, 23, 24sylancl 697 . . . . . . . . . 10 (𝜑 → (𝐼 × 2𝑜) ∈ V)
26 wrdexg 13499 . . . . . . . . . 10 ((𝐼 × 2𝑜) ∈ V → Word (𝐼 × 2𝑜) ∈ V)
27 fvi 6415 . . . . . . . . . 10 (Word (𝐼 × 2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
2825, 26, 273syl 18 . . . . . . . . 9 (𝜑 → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
2912, 28syl5eq 2804 . . . . . . . 8 (𝜑𝑊 = Word (𝐼 × 2𝑜))
30 eqid 2758 . . . . . . . . . 10 (Base‘(freeMnd‘(𝐼 × 2𝑜))) = (Base‘(freeMnd‘(𝐼 × 2𝑜)))
3120, 30frmdbas 17588 . . . . . . . . 9 ((𝐼 × 2𝑜) ∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
3225, 31syl 17 . . . . . . . 8 (𝜑 → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
3329, 32eqtr4d 2795 . . . . . . 7 (𝜑𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
34 fvex 6360 . . . . . . . . 9 ( ~FG𝐼) ∈ V
3513, 34eqeltri 2833 . . . . . . . 8 ∈ V
3635a1i 11 . . . . . . 7 (𝜑 ∈ V)
37 fvexd 6362 . . . . . . 7 (𝜑 → (freeMnd‘(𝐼 × 2𝑜)) ∈ V)
3822, 33, 36, 37qusbas 16405 . . . . . 6 (𝜑 → (𝑊 / ) = (Base‘𝐺))
3938, 2syl6reqr 2811 . . . . 5 (𝜑𝑋 = (𝑊 / ))
40 eqimss 3796 . . . . 5 (𝑋 = (𝑊 / ) → 𝑋 ⊆ (𝑊 / ))
4139, 40syl 17 . . . 4 (𝜑𝑋 ⊆ (𝑊 / ))
4241sselda 3742 . . 3 ((𝜑𝑎𝑋) → 𝑎 ∈ (𝑊 / ))
43 eqid 2758 . . . 4 (𝑊 / ) = (𝑊 / )
44 fveq2 6350 . . . . 5 ([𝑡] = 𝑎 → (𝐾‘[𝑡] ) = (𝐾𝑎))
45 fveq2 6350 . . . . 5 ([𝑡] = 𝑎 → (𝐸‘[𝑡] ) = (𝐸𝑎))
4644, 45eqeq12d 2773 . . . 4 ([𝑡] = 𝑎 → ((𝐾‘[𝑡] ) = (𝐸‘[𝑡] ) ↔ (𝐾𝑎) = (𝐸𝑎)))
47 simpr 479 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑡𝑊)
4829adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑊 = Word (𝐼 × 2𝑜))
4947, 48eleqtrd 2839 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝑡 ∈ Word (𝐼 × 2𝑜))
50 wrdf 13494 . . . . . . . . . . . . 13 (𝑡 ∈ Word (𝐼 × 2𝑜) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2𝑜))
5149, 50syl 17 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2𝑜))
5251ffvelrnda 6520 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑡𝑛) ∈ (𝐼 × 2𝑜))
53 elxp2 5287 . . . . . . . . . . 11 ((𝑡𝑛) ∈ (𝐼 × 2𝑜) ↔ ∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
5452, 53sylib 208 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
55 fveq2 6350 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝐹𝑦) = (𝐹𝑖))
5655fveq2d 6354 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝑁‘(𝐹𝑦)) = (𝑁‘(𝐹𝑖)))
5755, 56ifeq12d 4248 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))) = if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
58 eqeq1 2762 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅))
5958ifbid 4250 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
60 fvex 6360 . . . . . . . . . . . . . . . . 17 (𝐹𝑖) ∈ V
61 fvex 6360 . . . . . . . . . . . . . . . . 17 (𝑁‘(𝐹𝑖)) ∈ V
6260, 61ifex 4298 . . . . . . . . . . . . . . . 16 if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) ∈ V
6357, 59, 8, 62ovmpt2 6959 . . . . . . . . . . . . . . 15 ((𝑖𝐼𝑗 ∈ 2𝑜) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
6463adantl 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
65 elpri 4340 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {∅, 1𝑜} → (𝑗 = ∅ ∨ 𝑗 = 1𝑜))
66 df2o3 7740 . . . . . . . . . . . . . . . . 17 2𝑜 = {∅, 1𝑜}
6765, 66eleq2s 2855 . . . . . . . . . . . . . . . 16 (𝑗 ∈ 2𝑜 → (𝑗 = ∅ ∨ 𝑗 = 1𝑜))
68 frgpup3.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝑈) = 𝐹)
6968adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝐾𝑈) = 𝐹)
7069fveq1d 6352 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐹𝑖))
71 frgpup.u . . . . . . . . . . . . . . . . . . . . . . 23 𝑈 = (varFGrp𝐼)
7213, 71, 14, 2vrgpf 18379 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝑉𝑈:𝐼𝑋)
7310, 72syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:𝐼𝑋)
74 fvco3 6435 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈:𝐼𝑋𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7573, 74sylan 489 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7670, 75eqtr3d 2794 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
7776adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
78 iftrue 4234 . . . . . . . . . . . . . . . . . . 19 (𝑗 = ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
7978adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
80 simpr 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅)
8180opeq2d 4558 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, ∅⟩)
8281s1eqd 13569 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, ∅⟩”⟩)
8382eceq1d 7948 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, ∅⟩”⟩] )
8413, 71vrgpval 18378 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8510, 84sylan 489 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8685adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8783, 86eqtr4d 2795 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = (𝑈𝑖))
8887fveq2d 6354 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘(𝑈𝑖)))
8977, 79, 883eqtr4d 2802 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
9076fveq2d 6354 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝑁‘(𝐾‘(𝑈𝑖))))
911adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
9273ffvelrnda 6520 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) ∈ 𝑋)
93 eqid 2758 . . . . . . . . . . . . . . . . . . . . . 22 (invg𝐺) = (invg𝐺)
942, 93, 7ghminv 17866 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈𝑖) ∈ 𝑋) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9591, 92, 94syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9690, 95eqtr4d 2795 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
9796adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
98 1n0 7742 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ≠ ∅
99 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 = 1𝑜)
10099neeq1d 2989 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝑗 ≠ ∅ ↔ 1𝑜 ≠ ∅))
10198, 100mpbiri 248 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 ≠ ∅)
102 ifnefalse 4240 . . . . . . . . . . . . . . . . . . 19 (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
103101, 102syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10499opeq2d 4558 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, 1𝑜⟩)
105104s1eqd 13569 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, 1𝑜⟩”⟩)
106105eceq1d 7948 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
10713, 71, 14, 93vrgpinv 18380 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
10810, 107sylan 489 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
109108adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
110106, 109eqtr4d 2795 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → [⟨“⟨𝑖, 𝑗⟩”⟩] = ((invg𝐺)‘(𝑈𝑖)))
111110fveq2d 6354 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
11297, 103, 1113eqtr4d 2802 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11389, 112jaodan 861 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1𝑜)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11467, 113sylan2 492 . . . . . . . . . . . . . . 15 (((𝜑𝑖𝐼) ∧ 𝑗 ∈ 2𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
115114anasss 682 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11664, 115eqtrd 2792 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
117 fveq2 6350 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑇‘⟨𝑖, 𝑗⟩))
118 df-ov 6814 . . . . . . . . . . . . . . 15 (𝑖𝑇𝑗) = (𝑇‘⟨𝑖, 𝑗⟩)
119117, 118syl6eqr 2810 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑖𝑇𝑗))
120 s1eq 13568 . . . . . . . . . . . . . . . 16 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ⟨“(𝑡𝑛)”⟩ = ⟨“⟨𝑖, 𝑗⟩”⟩)
121120eceq1d 7948 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → [⟨“(𝑡𝑛)”⟩] = [⟨“⟨𝑖, 𝑗⟩”⟩] )
122121fveq2d 6354 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝐾‘[⟨“(𝑡𝑛)”⟩] ) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
123119, 122eqeq12d 2773 . . . . . . . . . . . . 13 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ((𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ) ↔ (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] )))
124116, 123syl5ibrcom 237 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
125124rexlimdvva 3174 . . . . . . . . . . 11 (𝜑 → (∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
126125ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
12754, 126mpd 15 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
128127mpteq2dva 4894 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
1293, 7, 8, 9, 10, 11frgpuptf 18381 . . . . . . . . . 10 (𝜑𝑇:(𝐼 × 2𝑜)⟶𝐵)
130129adantr 472 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝑇:(𝐼 × 2𝑜)⟶𝐵)
131 fcompt 6561 . . . . . . . . 9 ((𝑇:(𝐼 × 2𝑜)⟶𝐵𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2𝑜)) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
132130, 51, 131syl2anc 696 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
13352s1cld 13571 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ Word (𝐼 × 2𝑜))
13429ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → 𝑊 = Word (𝐼 × 2𝑜))
135133, 134eleqtrrd 2840 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ 𝑊)
13614, 13, 12, 2frgpeccl 18372 . . . . . . . . . 10 (⟨“(𝑡𝑛)”⟩ ∈ 𝑊 → [⟨“(𝑡𝑛)”⟩] 𝑋)
137135, 136syl 17 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → [⟨“(𝑡𝑛)”⟩] 𝑋)
13851feqmptd 6409 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝑡 = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑡𝑛)))
13910adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝐼𝑉)
140139, 23, 24sylancl 697 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → (𝐼 × 2𝑜) ∈ V)
141 eqid 2758 . . . . . . . . . . . . 13 (varFMnd‘(𝐼 × 2𝑜)) = (varFMnd‘(𝐼 × 2𝑜))
142141vrmdfval 17592 . . . . . . . . . . . 12 ((𝐼 × 2𝑜) ∈ V → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦ ⟨“𝑤”⟩))
143140, 142syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦ ⟨“𝑤”⟩))
144 s1eq 13568 . . . . . . . . . . 11 (𝑤 = (𝑡𝑛) → ⟨“𝑤”⟩ = ⟨“(𝑡𝑛)”⟩)
14552, 138, 143, 144fmptco 6557 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ ⟨“(𝑡𝑛)”⟩))
146 eqidd 2759 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] ))
147 eceq1 7947 . . . . . . . . . 10 (𝑤 = ⟨“(𝑡𝑛)”⟩ → [𝑤] = [⟨“(𝑡𝑛)”⟩] )
148135, 145, 146, 147fmptco 6557 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ [⟨“(𝑡𝑛)”⟩] ))
1491adantr 472 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
150149, 4syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → 𝐾:𝑋𝐵)
151150feqmptd 6409 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝐾 = (𝑤𝑋 ↦ (𝐾𝑤)))
152 fveq2 6350 . . . . . . . . 9 (𝑤 = [⟨“(𝑡𝑛)”⟩] → (𝐾𝑤) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
153137, 148, 151, 152fmptco 6557 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
154128, 132, 1533eqtr4d 2802 . . . . . . 7 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
155154oveq2d 6827 . . . . . 6 ((𝜑𝑡𝑊) → (𝐻 Σg (𝑇𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
1563, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpupval 18385 . . . . . 6 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐻 Σg (𝑇𝑡)))
157 ghmmhm 17869 . . . . . . . 8 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻))
158149, 157syl 17 . . . . . . 7 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻))
159141vrmdf 17594 . . . . . . . . . . 11 ((𝐼 × 2𝑜) ∈ V → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜))
160140, 159syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜))
16148feq3d 6191 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊 ↔ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜)))
162160, 161mpbird 247 . . . . . . . . 9 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊)
163 wrdco 13775 . . . . . . . . 9 ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊)
16449, 162, 163syl2anc 696 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊)
16533adantr 472 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
166165mpteq1d 4888 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ))
167 eqid 2758 . . . . . . . . . . . . 13 (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] )
16820, 30, 14, 13, 167frgpmhm 18376 . . . . . . . . . . . 12 (𝐼𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
169139, 168syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
170166, 169eqeltrd 2837 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
17130, 2mhmf 17539 . . . . . . . . . 10 ((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋)
172170, 171syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋)
173165feq2d 6190 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ):𝑊𝑋 ↔ (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋))
174172, 173mpbird 247 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋)
175 wrdco 13775 . . . . . . . 8 ((((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊 ∧ (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋)
176164, 174, 175syl2anc 696 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋)
1772gsumwmhm 17581 . . . . . . 7 ((𝐾 ∈ (𝐺 MndHom 𝐻) ∧ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
178158, 176, 177syl2anc 696 . . . . . 6 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
179155, 156, 1783eqtr4d 2802 . . . . 5 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
18020, 141frmdgsum 17598 . . . . . . . . 9 (((𝐼 × 2𝑜) ∈ V ∧ 𝑡 ∈ Word (𝐼 × 2𝑜)) → ((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = 𝑡)
181140, 49, 180syl2anc 696 . . . . . . . 8 ((𝜑𝑡𝑊) → ((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = 𝑡)
182181fveq2d 6354 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = ((𝑤𝑊 ↦ [𝑤] )‘𝑡))
183 wrdco 13775 . . . . . . . . . 10 ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜)) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word Word (𝐼 × 2𝑜))
18449, 160, 183syl2anc 696 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word Word (𝐼 × 2𝑜))
18532adantr 472 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
186 wrdeq 13511 . . . . . . . . . 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 2840 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2𝑜))))
18930gsumwmhm 17581 . . . . . . . 8 (((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺) ∧ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2𝑜)))) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
190170, 188, 189syl2anc 696 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
19112, 13efger 18329 . . . . . . . . 9 Er 𝑊
192191a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → Er 𝑊)
193 fvex 6360 . . . . . . . . . 10 ( I ‘Word (𝐼 × 2𝑜)) ∈ V
19412, 193eqeltri 2833 . . . . . . . . 9 𝑊 ∈ V
195194a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → 𝑊 ∈ V)
196 eqid 2758 . . . . . . . 8 (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] )
197192, 195, 196divsfval 16407 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘𝑡) = [𝑡] )
198182, 190, 1973eqtr3d 2800 . . . . . 6 ((𝜑𝑡𝑊) → (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = [𝑡] )
199198fveq2d 6354 . . . . 5 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐾‘[𝑡] ))
200179, 199eqtr2d 2793 . . . 4 ((𝜑𝑡𝑊) → (𝐾‘[𝑡] ) = (𝐸‘[𝑡] ))
20143, 46, 200ectocld 7979 . . 3 ((𝜑𝑎 ∈ (𝑊 / )) → (𝐾𝑎) = (𝐸𝑎))
20242, 201syldan 488 . 2 ((𝜑𝑎𝑋) → (𝐾𝑎) = (𝐸𝑎))
2036, 19, 202eqfnfvd 6475 1 (𝜑𝐾 = 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383   = wceq 1630  wcel 2137  wne 2930  wrex 3049  Vcvv 3338  wss 3713  c0 4056  ifcif 4228  {cpr 4321  cop 4325  cmpt 4879   I cid 5171   × cxp 5262  ran crn 5265  ccom 5268  Oncon0 5882   Fn wfn 6042  wf 6043  cfv 6047  (class class class)co 6811  cmpt2 6813  1𝑜c1o 7720  2𝑜c2o 7721   Er wer 7906  [cec 7907   / cqs 7908  0cc0 10126  ..^cfzo 12657  chash 13309  Word cword 13475  ⟨“cs1 13478  Basecbs 16057   Σg cgsu 16301   /s cqus 16365   MndHom cmhm 17532  freeMndcfrmd 17583  varFMndcvrmd 17584  Grpcgrp 17621  invgcminusg 17622   GrpHom cghm 17856   ~FG cefg 18317  freeGrpcfrgp 18318  varFGrpcvrgp 18319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-ot 4328  df-uni 4587  df-int 4626  df-iun 4672  df-iin 4673  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-2o 7728  df-oadd 7731  df-er 7909  df-ec 7911  df-qs 7915  df-map 8023  df-pm 8024  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-sup 8511  df-inf 8512  df-card 8953  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-nn 11211  df-2 11269  df-3 11270  df-4 11271  df-5 11272  df-6 11273  df-7 11274  df-8 11275  df-9 11276  df-n0 11483  df-xnn0 11554  df-z 11568  df-dec 11684  df-uz 11878  df-fz 12518  df-fzo 12658  df-seq 12994  df-hash 13310  df-word 13483  df-lsw 13484  df-concat 13485  df-s1 13486  df-substr 13487  df-splice 13488  df-reverse 13489  df-s2 13791  df-struct 16059  df-ndx 16060  df-slot 16061  df-base 16063  df-sets 16064  df-ress 16065  df-plusg 16154  df-mulr 16155  df-sca 16157  df-vsca 16158  df-ip 16159  df-tset 16160  df-ple 16161  df-ds 16164  df-0g 16302  df-gsum 16303  df-imas 16368  df-qus 16369  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-mhm 17534  df-submnd 17535  df-frmd 17585  df-vrmd 17586  df-grp 17624  df-minusg 17625  df-ghm 17857  df-efg 18320  df-frgp 18321  df-vrgp 18322
This theorem is referenced by:  frgpup3  18389
  Copyright terms: Public domain W3C validator