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

Theorem frgpup3lem 18903
 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 18362 . . 3 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋𝐵)
5 ffn 6503 . . 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 18901 . . 3 (𝜑𝐸 ∈ (𝐺 GrpHom 𝐻))
172, 3ghmf 18362 . . 3 (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋𝐵)
18 ffn 6503 . . 3 (𝐸:𝑋𝐵𝐸 Fn 𝑋)
1916, 17, 183syl 18 . 2 (𝜑𝐸 Fn 𝑋)
20 eqid 2824 . . . . . . . . 9 (freeMnd‘(𝐼 × 2o)) = (freeMnd‘(𝐼 × 2o))
2114, 20, 13frgpval 18884 . . . . . . . 8 (𝐼𝑉𝐺 = ((freeMnd‘(𝐼 × 2o)) /s ))
2210, 21syl 17 . . . . . . 7 (𝜑𝐺 = ((freeMnd‘(𝐼 × 2o)) /s ))
23 2on 8107 . . . . . . . . . . 11 2o ∈ On
24 xpexg 7467 . . . . . . . . . . 11 ((𝐼𝑉 ∧ 2o ∈ On) → (𝐼 × 2o) ∈ V)
2510, 23, 24sylancl 589 . . . . . . . . . 10 (𝜑 → (𝐼 × 2o) ∈ V)
26 wrdexg 13876 . . . . . . . . . 10 ((𝐼 × 2o) ∈ V → Word (𝐼 × 2o) ∈ V)
27 fvi 6731 . . . . . . . . . 10 (Word (𝐼 × 2o) ∈ V → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 × 2o))
2825, 26, 273syl 18 . . . . . . . . 9 (𝜑 → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 × 2o))
2912, 28syl5eq 2871 . . . . . . . 8 (𝜑𝑊 = Word (𝐼 × 2o))
30 eqid 2824 . . . . . . . . . 10 (Base‘(freeMnd‘(𝐼 × 2o))) = (Base‘(freeMnd‘(𝐼 × 2o)))
3120, 30frmdbas 18017 . . . . . . . . 9 ((𝐼 × 2o) ∈ V → (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o))
3225, 31syl 17 . . . . . . . 8 (𝜑 → (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o))
3329, 32eqtr4d 2862 . . . . . . 7 (𝜑𝑊 = (Base‘(freeMnd‘(𝐼 × 2o))))
3413fvexi 6675 . . . . . . . 8 ∈ V
3534a1i 11 . . . . . . 7 (𝜑 ∈ V)
36 fvexd 6676 . . . . . . 7 (𝜑 → (freeMnd‘(𝐼 × 2o)) ∈ V)
3722, 33, 35, 36qusbas 16818 . . . . . 6 (𝜑 → (𝑊 / ) = (Base‘𝐺))
3837, 2syl6reqr 2878 . . . . 5 (𝜑𝑋 = (𝑊 / ))
39 eqimss 4009 . . . . 5 (𝑋 = (𝑊 / ) → 𝑋 ⊆ (𝑊 / ))
4038, 39syl 17 . . . 4 (𝜑𝑋 ⊆ (𝑊 / ))
4140sselda 3953 . . 3 ((𝜑𝑎𝑋) → 𝑎 ∈ (𝑊 / ))
42 eqid 2824 . . . 4 (𝑊 / ) = (𝑊 / )
43 fveq2 6661 . . . . 5 ([𝑡] = 𝑎 → (𝐾‘[𝑡] ) = (𝐾𝑎))
44 fveq2 6661 . . . . 5 ([𝑡] = 𝑎 → (𝐸‘[𝑡] ) = (𝐸𝑎))
4543, 44eqeq12d 2840 . . . 4 ([𝑡] = 𝑎 → ((𝐾‘[𝑡] ) = (𝐸‘[𝑡] ) ↔ (𝐾𝑎) = (𝐸𝑎)))
46 simpr 488 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑡𝑊)
4729adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑊 = Word (𝐼 × 2o))
4846, 47eleqtrd 2918 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝑡 ∈ Word (𝐼 × 2o))
49 wrdf 13871 . . . . . . . . . . . . 13 (𝑡 ∈ Word (𝐼 × 2o) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o))
5048, 49syl 17 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o))
5150ffvelrnda 6842 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑡𝑛) ∈ (𝐼 × 2o))
52 elxp2 5566 . . . . . . . . . . 11 ((𝑡𝑛) ∈ (𝐼 × 2o) ↔ ∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
5351, 52sylib 221 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
54 fveq2 6661 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝐹𝑦) = (𝐹𝑖))
5554fveq2d 6665 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝑁‘(𝐹𝑦)) = (𝑁‘(𝐹𝑖)))
5654, 55ifeq12d 4470 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))) = if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
57 eqeq1 2828 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅))
5857ifbid 4472 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
59 fvex 6674 . . . . . . . . . . . . . . . . 17 (𝐹𝑖) ∈ V
60 fvex 6674 . . . . . . . . . . . . . . . . 17 (𝑁‘(𝐹𝑖)) ∈ V
6159, 60ifex 4498 . . . . . . . . . . . . . . . 16 if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) ∈ V
6256, 58, 8, 61ovmpo 7303 . . . . . . . . . . . . . . 15 ((𝑖𝐼𝑗 ∈ 2o) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
6362adantl 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
64 elpri 4572 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {∅, 1o} → (𝑗 = ∅ ∨ 𝑗 = 1o))
65 df2o3 8113 . . . . . . . . . . . . . . . . 17 2o = {∅, 1o}
6664, 65eleq2s 2934 . . . . . . . . . . . . . . . 16 (𝑗 ∈ 2o → (𝑗 = ∅ ∨ 𝑗 = 1o))
67 frgpup3.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝑈) = 𝐹)
6867adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝐾𝑈) = 𝐹)
6968fveq1d 6663 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐹𝑖))
70 frgpup.u . . . . . . . . . . . . . . . . . . . . . . 23 𝑈 = (varFGrp𝐼)
7113, 70, 14, 2vrgpf 18894 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝑉𝑈:𝐼𝑋)
7210, 71syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:𝐼𝑋)
73 fvco3 6751 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈:𝐼𝑋𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7472, 73sylan 583 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7569, 74eqtr3d 2861 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
7675adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
77 iftrue 4456 . . . . . . . . . . . . . . . . . . 19 (𝑗 = ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
7877adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
79 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅)
8079opeq2d 4796 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, ∅⟩)
8180s1eqd 13955 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, ∅⟩”⟩)
8281eceq1d 8324 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, ∅⟩”⟩] )
8313, 70vrgpval 18893 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8410, 83sylan 583 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8584adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8682, 85eqtr4d 2862 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = (𝑈𝑖))
8786fveq2d 6665 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘(𝑈𝑖)))
8876, 78, 873eqtr4d 2869 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
8975fveq2d 6665 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝑁‘(𝐾‘(𝑈𝑖))))
9072ffvelrnda 6842 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) ∈ 𝑋)
91 eqid 2824 . . . . . . . . . . . . . . . . . . . . . 22 (invg𝐺) = (invg𝐺)
922, 91, 7ghminv 18365 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈𝑖) ∈ 𝑋) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
931, 90, 92syl2an2r 684 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9489, 93eqtr4d 2862 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
9594adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
96 1n0 8115 . . . . . . . . . . . . . . . . . . . 20 1o ≠ ∅
97 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → 𝑗 = 1o)
9897neeq1d 3073 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝑗 ≠ ∅ ↔ 1o ≠ ∅))
9996, 98mpbiri 261 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → 𝑗 ≠ ∅)
100 ifnefalse 4462 . . . . . . . . . . . . . . . . . . 19 (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10199, 100syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
10297opeq2d 4796 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, 1o⟩)
103102s1eqd 13955 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, 1o⟩”⟩)
104103eceq1d 8324 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, 1o⟩”⟩] )
10513, 70, 14, 91vrgpinv 18895 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
10610, 105sylan 583 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
107106adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1o⟩”⟩] )
108104, 107eqtr4d 2862 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → [⟨“⟨𝑖, 𝑗⟩”⟩] = ((invg𝐺)‘(𝑈𝑖)))
109108fveq2d 6665 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
11095, 101, 1093eqtr4d 2869 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = 1o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11188, 110jaodan 955 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1o)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11266, 111sylan2 595 . . . . . . . . . . . . . . 15 (((𝜑𝑖𝐼) ∧ 𝑗 ∈ 2o) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
113112anasss 470 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11463, 113eqtrd 2859 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
115 fveq2 6661 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑇‘⟨𝑖, 𝑗⟩))
116 df-ov 7152 . . . . . . . . . . . . . . 15 (𝑖𝑇𝑗) = (𝑇‘⟨𝑖, 𝑗⟩)
117115, 116syl6eqr 2877 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑖𝑇𝑗))
118 s1eq 13954 . . . . . . . . . . . . . . . 16 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ⟨“(𝑡𝑛)”⟩ = ⟨“⟨𝑖, 𝑗⟩”⟩)
119118eceq1d 8324 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → [⟨“(𝑡𝑛)”⟩] = [⟨“⟨𝑖, 𝑗⟩”⟩] )
120119fveq2d 6665 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝐾‘[⟨“(𝑡𝑛)”⟩] ) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
121117, 120eqeq12d 2840 . . . . . . . . . . . . 13 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ((𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ) ↔ (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] )))
122114, 121syl5ibrcom 250 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2o)) → ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
123122rexlimdvva 3286 . . . . . . . . . . 11 (𝜑 → (∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
124123ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (∃𝑖𝐼𝑗 ∈ 2o (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
12553, 124mpd 15 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
126125mpteq2dva 5147 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
1273, 7, 8, 9, 10, 11frgpuptf 18896 . . . . . . . . 9 (𝜑𝑇:(𝐼 × 2o)⟶𝐵)
128 fcompt 6886 . . . . . . . . 9 ((𝑇:(𝐼 × 2o)⟶𝐵𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o)) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
129127, 50, 128syl2an2r 684 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
13051s1cld 13957 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ Word (𝐼 × 2o))
13129ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → 𝑊 = Word (𝐼 × 2o))
132130, 131eleqtrrd 2919 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ 𝑊)
13314, 13, 12, 2frgpeccl 18887 . . . . . . . . . 10 (⟨“(𝑡𝑛)”⟩ ∈ 𝑊 → [⟨“(𝑡𝑛)”⟩] 𝑋)
134132, 133syl 17 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → [⟨“(𝑡𝑛)”⟩] 𝑋)
13550feqmptd 6724 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝑡 = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑡𝑛)))
13610adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝐼𝑉)
137136, 23, 24sylancl 589 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → (𝐼 × 2o) ∈ V)
138 eqid 2824 . . . . . . . . . . . . 13 (varFMnd‘(𝐼 × 2o)) = (varFMnd‘(𝐼 × 2o))
139138vrmdfval 18021 . . . . . . . . . . . 12 ((𝐼 × 2o) ∈ V → (varFMnd‘(𝐼 × 2o)) = (𝑤 ∈ (𝐼 × 2o) ↦ ⟨“𝑤”⟩))
140137, 139syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)) = (𝑤 ∈ (𝐼 × 2o) ↦ ⟨“𝑤”⟩))
141 s1eq 13954 . . . . . . . . . . 11 (𝑤 = (𝑡𝑛) → ⟨“𝑤”⟩ = ⟨“(𝑡𝑛)”⟩)
14251, 135, 140, 141fmptco 6882 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ ⟨“(𝑡𝑛)”⟩))
143 eqidd 2825 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] ))
144 eceq1 8323 . . . . . . . . . 10 (𝑤 = ⟨“(𝑡𝑛)”⟩ → [𝑤] = [⟨“(𝑡𝑛)”⟩] )
145132, 142, 143, 144fmptco 6882 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ [⟨“(𝑡𝑛)”⟩] ))
1461adantr 484 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
147146, 4syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → 𝐾:𝑋𝐵)
148147feqmptd 6724 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝐾 = (𝑤𝑋 ↦ (𝐾𝑤)))
149 fveq2 6661 . . . . . . . . 9 (𝑤 = [⟨“(𝑡𝑛)”⟩] → (𝐾𝑤) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
150134, 145, 148, 149fmptco 6882 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
151126, 129, 1503eqtr4d 2869 . . . . . . 7 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))
152151oveq2d 7165 . . . . . 6 ((𝜑𝑡𝑊) → (𝐻 Σg (𝑇𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
1533, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpupval 18900 . . . . . 6 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐻 Σg (𝑇𝑡)))
154 ghmmhm 18368 . . . . . . . 8 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻))
155146, 154syl 17 . . . . . . 7 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻))
156138vrmdf 18023 . . . . . . . . . . 11 ((𝐼 × 2o) ∈ V → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o))
157137, 156syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o))
15847feq3d 6490 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊 ↔ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o)))
159157, 158mpbird 260 . . . . . . . . 9 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊)
160 wrdco 14193 . . . . . . . . 9 ((𝑡 ∈ Word (𝐼 × 2o) ∧ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊)
16148, 159, 160syl2anc 587 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊)
16233adantr 484 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 × 2o))))
163162mpteq1d 5141 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ))
164 eqid 2824 . . . . . . . . . . . . 13 (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] )
16520, 30, 14, 13, 164frgpmhm 18891 . . . . . . . . . . . 12 (𝐼𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
166136, 165syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
167163, 166eqeltrd 2916 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺))
16830, 2mhmf 17961 . . . . . . . . . 10 ((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋)
169167, 168syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋)
170162feq2d 6489 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ):𝑊𝑋 ↔ (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋))
171169, 170mpbird 260 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋)
172 wrdco 14193 . . . . . . . 8 ((((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊 ∧ (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋)
173161, 171, 172syl2anc 587 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋)
1742gsumwmhm 18010 . . . . . . 7 ((𝐾 ∈ (𝐺 MndHom 𝐻) ∧ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
175155, 173, 174syl2anc 587 . . . . . 6 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
176152, 153, 1753eqtr4d 2869 . . . . 5 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))))
17720, 138frmdgsum 18027 . . . . . . . . 9 (((𝐼 × 2o) ∈ V ∧ 𝑡 ∈ Word (𝐼 × 2o)) → ((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = 𝑡)
17825, 48, 177syl2an2r 684 . . . . . . . 8 ((𝜑𝑡𝑊) → ((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = 𝑡)
179178fveq2d 6665 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = ((𝑤𝑊 ↦ [𝑤] )‘𝑡))
180 wrdco 14193 . . . . . . . . . 10 ((𝑡 ∈ Word (𝐼 × 2o) ∧ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o)) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word Word (𝐼 × 2o))
18148, 157, 180syl2anc 587 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word Word (𝐼 × 2o))
18232adantr 484 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o))
183 wrdeq 13888 . . . . . . . . . 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 2919 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2o))))
18630gsumwmhm 18010 . . . . . . . 8 (((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2o)) MndHom 𝐺) ∧ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2o)))) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))
187167, 185, 186syl2anc 587 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2o)) Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))
18812, 13efger 18844 . . . . . . . . 9 Er 𝑊
189188a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → Er 𝑊)
19012fvexi 6675 . . . . . . . . 9 𝑊 ∈ V
191190a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → 𝑊 ∈ V)
192 eqid 2824 . . . . . . . 8 (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] )
193189, 191, 192divsfval 16820 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘𝑡) = [𝑡] )
194179, 187, 1933eqtr3d 2867 . . . . . 6 ((𝜑𝑡𝑊) → (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = [𝑡] )
195194fveq2d 6665 . . . . 5 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐾‘[𝑡] ))
196176, 195eqtr2d 2860 . . . 4 ((𝜑𝑡𝑊) → (𝐾‘[𝑡] ) = (𝐸‘[𝑡] ))
19742, 45, 196ectocld 8360 . . 3 ((𝜑𝑎 ∈ (𝑊 / )) → (𝐾𝑎) = (𝐸𝑎))
19841, 197syldan 594 . 2 ((𝜑𝑎𝑋) → (𝐾𝑎) = (𝐸𝑎))
1996, 19, 198eqfnfvd 6796 1 (𝜑𝐾 = 𝐸)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∃wrex 3134  Vcvv 3480   ⊆ wss 3919  ∅c0 4276  ifcif 4450  {cpr 4552  ⟨cop 4556   ↦ cmpt 5132   I cid 5446   × cxp 5540  ran crn 5543   ∘ ccom 5546  Oncon0 6178   Fn wfn 6338  ⟶wf 6339  ‘cfv 6343  (class class class)co 7149   ∈ cmpo 7151  1oc1o 8091  2oc2o 8092   Er wer 8282  [cec 8283   / cqs 8284  0cc0 10535  ..^cfzo 13037  ♯chash 13695  Word cword 13866  ⟨“cs1 13949  Basecbs 16483   Σg cgsu 16714   /s cqus 16778   MndHom cmhm 17954  freeMndcfrmd 18012  varFMndcvrmd 18013  Grpcgrp 18103  invgcminusg 18104   GrpHom cghm 18355   ~FG cefg 18832  freeGrpcfrgp 18833  varFGrpcvrgp 18834 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-ot 4559  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-ec 8287  df-qs 8291  df-map 8404  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-sup 8903  df-inf 8904  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-xnn0 11965  df-z 11979  df-dec 12096  df-uz 12241  df-fz 12895  df-fzo 13038  df-seq 13374  df-hash 13696  df-word 13867  df-lsw 13915  df-concat 13923  df-s1 13950  df-substr 14003  df-pfx 14033  df-splice 14112  df-reverse 14121  df-s2 14210  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-0g 16715  df-gsum 16716  df-imas 16781  df-qus 16782  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-mhm 17956  df-submnd 17957  df-frmd 18014  df-vrmd 18015  df-grp 18106  df-minusg 18107  df-ghm 18356  df-efg 18835  df-frgp 18836  df-vrgp 18837 This theorem is referenced by:  frgpup3  18904
 Copyright terms: Public domain W3C validator