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

Theorem frgpup3lem 18459
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 17931 . . 3 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋𝐵)
5 ffn 6225 . . 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 18457 . . 3 (𝜑𝐸 ∈ (𝐺 GrpHom 𝐻))
172, 3ghmf 17931 . . 3 (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋𝐵)
18 ffn 6225 . . 3 (𝐸:𝑋𝐵𝐸 Fn 𝑋)
1916, 17, 183syl 18 . 2 (𝜑𝐸 Fn 𝑋)
20 eqid 2765 . . . . . . . . 9 (freeMnd‘(𝐼 × 2𝑜)) = (freeMnd‘(𝐼 × 2𝑜))
2114, 20, 13frgpval 18440 . . . . . . . 8 (𝐼𝑉𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
2210, 21syl 17 . . . . . . 7 (𝜑𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
23 2on 7775 . . . . . . . . . . 11 2𝑜 ∈ On
24 xpexg 7160 . . . . . . . . . . 11 ((𝐼𝑉 ∧ 2𝑜 ∈ On) → (𝐼 × 2𝑜) ∈ V)
2510, 23, 24sylancl 580 . . . . . . . . . 10 (𝜑 → (𝐼 × 2𝑜) ∈ V)
26 wrdexg 13499 . . . . . . . . . 10 ((𝐼 × 2𝑜) ∈ V → Word (𝐼 × 2𝑜) ∈ V)
27 fvi 6446 . . . . . . . . . 10 (Word (𝐼 × 2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
2825, 26, 273syl 18 . . . . . . . . 9 (𝜑 → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
2912, 28syl5eq 2811 . . . . . . . 8 (𝜑𝑊 = Word (𝐼 × 2𝑜))
30 eqid 2765 . . . . . . . . . 10 (Base‘(freeMnd‘(𝐼 × 2𝑜))) = (Base‘(freeMnd‘(𝐼 × 2𝑜)))
3120, 30frmdbas 17659 . . . . . . . . 9 ((𝐼 × 2𝑜) ∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
3225, 31syl 17 . . . . . . . 8 (𝜑 → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
3329, 32eqtr4d 2802 . . . . . . 7 (𝜑𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
3413fvexi 6391 . . . . . . . 8 ∈ V
3534a1i 11 . . . . . . 7 (𝜑 ∈ V)
36 fvexd 6392 . . . . . . 7 (𝜑 → (freeMnd‘(𝐼 × 2𝑜)) ∈ V)
3722, 33, 35, 36qusbas 16474 . . . . . 6 (𝜑 → (𝑊 / ) = (Base‘𝐺))
3837, 2syl6reqr 2818 . . . . 5 (𝜑𝑋 = (𝑊 / ))
39 eqimss 3819 . . . . 5 (𝑋 = (𝑊 / ) → 𝑋 ⊆ (𝑊 / ))
4038, 39syl 17 . . . 4 (𝜑𝑋 ⊆ (𝑊 / ))
4140sselda 3763 . . 3 ((𝜑𝑎𝑋) → 𝑎 ∈ (𝑊 / ))
42 eqid 2765 . . . 4 (𝑊 / ) = (𝑊 / )
43 fveq2 6377 . . . . 5 ([𝑡] = 𝑎 → (𝐾‘[𝑡] ) = (𝐾𝑎))
44 fveq2 6377 . . . . 5 ([𝑡] = 𝑎 → (𝐸‘[𝑡] ) = (𝐸𝑎))
4543, 44eqeq12d 2780 . . . 4 ([𝑡] = 𝑎 → ((𝐾‘[𝑡] ) = (𝐸‘[𝑡] ) ↔ (𝐾𝑎) = (𝐸𝑎)))
46 simpr 477 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑡𝑊)
4729adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑊 = Word (𝐼 × 2𝑜))
4846, 47eleqtrd 2846 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝑡 ∈ Word (𝐼 × 2𝑜))
49 wrdf 13494 . . . . . . . . . . . . 13 (𝑡 ∈ Word (𝐼 × 2𝑜) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2𝑜))
5048, 49syl 17 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2𝑜))
5150ffvelrnda 6551 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑡𝑛) ∈ (𝐼 × 2𝑜))
52 elxp2 5303 . . . . . . . . . . 11 ((𝑡𝑛) ∈ (𝐼 × 2𝑜) ↔ ∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
5351, 52sylib 209 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
54 fveq2 6377 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝐹𝑦) = (𝐹𝑖))
5554fveq2d 6381 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝑁‘(𝐹𝑦)) = (𝑁‘(𝐹𝑖)))
5654, 55ifeq12d 4265 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))) = if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
57 eqeq1 2769 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅))
5857ifbid 4267 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
59 fvex 6390 . . . . . . . . . . . . . . . . 17 (𝐹𝑖) ∈ V
60 fvex 6390 . . . . . . . . . . . . . . . . 17 (𝑁‘(𝐹𝑖)) ∈ V
6159, 60ifex 4293 . . . . . . . . . . . . . . . 16 if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) ∈ V
6256, 58, 8, 61ovmpt2 6996 . . . . . . . . . . . . . . 15 ((𝑖𝐼𝑗 ∈ 2𝑜) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
6362adantl 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
64 elpri 4358 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {∅, 1𝑜} → (𝑗 = ∅ ∨ 𝑗 = 1𝑜))
65 df2o3 7780 . . . . . . . . . . . . . . . . 17 2𝑜 = {∅, 1𝑜}
6664, 65eleq2s 2862 . . . . . . . . . . . . . . . 16 (𝑗 ∈ 2𝑜 → (𝑗 = ∅ ∨ 𝑗 = 1𝑜))
67 frgpup3.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝑈) = 𝐹)
6867adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝐾𝑈) = 𝐹)
6968fveq1d 6379 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐹𝑖))
70 frgpup.u . . . . . . . . . . . . . . . . . . . . . . 23 𝑈 = (varFGrp𝐼)
7113, 70, 14, 2vrgpf 18450 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝑉𝑈:𝐼𝑋)
7210, 71syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:𝐼𝑋)
73 fvco3 6466 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈:𝐼𝑋𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7472, 73sylan 575 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7569, 74eqtr3d 2801 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
7675adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
77 iftrue 4251 . . . . . . . . . . . . . . . . . . 19 (𝑗 = ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
7877adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
79 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅)
8079opeq2d 4568 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, ∅⟩)
8180s1eqd 13575 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, ∅⟩”⟩)
8281eceq1d 7988 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, ∅⟩”⟩] )
8313, 70vrgpval 18449 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8410, 83sylan 575 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8584adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8682, 85eqtr4d 2802 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = (𝑈𝑖))
8786fveq2d 6381 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘(𝑈𝑖)))
8876, 78, 873eqtr4d 2809 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
8975fveq2d 6381 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝑁‘(𝐾‘(𝑈𝑖))))
901adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
9172ffvelrnda 6551 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) ∈ 𝑋)
92 eqid 2765 . . . . . . . . . . . . . . . . . . . . . 22 (invg𝐺) = (invg𝐺)
932, 92, 7ghminv 17934 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈𝑖) ∈ 𝑋) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9490, 91, 93syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9589, 94eqtr4d 2802 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
9695adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
97 1n0 7782 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ≠ ∅
98 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 = 1𝑜)
9998neeq1d 2996 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝑗 ≠ ∅ ↔ 1𝑜 ≠ ∅))
10097, 99mpbiri 249 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 ≠ ∅)
101 ifnefalse 4257 . . . . . . . . . . . . . . . . . . 19 (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
102100, 101syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10398opeq2d 4568 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, 1𝑜⟩)
104103s1eqd 13575 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, 1𝑜⟩”⟩)
105104eceq1d 7988 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
10613, 70, 14, 92vrgpinv 18451 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
10710, 106sylan 575 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
108107adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
109105, 108eqtr4d 2802 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → [⟨“⟨𝑖, 𝑗⟩”⟩] = ((invg𝐺)‘(𝑈𝑖)))
110109fveq2d 6381 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
11196, 102, 1103eqtr4d 2809 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11288, 111jaodan 980 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1𝑜)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11366, 112sylan2 586 . . . . . . . . . . . . . . 15 (((𝜑𝑖𝐼) ∧ 𝑗 ∈ 2𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
114113anasss 458 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11563, 114eqtrd 2799 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
116 fveq2 6377 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑇‘⟨𝑖, 𝑗⟩))
117 df-ov 6847 . . . . . . . . . . . . . . 15 (𝑖𝑇𝑗) = (𝑇‘⟨𝑖, 𝑗⟩)
118116, 117syl6eqr 2817 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑖𝑇𝑗))
119 s1eq 13574 . . . . . . . . . . . . . . . 16 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ⟨“(𝑡𝑛)”⟩ = ⟨“⟨𝑖, 𝑗⟩”⟩)
120119eceq1d 7988 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → [⟨“(𝑡𝑛)”⟩] = [⟨“⟨𝑖, 𝑗⟩”⟩] )
121120fveq2d 6381 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝐾‘[⟨“(𝑡𝑛)”⟩] ) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
122118, 121eqeq12d 2780 . . . . . . . . . . . . 13 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ((𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ) ↔ (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] )))
123115, 122syl5ibrcom 238 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
124123rexlimdvva 3185 . . . . . . . . . . 11 (𝜑 → (∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
125124ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
12653, 125mpd 15 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
127126mpteq2dva 4905 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
1283, 7, 8, 9, 10, 11frgpuptf 18452 . . . . . . . . . 10 (𝜑𝑇:(𝐼 × 2𝑜)⟶𝐵)
129128adantr 472 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝑇:(𝐼 × 2𝑜)⟶𝐵)
130 fcompt 6593 . . . . . . . . 9 ((𝑇:(𝐼 × 2𝑜)⟶𝐵𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2𝑜)) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
131129, 50, 130syl2anc 579 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
13251s1cld 13577 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ Word (𝐼 × 2𝑜))
13329ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → 𝑊 = Word (𝐼 × 2𝑜))
134132, 133eleqtrrd 2847 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ 𝑊)
13514, 13, 12, 2frgpeccl 18443 . . . . . . . . . 10 (⟨“(𝑡𝑛)”⟩ ∈ 𝑊 → [⟨“(𝑡𝑛)”⟩] 𝑋)
136134, 135syl 17 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → [⟨“(𝑡𝑛)”⟩] 𝑋)
13750feqmptd 6440 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝑡 = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑡𝑛)))
13810adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝐼𝑉)
139138, 23, 24sylancl 580 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → (𝐼 × 2𝑜) ∈ V)
140 eqid 2765 . . . . . . . . . . . . 13 (varFMnd‘(𝐼 × 2𝑜)) = (varFMnd‘(𝐼 × 2𝑜))
141140vrmdfval 17663 . . . . . . . . . . . 12 ((𝐼 × 2𝑜) ∈ V → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦ ⟨“𝑤”⟩))
142139, 141syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦ ⟨“𝑤”⟩))
143 s1eq 13574 . . . . . . . . . . 11 (𝑤 = (𝑡𝑛) → ⟨“𝑤”⟩ = ⟨“(𝑡𝑛)”⟩)
14451, 137, 142, 143fmptco 6589 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ ⟨“(𝑡𝑛)”⟩))
145 eqidd 2766 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] ))
146 eceq1 7987 . . . . . . . . . 10 (𝑤 = ⟨“(𝑡𝑛)”⟩ → [𝑤] = [⟨“(𝑡𝑛)”⟩] )
147134, 144, 145, 146fmptco 6589 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ [⟨“(𝑡𝑛)”⟩] ))
1481adantr 472 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
149148, 4syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → 𝐾:𝑋𝐵)
150149feqmptd 6440 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝐾 = (𝑤𝑋 ↦ (𝐾𝑤)))
151 fveq2 6377 . . . . . . . . 9 (𝑤 = [⟨“(𝑡𝑛)”⟩] → (𝐾𝑤) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
152136, 147, 150, 151fmptco 6589 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
153127, 131, 1523eqtr4d 2809 . . . . . . 7 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
154153oveq2d 6860 . . . . . 6 ((𝜑𝑡𝑊) → (𝐻 Σg (𝑇𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
1553, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpupval 18456 . . . . . 6 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐻 Σg (𝑇𝑡)))
156 ghmmhm 17937 . . . . . . . 8 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻))
157148, 156syl 17 . . . . . . 7 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻))
158140vrmdf 17665 . . . . . . . . . . 11 ((𝐼 × 2𝑜) ∈ V → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜))
159139, 158syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜))
16047feq3d 6212 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊 ↔ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜)))
161159, 160mpbird 248 . . . . . . . . 9 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊)
162 wrdco 13863 . . . . . . . . 9 ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊)
16348, 161, 162syl2anc 579 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊)
16433adantr 472 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
165164mpteq1d 4899 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ))
166 eqid 2765 . . . . . . . . . . . . 13 (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] )
16720, 30, 14, 13, 166frgpmhm 18447 . . . . . . . . . . . 12 (𝐼𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
168138, 167syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
169165, 168eqeltrd 2844 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
17030, 2mhmf 17609 . . . . . . . . . 10 ((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋)
171169, 170syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋)
172164feq2d 6211 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ):𝑊𝑋 ↔ (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋))
173171, 172mpbird 248 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋)
174 wrdco 13863 . . . . . . . 8 ((((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊 ∧ (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋)
175163, 173, 174syl2anc 579 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋)
1762gsumwmhm 17652 . . . . . . 7 ((𝐾 ∈ (𝐺 MndHom 𝐻) ∧ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
177157, 175, 176syl2anc 579 . . . . . 6 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
178154, 155, 1773eqtr4d 2809 . . . . 5 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
17920, 140frmdgsum 17669 . . . . . . . . 9 (((𝐼 × 2𝑜) ∈ V ∧ 𝑡 ∈ Word (𝐼 × 2𝑜)) → ((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = 𝑡)
180139, 48, 179syl2anc 579 . . . . . . . 8 ((𝜑𝑡𝑊) → ((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = 𝑡)
181180fveq2d 6381 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = ((𝑤𝑊 ↦ [𝑤] )‘𝑡))
182 wrdco 13863 . . . . . . . . . 10 ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜)) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word Word (𝐼 × 2𝑜))
18348, 159, 182syl2anc 579 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word Word (𝐼 × 2𝑜))
18432adantr 472 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
185 wrdeq 13511 . . . . . . . . . 10 ((Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜) → Word (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word Word (𝐼 × 2𝑜))
186184, 185syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → Word (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word Word (𝐼 × 2𝑜))
187183, 186eleqtrrd 2847 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2𝑜))))
18830gsumwmhm 17652 . . . . . . . 8 (((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺) ∧ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2𝑜)))) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
189169, 187, 188syl2anc 579 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
19012, 13efger 18398 . . . . . . . . 9 Er 𝑊
191190a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → Er 𝑊)
19212fvexi 6391 . . . . . . . . 9 𝑊 ∈ V
193192a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → 𝑊 ∈ V)
194 eqid 2765 . . . . . . . 8 (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] )
195191, 193, 194divsfval 16476 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘𝑡) = [𝑡] )
196181, 189, 1953eqtr3d 2807 . . . . . 6 ((𝜑𝑡𝑊) → (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = [𝑡] )
197196fveq2d 6381 . . . . 5 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐾‘[𝑡] ))
198178, 197eqtr2d 2800 . . . 4 ((𝜑𝑡𝑊) → (𝐾‘[𝑡] ) = (𝐸‘[𝑡] ))
19942, 45, 198ectocld 8019 . . 3 ((𝜑𝑎 ∈ (𝑊 / )) → (𝐾𝑎) = (𝐸𝑎))
20041, 199syldan 585 . 2 ((𝜑𝑎𝑋) → (𝐾𝑎) = (𝐸𝑎))
2016, 19, 200eqfnfvd 6506 1 (𝜑𝐾 = 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wo 873   = wceq 1652  wcel 2155  wne 2937  wrex 3056  Vcvv 3350  wss 3734  c0 4081  ifcif 4245  {cpr 4338  cop 4342  cmpt 4890   I cid 5186   × cxp 5277  ran crn 5280  ccom 5283  Oncon0 5910   Fn wfn 6065  wf 6066  cfv 6070  (class class class)co 6844  cmpt2 6846  1𝑜c1o 7759  2𝑜c2o 7760   Er wer 7946  [cec 7947   / cqs 7948  0cc0 10191  ..^cfzo 12676  chash 13324  Word cword 13489  ⟨“cs1 13569  Basecbs 16133   Σg cgsu 16370   /s cqus 16434   MndHom cmhm 17602  freeMndcfrmd 17654  varFMndcvrmd 17655  Grpcgrp 17692  invgcminusg 17693   GrpHom cghm 17924   ~FG cefg 18386  freeGrpcfrgp 18387  varFGrpcvrgp 18388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-ot 4345  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-ec 7951  df-qs 7955  df-map 8064  df-pm 8065  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-sup 8557  df-inf 8558  df-card 9018  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-xnn0 11613  df-z 11627  df-dec 11744  df-uz 11890  df-fz 12537  df-fzo 12677  df-seq 13012  df-hash 13325  df-word 13490  df-lsw 13537  df-concat 13545  df-s1 13570  df-substr 13620  df-pfx 13665  df-splice 13768  df-reverse 13786  df-s2 13880  df-struct 16135  df-ndx 16136  df-slot 16137  df-base 16139  df-sets 16140  df-ress 16141  df-plusg 16230  df-mulr 16231  df-sca 16233  df-vsca 16234  df-ip 16235  df-tset 16236  df-ple 16237  df-ds 16239  df-0g 16371  df-gsum 16372  df-imas 16437  df-qus 16438  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-mhm 17604  df-submnd 17605  df-frmd 17656  df-vrmd 17657  df-grp 17695  df-minusg 17696  df-ghm 17925  df-efg 18389  df-frgp 18390  df-vrgp 18391
This theorem is referenced by:  frgpup3  18460
  Copyright terms: Public domain W3C validator