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

Theorem frgpup3lem 19796
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 𝑇 = (𝑦𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
frgpup.h (𝜑𝐻 ∈ Grp)
frgpup.i (𝜑𝐼𝑉)
frgpup.a (𝜑𝐹:𝐼𝐵)
frgpup.w 𝑊 = ( I ‘Word (𝐼 × 2o))
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 19239 . . 3 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋𝐵)
5 ffn 6735 . . 3 (𝐾:𝑋𝐵𝐾 Fn 𝑋)
61, 4, 53syl 18 . 2 (𝜑𝐾 Fn 𝑋)
7 frgpup.n . . . 4 𝑁 = (invg𝐻)
8 frgpup.t . . . 4 𝑇 = (𝑦𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
9 frgpup.h . . . 4 (𝜑𝐻 ∈ Grp)
10 frgpup.i . . . 4 (𝜑𝐼𝑉)
11 frgpup.a . . . 4 (𝜑𝐹:𝐼𝐵)
12 frgpup.w . . . 4 𝑊 = ( I ‘Word (𝐼 × 2o))
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 19794 . . 3 (𝜑𝐸 ∈ (𝐺 GrpHom 𝐻))
172, 3ghmf 19239 . . 3 (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋𝐵)
18 ffn 6735 . . 3 (𝐸:𝑋𝐵𝐸 Fn 𝑋)
1916, 17, 183syl 18 . 2 (𝜑𝐸 Fn 𝑋)
20 eqid 2736 . . . . . . . . 9 (freeMnd‘(𝐼 × 2o)) = (freeMnd‘(𝐼 × 2o))
2114, 20, 13frgpval 19777 . . . . . . . 8 (𝐼𝑉𝐺 = ((freeMnd‘(𝐼 × 2o)) /s ))
2210, 21syl 17 . . . . . . 7 (𝜑𝐺 = ((freeMnd‘(𝐼 × 2o)) /s ))
23 2on 8521 . . . . . . . . . . 11 2o ∈ On
24 xpexg 7771 . . . . . . . . . . 11 ((𝐼𝑉 ∧ 2o ∈ On) → (𝐼 × 2o) ∈ V)
2510, 23, 24sylancl 586 . . . . . . . . . 10 (𝜑 → (𝐼 × 2o) ∈ V)
26 wrdexg 14563 . . . . . . . . . 10 ((𝐼 × 2o) ∈ V → Word (𝐼 × 2o) ∈ V)
27 fvi 6984 . . . . . . . . . 10 (Word (𝐼 × 2o) ∈ V → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 × 2o))
2825, 26, 273syl 18 . . . . . . . . 9 (𝜑 → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 × 2o))
2912, 28eqtrid 2788 . . . . . . . 8 (𝜑𝑊 = Word (𝐼 × 2o))
30 eqid 2736 . . . . . . . . . 10 (Base‘(freeMnd‘(𝐼 × 2o))) = (Base‘(freeMnd‘(𝐼 × 2o)))
3120, 30frmdbas 18866 . . . . . . . . 9 ((𝐼 × 2o) ∈ V → (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o))
3225, 31syl 17 . . . . . . . 8 (𝜑 → (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o))
3329, 32eqtr4d 2779 . . . . . . 7 (𝜑𝑊 = (Base‘(freeMnd‘(𝐼 × 2o))))
3413fvexi 6919 . . . . . . . 8 ∈ V
3534a1i 11 . . . . . . 7 (𝜑 ∈ V)
36 fvexd 6920 . . . . . . 7 (𝜑 → (freeMnd‘(𝐼 × 2o)) ∈ V)
3722, 33, 35, 36qusbas 17591 . . . . . 6 (𝜑 → (𝑊 / ) = (Base‘𝐺))
382, 37eqtr4id 2795 . . . . 5 (𝜑𝑋 = (𝑊 / ))
39 eqimss 4041 . . . . 5 (𝑋 = (𝑊 / ) → 𝑋 ⊆ (𝑊 / ))
4038, 39syl 17 . . . 4 (𝜑𝑋 ⊆ (𝑊 / ))
4140sselda 3982 . . 3 ((𝜑𝑎𝑋) → 𝑎 ∈ (𝑊 / ))
42 eqid 2736 . . . 4 (𝑊 / ) = (𝑊 / )
43 fveq2 6905 . . . . 5 ([𝑡] = 𝑎 → (𝐾‘[𝑡] ) = (𝐾𝑎))
44 fveq2 6905 . . . . 5 ([𝑡] = 𝑎 → (𝐸‘[𝑡] ) = (𝐸𝑎))
4543, 44eqeq12d 2752 . . . 4 ([𝑡] = 𝑎 → ((𝐾‘[𝑡] ) = (𝐸‘[𝑡] ) ↔ (𝐾𝑎) = (𝐸𝑎)))
46 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑡𝑊)
4729adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑊 = Word (𝐼 × 2o))
4846, 47eleqtrd 2842 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝑡 ∈ Word (𝐼 × 2o))
49 wrdf 14558 . . . . . . . . . . . . 13 (𝑡 ∈ Word (𝐼 × 2o) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o))
5048, 49syl 17 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o))
5150ffvelcdmda 7103 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑡𝑛) ∈ (𝐼 × 2o))
52 elxp2 5708 . . . . . . . . . . 11 ((𝑡𝑛) ∈ (𝐼 × 2o) ↔ ∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
5351, 52sylib 218 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
54 fveq2 6905 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝐹𝑦) = (𝐹𝑖))
5554fveq2d 6909 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝑁‘(𝐹𝑦)) = (𝑁‘(𝐹𝑖)))
5654, 55ifeq12d 4546 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))) = if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
57 eqeq1 2740 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅))
5857ifbid 4548 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
59 fvex 6918 . . . . . . . . . . . . . . . . 17 (𝐹𝑖) ∈ V
60 fvex 6918 . . . . . . . . . . . . . . . . 17 (𝑁‘(𝐹𝑖)) ∈ V
6159, 60ifex 4575 . . . . . . . . . . . . . . . 16 if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) ∈ V
6256, 58, 8, 61ovmpo 7594 . . . . . . . . . . . . . . 15 ((𝑖𝐼𝑗 ∈ 2o) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
6362adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
64 elpri 4648 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {∅, 1o} → (𝑗 = ∅ ∨ 𝑗 = 1o))
65 df2o3 8515 . . . . . . . . . . . . . . . . 17 2o = {∅, 1o}
6664, 65eleq2s 2858 . . . . . . . . . . . . . . . 16 (𝑗 ∈ 2o → (𝑗 = ∅ ∨ 𝑗 = 1o))
67 frgpup3.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝑈) = 𝐹)
6867adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝐾𝑈) = 𝐹)
6968fveq1d 6907 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐹𝑖))
70 frgpup.u . . . . . . . . . . . . . . . . . . . . . . 23 𝑈 = (varFGrp𝐼)
7113, 70, 14, 2vrgpf 19787 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝑉𝑈:𝐼𝑋)
7210, 71syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:𝐼𝑋)
73 fvco3 7007 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈:𝐼𝑋𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7472, 73sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7569, 74eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
7675adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
77 iftrue 4530 . . . . . . . . . . . . . . . . . . 19 (𝑗 = ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
7877adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
79 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅)
8079opeq2d 4879 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, ∅⟩)
8180s1eqd 14640 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, ∅⟩”⟩)
8281eceq1d 8786 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, ∅⟩”⟩] )
8313, 70vrgpval 19786 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8410, 83sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8584adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8682, 85eqtr4d 2779 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = (𝑈𝑖))
8786fveq2d 6909 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘(𝑈𝑖)))
8876, 78, 873eqtr4d 2786 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
8975fveq2d 6909 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝑁‘(𝐾‘(𝑈𝑖))))
9072ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) ∈ 𝑋)
91 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 (invg𝐺) = (invg𝐺)
922, 91, 7ghminv 19242 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈𝑖) ∈ 𝑋) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
931, 90, 92syl2an2r 685 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9489, 93eqtr4d 2779 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
9594adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
96 1n0 8527 . . . . . . . . . . . . . . . . . . . 20 1o ≠ ∅
97 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → 𝑗 = 1o)
9897neeq1d 2999 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝑗 ≠ ∅ ↔ 1o ≠ ∅))
9996, 98mpbiri 258 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → 𝑗 ≠ ∅)
100 ifnefalse 4536 . . . . . . . . . . . . . . . . . . 19 (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10199, 100syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10297opeq2d 4879 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, 1o⟩)
103102s1eqd 14640 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, 1o⟩”⟩)
104103eceq1d 8786 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, 1o⟩”⟩] )
10513, 70, 14, 91vrgpinv 19788 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
10610, 105sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
107106adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
108104, 107eqtr4d 2779 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → [⟨“⟨𝑖, 𝑗⟩”⟩] = ((invg𝐺)‘(𝑈𝑖)))
109108fveq2d 6909 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
11095, 101, 1093eqtr4d 2786 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11188, 110jaodan 959 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1o)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11266, 111sylan2 593 . . . . . . . . . . . . . . 15 (((𝜑𝑖𝐼) ∧ 𝑗 ∈ 2o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
113112anasss 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11463, 113eqtrd 2776 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
115 fveq2 6905 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑇‘⟨𝑖, 𝑗⟩))
116 df-ov 7435 . . . . . . . . . . . . . . 15 (𝑖𝑇𝑗) = (𝑇‘⟨𝑖, 𝑗⟩)
117115, 116eqtr4di 2794 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑖𝑇𝑗))
118 s1eq 14639 . . . . . . . . . . . . . . . 16 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ⟨“(𝑡𝑛)”⟩ = ⟨“⟨𝑖, 𝑗⟩”⟩)
119118eceq1d 8786 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → [⟨“(𝑡𝑛)”⟩] = [⟨“⟨𝑖, 𝑗⟩”⟩] )
120119fveq2d 6909 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝐾‘[⟨“(𝑡𝑛)”⟩] ) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
121117, 120eqeq12d 2752 . . . . . . . . . . . . 13 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ((𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ) ↔ (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] )))
122114, 121syl5ibrcom 247 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
123122rexlimdvva 3212 . . . . . . . . . . 11 (𝜑 → (∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
124123ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
12553, 124mpd 15 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
126125mpteq2dva 5241 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
1273, 7, 8, 9, 10, 11frgpuptf 19789 . . . . . . . . 9 (𝜑𝑇:(𝐼 × 2o)⟶𝐵)
128 fcompt 7152 . . . . . . . . 9 ((𝑇:(𝐼 × 2o)⟶𝐵𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o)) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
129127, 50, 128syl2an2r 685 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
13051s1cld 14642 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ Word (𝐼 × 2o))
13129ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → 𝑊 = Word (𝐼 × 2o))
132130, 131eleqtrrd 2843 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ 𝑊)
13314, 13, 12, 2frgpeccl 19780 . . . . . . . . . 10 (⟨“(𝑡𝑛)”⟩ ∈ 𝑊 → [⟨“(𝑡𝑛)”⟩] 𝑋)
134132, 133syl 17 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → [⟨“(𝑡𝑛)”⟩] 𝑋)
13550feqmptd 6976 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝑡 = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑡𝑛)))
13610adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝐼𝑉)
137136, 23, 24sylancl 586 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → (𝐼 × 2o) ∈ V)
138 eqid 2736 . . . . . . . . . . . . 13 (varFMnd‘(𝐼 × 2o)) = (varFMnd‘(𝐼 × 2o))
139138vrmdfval 18870 . . . . . . . . . . . 12 ((𝐼 × 2o) ∈ V → (varFMnd‘(𝐼 × 2o)) = (𝑤 ∈ (𝐼 × 2o) ↦ ⟨“𝑤”⟩))
140137, 139syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)) = (𝑤 ∈ (𝐼 × 2o) ↦ ⟨“𝑤”⟩))
141 s1eq 14639 . . . . . . . . . . 11 (𝑤 = (𝑡𝑛) → ⟨“𝑤”⟩ = ⟨“(𝑡𝑛)”⟩)
14251, 135, 140, 141fmptco 7148 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ ⟨“(𝑡𝑛)”⟩))
143 eqidd 2737 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] ))
144 eceq1 8785 . . . . . . . . . 10 (𝑤 = ⟨“(𝑡𝑛)”⟩ → [𝑤] = [⟨“(𝑡𝑛)”⟩] )
145132, 142, 143, 144fmptco 7148 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ [⟨“(𝑡𝑛)”⟩] ))
1461adantr 480 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
147146, 4syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → 𝐾:𝑋𝐵)
148147feqmptd 6976 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝐾 = (𝑤𝑋 ↦ (𝐾𝑤)))
149 fveq2 6905 . . . . . . . . 9 (𝑤 = [⟨“(𝑡𝑛)”⟩] → (𝐾𝑤) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
150134, 145, 148, 149fmptco 7148 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
151126, 129, 1503eqtr4d 2786 . . . . . . 7 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))
152151oveq2d 7448 . . . . . 6 ((𝜑𝑡𝑊) → (𝐻 Σg (𝑇𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
1533, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpupval 19793 . . . . . 6 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐻 Σg (𝑇𝑡)))
154 ghmmhm 19245 . . . . . . . 8 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻))
155146, 154syl 17 . . . . . . 7 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻))
156138vrmdf 18872 . . . . . . . . . . 11 ((𝐼 × 2o) ∈ V → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o))
157137, 156syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o))
15847feq3d 6722 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊 ↔ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o)))
159157, 158mpbird 257 . . . . . . . . 9 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊)
160 wrdco 14871 . . . . . . . . 9 ((𝑡 ∈ Word (𝐼 × 2o) ∧ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊)
16148, 159, 160syl2anc 584 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊)
16233adantr 480 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 × 2o))))
163162mpteq1d 5236 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ))
164 eqid 2736 . . . . . . . . . . . . 13 (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] )
16520, 30, 14, 13, 164frgpmhm 19784 . . . . . . . . . . . 12 (𝐼𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
166136, 165syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
167163, 166eqeltrd 2840 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
16830, 2mhmf 18803 . . . . . . . . . 10 ((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋)
169167, 168syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋)
170162feq2d 6721 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ):𝑊𝑋 ↔ (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋))
171169, 170mpbird 257 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋)
172 wrdco 14871 . . . . . . . 8 ((((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊 ∧ (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋)
173161, 171, 172syl2anc 584 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋)
1742gsumwmhm 18859 . . . . . . 7 ((𝐾 ∈ (𝐺 MndHom 𝐻) ∧ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
175155, 173, 174syl2anc 584 . . . . . 6 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
176152, 153, 1753eqtr4d 2786 . . . . 5 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
17720, 138frmdgsum 18876 . . . . . . . . 9 (((𝐼 × 2o) ∈ V ∧ 𝑡 ∈ Word (𝐼 × 2o)) → ((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = 𝑡)
17825, 48, 177syl2an2r 685 . . . . . . . 8 ((𝜑𝑡𝑊) → ((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = 𝑡)
179178fveq2d 6909 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = ((𝑤𝑊 ↦ [𝑤] )‘𝑡))
180 wrdco 14871 . . . . . . . . . 10 ((𝑡 ∈ Word (𝐼 × 2o) ∧ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o)) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word Word (𝐼 × 2o))
18148, 157, 180syl2anc 584 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word Word (𝐼 × 2o))
18232adantr 480 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o))
183 wrdeq 14575 . . . . . . . . . 10 ((Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o) → Word (Base‘(freeMnd‘(𝐼 × 2o))) = Word Word (𝐼 × 2o))
184182, 183syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → Word (Base‘(freeMnd‘(𝐼 × 2o))) = Word Word (𝐼 × 2o))
185181, 184eleqtrrd 2843 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2o))))
18630gsumwmhm 18859 . . . . . . . 8 (((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺) ∧ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2o)))) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))
187167, 185, 186syl2anc 584 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))
18812, 13efger 19737 . . . . . . . . 9 Er 𝑊
189188a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → Er 𝑊)
19012fvexi 6919 . . . . . . . . 9 𝑊 ∈ V
191190a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → 𝑊 ∈ V)
192 eqid 2736 . . . . . . . 8 (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] )
193189, 191, 192divsfval 17593 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘𝑡) = [𝑡] )
194179, 187, 1933eqtr3d 2784 . . . . . 6 ((𝜑𝑡𝑊) → (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = [𝑡] )
195194fveq2d 6909 . . . . 5 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐾‘[𝑡] ))
196176, 195eqtr2d 2777 . . . 4 ((𝜑𝑡𝑊) → (𝐾‘[𝑡] ) = (𝐸‘[𝑡] ))
19742, 45, 196ectocld 8825 . . 3 ((𝜑𝑎 ∈ (𝑊 / )) → (𝐾𝑎) = (𝐸𝑎))
19841, 197syldan 591 . 2 ((𝜑𝑎𝑋) → (𝐾𝑎) = (𝐸𝑎))
1996, 19, 198eqfnfvd 7053 1 (𝜑𝐾 = 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 847   = wceq 1539  wcel 2107  wne 2939  wrex 3069  Vcvv 3479  wss 3950  c0 4332  ifcif 4524  {cpr 4627  cop 4631  cmpt 5224   I cid 5576   × cxp 5682  ran crn 5685  ccom 5688  Oncon0 6383   Fn wfn 6555  wf 6556  cfv 6560  (class class class)co 7432  cmpo 7434  1oc1o 8500  2oc2o 8501   Er wer 8743  [cec 8744   / cqs 8745  0cc0 11156  ..^cfzo 13695  chash 14370  Word cword 14553  ⟨“cs1 14634  Basecbs 17248   Σg cgsu 17486   /s cqus 17551   MndHom cmhm 18795  freeMndcfrmd 18861  varFMndcvrmd 18862  Grpcgrp 18952  invgcminusg 18953   GrpHom cghm 19231   ~FG cefg 19725  freeGrpcfrgp 19726  varFGrpcvrgp 19727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-ot 4634  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-er 8746  df-ec 8748  df-qs 8752  df-map 8869  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-sup 9483  df-inf 9484  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12529  df-xnn0 12602  df-z 12616  df-dec 12736  df-uz 12880  df-fz 13549  df-fzo 13696  df-seq 14044  df-hash 14371  df-word 14554  df-lsw 14602  df-concat 14610  df-s1 14635  df-substr 14680  df-pfx 14710  df-splice 14789  df-reverse 14798  df-s2 14888  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17249  df-ress 17276  df-plusg 17311  df-mulr 17312  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-0g 17487  df-gsum 17488  df-imas 17554  df-qus 17555  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-mhm 18797  df-submnd 18798  df-frmd 18863  df-vrmd 18864  df-grp 18955  df-minusg 18956  df-ghm 19232  df-efg 19728  df-frgp 19729  df-vrgp 19730
This theorem is referenced by:  frgpup3  19797
  Copyright terms: Public domain W3C validator