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

Theorem frgpup3lem 19809
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 19250 . . 3 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋𝐵)
5 ffn 6736 . . 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 19807 . . 3 (𝜑𝐸 ∈ (𝐺 GrpHom 𝐻))
172, 3ghmf 19250 . . 3 (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋𝐵)
18 ffn 6736 . . 3 (𝐸:𝑋𝐵𝐸 Fn 𝑋)
1916, 17, 183syl 18 . 2 (𝜑𝐸 Fn 𝑋)
20 eqid 2734 . . . . . . . . 9 (freeMnd‘(𝐼 × 2o)) = (freeMnd‘(𝐼 × 2o))
2114, 20, 13frgpval 19790 . . . . . . . 8 (𝐼𝑉𝐺 = ((freeMnd‘(𝐼 × 2o)) /s ))
2210, 21syl 17 . . . . . . 7 (𝜑𝐺 = ((freeMnd‘(𝐼 × 2o)) /s ))
23 2on 8518 . . . . . . . . . . 11 2o ∈ On
24 xpexg 7768 . . . . . . . . . . 11 ((𝐼𝑉 ∧ 2o ∈ On) → (𝐼 × 2o) ∈ V)
2510, 23, 24sylancl 586 . . . . . . . . . 10 (𝜑 → (𝐼 × 2o) ∈ V)
26 wrdexg 14558 . . . . . . . . . 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 2786 . . . . . . . 8 (𝜑𝑊 = Word (𝐼 × 2o))
30 eqid 2734 . . . . . . . . . 10 (Base‘(freeMnd‘(𝐼 × 2o))) = (Base‘(freeMnd‘(𝐼 × 2o)))
3120, 30frmdbas 18877 . . . . . . . . 9 ((𝐼 × 2o) ∈ V → (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o))
3225, 31syl 17 . . . . . . . 8 (𝜑 → (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o))
3329, 32eqtr4d 2777 . . . . . . 7 (𝜑𝑊 = (Base‘(freeMnd‘(𝐼 × 2o))))
3413fvexi 6920 . . . . . . . 8 ∈ V
3534a1i 11 . . . . . . 7 (𝜑 ∈ V)
36 fvexd 6921 . . . . . . 7 (𝜑 → (freeMnd‘(𝐼 × 2o)) ∈ V)
3722, 33, 35, 36qusbas 17591 . . . . . 6 (𝜑 → (𝑊 / ) = (Base‘𝐺))
382, 37eqtr4id 2793 . . . . 5 (𝜑𝑋 = (𝑊 / ))
39 eqimss 4053 . . . . 5 (𝑋 = (𝑊 / ) → 𝑋 ⊆ (𝑊 / ))
4038, 39syl 17 . . . 4 (𝜑𝑋 ⊆ (𝑊 / ))
4140sselda 3994 . . 3 ((𝜑𝑎𝑋) → 𝑎 ∈ (𝑊 / ))
42 eqid 2734 . . . 4 (𝑊 / ) = (𝑊 / )
43 fveq2 6906 . . . . 5 ([𝑡] = 𝑎 → (𝐾‘[𝑡] ) = (𝐾𝑎))
44 fveq2 6906 . . . . 5 ([𝑡] = 𝑎 → (𝐸‘[𝑡] ) = (𝐸𝑎))
4543, 44eqeq12d 2750 . . . 4 ([𝑡] = 𝑎 → ((𝐾‘[𝑡] ) = (𝐸‘[𝑡] ) ↔ (𝐾𝑎) = (𝐸𝑎)))
46 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑡𝑊)
4729adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑊 = Word (𝐼 × 2o))
4846, 47eleqtrd 2840 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝑡 ∈ Word (𝐼 × 2o))
49 wrdf 14553 . . . . . . . . . . . . 13 (𝑡 ∈ Word (𝐼 × 2o) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o))
5048, 49syl 17 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o))
5150ffvelcdmda 7103 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑡𝑛) ∈ (𝐼 × 2o))
52 elxp2 5712 . . . . . . . . . . 11 ((𝑡𝑛) ∈ (𝐼 × 2o) ↔ ∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
5351, 52sylib 218 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
54 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝐹𝑦) = (𝐹𝑖))
5554fveq2d 6910 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝑁‘(𝐹𝑦)) = (𝑁‘(𝐹𝑖)))
5654, 55ifeq12d 4551 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))) = if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
57 eqeq1 2738 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅))
5857ifbid 4553 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
59 fvex 6919 . . . . . . . . . . . . . . . . 17 (𝐹𝑖) ∈ V
60 fvex 6919 . . . . . . . . . . . . . . . . 17 (𝑁‘(𝐹𝑖)) ∈ V
6159, 60ifex 4580 . . . . . . . . . . . . . . . 16 if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) ∈ V
6256, 58, 8, 61ovmpo 7592 . . . . . . . . . . . . . . 15 ((𝑖𝐼𝑗 ∈ 2o) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
6362adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
64 elpri 4653 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {∅, 1o} → (𝑗 = ∅ ∨ 𝑗 = 1o))
65 df2o3 8512 . . . . . . . . . . . . . . . . 17 2o = {∅, 1o}
6664, 65eleq2s 2856 . . . . . . . . . . . . . . . 16 (𝑗 ∈ 2o → (𝑗 = ∅ ∨ 𝑗 = 1o))
67 frgpup3.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝑈) = 𝐹)
6867adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝐾𝑈) = 𝐹)
6968fveq1d 6908 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐹𝑖))
70 frgpup.u . . . . . . . . . . . . . . . . . . . . . . 23 𝑈 = (varFGrp𝐼)
7113, 70, 14, 2vrgpf 19800 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝑉𝑈:𝐼𝑋)
7210, 71syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:𝐼𝑋)
73 fvco3 7007 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈:𝐼𝑋𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7472, 73sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7569, 74eqtr3d 2776 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
7675adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
77 iftrue 4536 . . . . . . . . . . . . . . . . . . 19 (𝑗 = ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
7877adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
79 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅)
8079opeq2d 4884 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, ∅⟩)
8180s1eqd 14635 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, ∅⟩”⟩)
8281eceq1d 8783 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, ∅⟩”⟩] )
8313, 70vrgpval 19799 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8410, 83sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8584adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8682, 85eqtr4d 2777 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = (𝑈𝑖))
8786fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘(𝑈𝑖)))
8876, 78, 873eqtr4d 2784 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
8975fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝑁‘(𝐾‘(𝑈𝑖))))
9072ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) ∈ 𝑋)
91 eqid 2734 . . . . . . . . . . . . . . . . . . . . . 22 (invg𝐺) = (invg𝐺)
922, 91, 7ghminv 19253 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈𝑖) ∈ 𝑋) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
931, 90, 92syl2an2r 685 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9489, 93eqtr4d 2777 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
9594adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
96 1n0 8524 . . . . . . . . . . . . . . . . . . . 20 1o ≠ ∅
97 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → 𝑗 = 1o)
9897neeq1d 2997 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝑗 ≠ ∅ ↔ 1o ≠ ∅))
9996, 98mpbiri 258 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → 𝑗 ≠ ∅)
100 ifnefalse 4542 . . . . . . . . . . . . . . . . . . 19 (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10199, 100syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10297opeq2d 4884 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, 1o⟩)
103102s1eqd 14635 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, 1o⟩”⟩)
104103eceq1d 8783 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, 1o⟩”⟩] )
10513, 70, 14, 91vrgpinv 19801 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
10610, 105sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
107106adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
108104, 107eqtr4d 2777 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → [⟨“⟨𝑖, 𝑗⟩”⟩] = ((invg𝐺)‘(𝑈𝑖)))
109108fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
11095, 101, 1093eqtr4d 2784 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11188, 110jaodan 959 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1o)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11266, 111sylan2 593 . . . . . . . . . . . . . . 15 (((𝜑𝑖𝐼) ∧ 𝑗 ∈ 2o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
113112anasss 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11463, 113eqtrd 2774 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
115 fveq2 6906 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑇‘⟨𝑖, 𝑗⟩))
116 df-ov 7433 . . . . . . . . . . . . . . 15 (𝑖𝑇𝑗) = (𝑇‘⟨𝑖, 𝑗⟩)
117115, 116eqtr4di 2792 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑖𝑇𝑗))
118 s1eq 14634 . . . . . . . . . . . . . . . 16 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ⟨“(𝑡𝑛)”⟩ = ⟨“⟨𝑖, 𝑗⟩”⟩)
119118eceq1d 8783 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → [⟨“(𝑡𝑛)”⟩] = [⟨“⟨𝑖, 𝑗⟩”⟩] )
120119fveq2d 6910 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝐾‘[⟨“(𝑡𝑛)”⟩] ) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
121117, 120eqeq12d 2750 . . . . . . . . . . . . 13 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ((𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ) ↔ (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] )))
122114, 121syl5ibrcom 247 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
123122rexlimdvva 3210 . . . . . . . . . . 11 (𝜑 → (∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
124123ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
12553, 124mpd 15 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
126125mpteq2dva 5247 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
1273, 7, 8, 9, 10, 11frgpuptf 19802 . . . . . . . . 9 (𝜑𝑇:(𝐼 × 2o)⟶𝐵)
128 fcompt 7152 . . . . . . . . 9 ((𝑇:(𝐼 × 2o)⟶𝐵𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o)) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
129127, 50, 128syl2an2r 685 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
13051s1cld 14637 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ Word (𝐼 × 2o))
13129ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → 𝑊 = Word (𝐼 × 2o))
132130, 131eleqtrrd 2841 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ 𝑊)
13314, 13, 12, 2frgpeccl 19793 . . . . . . . . . 10 (⟨“(𝑡𝑛)”⟩ ∈ 𝑊 → [⟨“(𝑡𝑛)”⟩] 𝑋)
134132, 133syl 17 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → [⟨“(𝑡𝑛)”⟩] 𝑋)
13550feqmptd 6976 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝑡 = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑡𝑛)))
13610adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝐼𝑉)
137136, 23, 24sylancl 586 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → (𝐼 × 2o) ∈ V)
138 eqid 2734 . . . . . . . . . . . . 13 (varFMnd‘(𝐼 × 2o)) = (varFMnd‘(𝐼 × 2o))
139138vrmdfval 18881 . . . . . . . . . . . 12 ((𝐼 × 2o) ∈ V → (varFMnd‘(𝐼 × 2o)) = (𝑤 ∈ (𝐼 × 2o) ↦ ⟨“𝑤”⟩))
140137, 139syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)) = (𝑤 ∈ (𝐼 × 2o) ↦ ⟨“𝑤”⟩))
141 s1eq 14634 . . . . . . . . . . 11 (𝑤 = (𝑡𝑛) → ⟨“𝑤”⟩ = ⟨“(𝑡𝑛)”⟩)
14251, 135, 140, 141fmptco 7148 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ ⟨“(𝑡𝑛)”⟩))
143 eqidd 2735 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] ))
144 eceq1 8782 . . . . . . . . . 10 (𝑤 = ⟨“(𝑡𝑛)”⟩ → [𝑤] = [⟨“(𝑡𝑛)”⟩] )
145132, 142, 143, 144fmptco 7148 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ [⟨“(𝑡𝑛)”⟩] ))
1461adantr 480 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
147146, 4syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → 𝐾:𝑋𝐵)
148147feqmptd 6976 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝐾 = (𝑤𝑋 ↦ (𝐾𝑤)))
149 fveq2 6906 . . . . . . . . 9 (𝑤 = [⟨“(𝑡𝑛)”⟩] → (𝐾𝑤) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
150134, 145, 148, 149fmptco 7148 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
151126, 129, 1503eqtr4d 2784 . . . . . . 7 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))
152151oveq2d 7446 . . . . . 6 ((𝜑𝑡𝑊) → (𝐻 Σg (𝑇𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
1533, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpupval 19806 . . . . . 6 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐻 Σg (𝑇𝑡)))
154 ghmmhm 19256 . . . . . . . 8 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻))
155146, 154syl 17 . . . . . . 7 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻))
156138vrmdf 18883 . . . . . . . . . . 11 ((𝐼 × 2o) ∈ V → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o))
157137, 156syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o))
15847feq3d 6723 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊 ↔ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o)))
159157, 158mpbird 257 . . . . . . . . 9 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊)
160 wrdco 14866 . . . . . . . . 9 ((𝑡 ∈ Word (𝐼 × 2o) ∧ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊)
16148, 159, 160syl2anc 584 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊)
16233adantr 480 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 × 2o))))
163162mpteq1d 5242 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ))
164 eqid 2734 . . . . . . . . . . . . 13 (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] )
16520, 30, 14, 13, 164frgpmhm 19797 . . . . . . . . . . . 12 (𝐼𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
166136, 165syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
167163, 166eqeltrd 2838 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
16830, 2mhmf 18814 . . . . . . . . . 10 ((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋)
169167, 168syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋)
170162feq2d 6722 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ):𝑊𝑋 ↔ (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋))
171169, 170mpbird 257 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋)
172 wrdco 14866 . . . . . . . 8 ((((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊 ∧ (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋)
173161, 171, 172syl2anc 584 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋)
1742gsumwmhm 18870 . . . . . . 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 2784 . . . . 5 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
17720, 138frmdgsum 18887 . . . . . . . . 9 (((𝐼 × 2o) ∈ V ∧ 𝑡 ∈ Word (𝐼 × 2o)) → ((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = 𝑡)
17825, 48, 177syl2an2r 685 . . . . . . . 8 ((𝜑𝑡𝑊) → ((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = 𝑡)
179178fveq2d 6910 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = ((𝑤𝑊 ↦ [𝑤] )‘𝑡))
180 wrdco 14866 . . . . . . . . . 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 14570 . . . . . . . . . 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 2841 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2o))))
18630gsumwmhm 18870 . . . . . . . 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 19750 . . . . . . . . 9 Er 𝑊
189188a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → Er 𝑊)
19012fvexi 6920 . . . . . . . . 9 𝑊 ∈ V
191190a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → 𝑊 ∈ V)
192 eqid 2734 . . . . . . . 8 (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] )
193189, 191, 192divsfval 17593 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘𝑡) = [𝑡] )
194179, 187, 1933eqtr3d 2782 . . . . . 6 ((𝜑𝑡𝑊) → (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = [𝑡] )
195194fveq2d 6910 . . . . 5 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐾‘[𝑡] ))
196176, 195eqtr2d 2775 . . . 4 ((𝜑𝑡𝑊) → (𝐾‘[𝑡] ) = (𝐸‘[𝑡] ))
19742, 45, 196ectocld 8822 . . 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 1536  wcel 2105  wne 2937  wrex 3067  Vcvv 3477  wss 3962  c0 4338  ifcif 4530  {cpr 4632  cop 4636  cmpt 5230   I cid 5581   × cxp 5686  ran crn 5689  ccom 5692  Oncon0 6385   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  cmpo 7432  1oc1o 8497  2oc2o 8498   Er wer 8740  [cec 8741   / cqs 8742  0cc0 11152  ..^cfzo 13690  chash 14365  Word cword 14548  ⟨“cs1 14629  Basecbs 17244   Σg cgsu 17486   /s cqus 17551   MndHom cmhm 18806  freeMndcfrmd 18872  varFMndcvrmd 18873  Grpcgrp 18963  invgcminusg 18964   GrpHom cghm 19242   ~FG cefg 19738  freeGrpcfrgp 19739  varFGrpcvrgp 19740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-ot 4639  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-ec 8745  df-qs 8749  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-xnn0 12597  df-z 12611  df-dec 12731  df-uz 12876  df-fz 13544  df-fzo 13691  df-seq 14039  df-hash 14366  df-word 14549  df-lsw 14597  df-concat 14605  df-s1 14630  df-substr 14675  df-pfx 14705  df-splice 14784  df-reverse 14793  df-s2 14883  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-0g 17487  df-gsum 17488  df-imas 17554  df-qus 17555  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-frmd 18874  df-vrmd 18875  df-grp 18966  df-minusg 18967  df-ghm 19243  df-efg 19741  df-frgp 19742  df-vrgp 19743
This theorem is referenced by:  frgpup3  19810
  Copyright terms: Public domain W3C validator