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

Theorem frgpup3lem 18013
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 17487 . . 3 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋𝐵)
5 ffn 5958 . . 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 18011 . . 3 (𝜑𝐸 ∈ (𝐺 GrpHom 𝐻))
172, 3ghmf 17487 . . 3 (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋𝐵)
18 ffn 5958 . . 3 (𝐸:𝑋𝐵𝐸 Fn 𝑋)
1916, 17, 183syl 18 . 2 (𝜑𝐸 Fn 𝑋)
20 eqid 2610 . . . . . . . . 9 (freeMnd‘(𝐼 × 2𝑜)) = (freeMnd‘(𝐼 × 2𝑜))
2114, 20, 13frgpval 17994 . . . . . . . 8 (𝐼𝑉𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
2210, 21syl 17 . . . . . . 7 (𝜑𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
23 2on 7455 . . . . . . . . . . 11 2𝑜 ∈ On
24 xpexg 6858 . . . . . . . . . . 11 ((𝐼𝑉 ∧ 2𝑜 ∈ On) → (𝐼 × 2𝑜) ∈ V)
2510, 23, 24sylancl 693 . . . . . . . . . 10 (𝜑 → (𝐼 × 2𝑜) ∈ V)
26 wrdexg 13170 . . . . . . . . . 10 ((𝐼 × 2𝑜) ∈ V → Word (𝐼 × 2𝑜) ∈ V)
27 fvi 6165 . . . . . . . . . 10 (Word (𝐼 × 2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
2825, 26, 273syl 18 . . . . . . . . 9 (𝜑 → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
2912, 28syl5eq 2656 . . . . . . . 8 (𝜑𝑊 = Word (𝐼 × 2𝑜))
30 eqid 2610 . . . . . . . . . 10 (Base‘(freeMnd‘(𝐼 × 2𝑜))) = (Base‘(freeMnd‘(𝐼 × 2𝑜)))
3120, 30frmdbas 17212 . . . . . . . . 9 ((𝐼 × 2𝑜) ∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
3225, 31syl 17 . . . . . . . 8 (𝜑 → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
3329, 32eqtr4d 2647 . . . . . . 7 (𝜑𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
34 fvex 6113 . . . . . . . . 9 ( ~FG𝐼) ∈ V
3513, 34eqeltri 2684 . . . . . . . 8 ∈ V
3635a1i 11 . . . . . . 7 (𝜑 ∈ V)
37 fvex 6113 . . . . . . . 8 (freeMnd‘(𝐼 × 2𝑜)) ∈ V
3837a1i 11 . . . . . . 7 (𝜑 → (freeMnd‘(𝐼 × 2𝑜)) ∈ V)
3922, 33, 36, 38qusbas 16028 . . . . . 6 (𝜑 → (𝑊 / ) = (Base‘𝐺))
4039, 2syl6reqr 2663 . . . . 5 (𝜑𝑋 = (𝑊 / ))
41 eqimss 3620 . . . . 5 (𝑋 = (𝑊 / ) → 𝑋 ⊆ (𝑊 / ))
4240, 41syl 17 . . . 4 (𝜑𝑋 ⊆ (𝑊 / ))
4342sselda 3568 . . 3 ((𝜑𝑎𝑋) → 𝑎 ∈ (𝑊 / ))
44 eqid 2610 . . . 4 (𝑊 / ) = (𝑊 / )
45 fveq2 6103 . . . . 5 ([𝑡] = 𝑎 → (𝐾‘[𝑡] ) = (𝐾𝑎))
46 fveq2 6103 . . . . 5 ([𝑡] = 𝑎 → (𝐸‘[𝑡] ) = (𝐸𝑎))
4745, 46eqeq12d 2625 . . . 4 ([𝑡] = 𝑎 → ((𝐾‘[𝑡] ) = (𝐸‘[𝑡] ) ↔ (𝐾𝑎) = (𝐸𝑎)))
48 simpr 476 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑡𝑊)
4929adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑊) → 𝑊 = Word (𝐼 × 2𝑜))
5048, 49eleqtrd 2690 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝑡 ∈ Word (𝐼 × 2𝑜))
51 wrdf 13165 . . . . . . . . . . . . 13 (𝑡 ∈ Word (𝐼 × 2𝑜) → 𝑡:(0..^(#‘𝑡))⟶(𝐼 × 2𝑜))
5250, 51syl 17 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑡:(0..^(#‘𝑡))⟶(𝐼 × 2𝑜))
5352ffvelrnda 6267 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (𝑡𝑛) ∈ (𝐼 × 2𝑜))
54 elxp2 5056 . . . . . . . . . . 11 ((𝑡𝑛) ∈ (𝐼 × 2𝑜) ↔ ∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
5553, 54sylib 207 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → ∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩)
56 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝐹𝑦) = (𝐹𝑖))
5756fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑖 → (𝑁‘(𝐹𝑦)) = (𝑁‘(𝐹𝑖)))
5856, 57ifeq12d 4056 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))) = if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
59 eqeq1 2614 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅))
6059ifbid 4058 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
61 fvex 6113 . . . . . . . . . . . . . . . . 17 (𝐹𝑖) ∈ V
62 fvex 6113 . . . . . . . . . . . . . . . . 17 (𝑁‘(𝐹𝑖)) ∈ V
6361, 62ifex 4106 . . . . . . . . . . . . . . . 16 if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) ∈ V
6458, 60, 8, 63ovmpt2 6694 . . . . . . . . . . . . . . 15 ((𝑖𝐼𝑗 ∈ 2𝑜) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
6564adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))))
66 elpri 4145 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {∅, 1𝑜} → (𝑗 = ∅ ∨ 𝑗 = 1𝑜))
67 df2o3 7460 . . . . . . . . . . . . . . . . 17 2𝑜 = {∅, 1𝑜}
6866, 67eleq2s 2706 . . . . . . . . . . . . . . . 16 (𝑗 ∈ 2𝑜 → (𝑗 = ∅ ∨ 𝑗 = 1𝑜))
69 frgpup3.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝑈) = 𝐹)
7069adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝐾𝑈) = 𝐹)
7170fveq1d 6105 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐹𝑖))
72 frgpup.u . . . . . . . . . . . . . . . . . . . . . . 23 𝑈 = (varFGrp𝐼)
7313, 72, 14, 2vrgpf 18004 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝑉𝑈:𝐼𝑋)
7410, 73syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:𝐼𝑋)
75 fvco3 6185 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈:𝐼𝑋𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7674, 75sylan 487 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → ((𝐾𝑈)‘𝑖) = (𝐾‘(𝑈𝑖)))
7771, 76eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
7877adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐹𝑖) = (𝐾‘(𝑈𝑖)))
79 iftrue 4042 . . . . . . . . . . . . . . . . . . 19 (𝑗 = ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
8079adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐹𝑖))
81 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅)
8281opeq2d 4347 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, ∅⟩)
8382s1eqd 13234 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, ∅⟩”⟩)
8483eceq1d 7670 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, ∅⟩”⟩] )
8513, 72vrgpval 18003 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8610, 85sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8786adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝑈𝑖) = [⟨“⟨𝑖, ∅⟩”⟩] )
8884, 87eqtr4d 2647 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → [⟨“⟨𝑖, 𝑗⟩”⟩] = (𝑈𝑖))
8988fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘(𝑈𝑖)))
9078, 80, 893eqtr4d 2654 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
9177fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝑁‘(𝐾‘(𝑈𝑖))))
921adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
9374ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (𝑈𝑖) ∈ 𝑋)
94 eqid 2610 . . . . . . . . . . . . . . . . . . . . . 22 (invg𝐺) = (invg𝐺)
952, 94, 7ghminv 17490 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈𝑖) ∈ 𝑋) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9692, 93, 95syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (𝐾‘((invg𝐺)‘(𝑈𝑖))) = (𝑁‘(𝐾‘(𝑈𝑖))))
9791, 96eqtr4d 2647 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
9897adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝑁‘(𝐹𝑖)) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
99 1n0 7462 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ≠ ∅
100 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 = 1𝑜)
101100neeq1d 2841 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝑗 ≠ ∅ ↔ 1𝑜 ≠ ∅))
10299, 101mpbiri 247 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 ≠ ∅)
103 ifnefalse 4048 . . . . . . . . . . . . . . . . . . 19 (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
104102, 103syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝑁‘(𝐹𝑖)))
105100opeq2d 4347 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ⟨𝑖, 𝑗⟩ = ⟨𝑖, 1𝑜⟩)
106105s1eqd 13234 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ⟨“⟨𝑖, 𝑗⟩”⟩ = ⟨“⟨𝑖, 1𝑜⟩”⟩)
107106eceq1d 7670 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → [⟨“⟨𝑖, 𝑗⟩”⟩] = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
10813, 72, 14, 94vrgpinv 18005 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼𝑉𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
10910, 108sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
110109adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → ((invg𝐺)‘(𝑈𝑖)) = [⟨“⟨𝑖, 1𝑜⟩”⟩] )
111107, 110eqtr4d 2647 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → [⟨“⟨𝑖, 𝑗⟩”⟩] = ((invg𝐺)‘(𝑈𝑖)))
112111fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ) = (𝐾‘((invg𝐺)‘(𝑈𝑖))))
11398, 104, 1123eqtr4d 2654 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11490, 113jaodan 822 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1𝑜)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11568, 114sylan2 490 . . . . . . . . . . . . . . 15 (((𝜑𝑖𝐼) ∧ 𝑗 ∈ 2𝑜) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
116115anasss 677 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → if(𝑗 = ∅, (𝐹𝑖), (𝑁‘(𝐹𝑖))) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
11765, 116eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
118 fveq2 6103 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑇‘⟨𝑖, 𝑗⟩))
119 df-ov 6552 . . . . . . . . . . . . . . 15 (𝑖𝑇𝑗) = (𝑇‘⟨𝑖, 𝑗⟩)
120118, 119syl6eqr 2662 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝑖𝑇𝑗))
121 s1eq 13233 . . . . . . . . . . . . . . . 16 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ⟨“(𝑡𝑛)”⟩ = ⟨“⟨𝑖, 𝑗⟩”⟩)
122121eceq1d 7670 . . . . . . . . . . . . . . 15 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → [⟨“(𝑡𝑛)”⟩] = [⟨“⟨𝑖, 𝑗⟩”⟩] )
123122fveq2d 6107 . . . . . . . . . . . . . 14 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝐾‘[⟨“(𝑡𝑛)”⟩] ) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] ))
124120, 123eqeq12d 2625 . . . . . . . . . . . . 13 ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → ((𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ) ↔ (𝑖𝑇𝑗) = (𝐾‘[⟨“⟨𝑖, 𝑗⟩”⟩] )))
125117, 124syl5ibrcom 236 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝐼𝑗 ∈ 2𝑜)) → ((𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
126125rexlimdvva 3020 . . . . . . . . . . 11 (𝜑 → (∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
127126ad2antrr 758 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (∃𝑖𝐼𝑗 ∈ 2𝑜 (𝑡𝑛) = ⟨𝑖, 𝑗⟩ → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
12855, 127mpd 15 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (𝑇‘(𝑡𝑛)) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
129128mpteq2dva 4672 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡𝑛))) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
1303, 7, 8, 9, 10, 11frgpuptf 18006 . . . . . . . . . 10 (𝜑𝑇:(𝐼 × 2𝑜)⟶𝐵)
131130adantr 480 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝑇:(𝐼 × 2𝑜)⟶𝐵)
132 fcompt 6306 . . . . . . . . 9 ((𝑇:(𝐼 × 2𝑜)⟶𝐵𝑡:(0..^(#‘𝑡))⟶(𝐼 × 2𝑜)) → (𝑇𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
133131, 52, 132syl2anc 691 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡𝑛))))
13453s1cld 13236 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ Word (𝐼 × 2𝑜))
13529ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → 𝑊 = Word (𝐼 × 2𝑜))
136134, 135eleqtrrd 2691 . . . . . . . . . 10 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → ⟨“(𝑡𝑛)”⟩ ∈ 𝑊)
13714, 13, 12, 2frgpeccl 17997 . . . . . . . . . 10 (⟨“(𝑡𝑛)”⟩ ∈ 𝑊 → [⟨“(𝑡𝑛)”⟩] 𝑋)
138136, 137syl 17 . . . . . . . . 9 (((𝜑𝑡𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → [⟨“(𝑡𝑛)”⟩] 𝑋)
13952feqmptd 6159 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝑡 = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑡𝑛)))
14010adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑡𝑊) → 𝐼𝑉)
141140, 23, 24sylancl 693 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → (𝐼 × 2𝑜) ∈ V)
142 eqid 2610 . . . . . . . . . . . . 13 (varFMnd‘(𝐼 × 2𝑜)) = (varFMnd‘(𝐼 × 2𝑜))
143142vrmdfval 17216 . . . . . . . . . . . 12 ((𝐼 × 2𝑜) ∈ V → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦ ⟨“𝑤”⟩))
144141, 143syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦ ⟨“𝑤”⟩))
145 s1eq 13233 . . . . . . . . . . 11 (𝑤 = (𝑡𝑛) → ⟨“𝑤”⟩ = ⟨“(𝑡𝑛)”⟩)
14653, 139, 144, 145fmptco 6303 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ ⟨“(𝑡𝑛)”⟩))
147 eqidd 2611 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] ))
148 eceq1 7669 . . . . . . . . . 10 (𝑤 = ⟨“(𝑡𝑛)”⟩ → [𝑤] = [⟨“(𝑡𝑛)”⟩] )
149136, 146, 147, 148fmptco 6303 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ [⟨“(𝑡𝑛)”⟩] ))
1501adantr 480 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻))
151150, 4syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → 𝐾:𝑋𝐵)
152151feqmptd 6159 . . . . . . . . 9 ((𝜑𝑡𝑊) → 𝐾 = (𝑤𝑋 ↦ (𝐾𝑤)))
153 fveq2 6103 . . . . . . . . 9 (𝑤 = [⟨“(𝑡𝑛)”⟩] → (𝐾𝑤) = (𝐾‘[⟨“(𝑡𝑛)”⟩] ))
154138, 149, 152, 153fmptco 6303 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝐾‘[⟨“(𝑡𝑛)”⟩] )))
155129, 133, 1543eqtr4d 2654 . . . . . . 7 ((𝜑𝑡𝑊) → (𝑇𝑡) = (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
156155oveq2d 6565 . . . . . 6 ((𝜑𝑡𝑊) → (𝐻 Σg (𝑇𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
1573, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpupval 18010 . . . . . 6 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐻 Σg (𝑇𝑡)))
158 ghmmhm 17493 . . . . . . . 8 (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻))
159150, 158syl 17 . . . . . . 7 ((𝜑𝑡𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻))
160142vrmdf 17218 . . . . . . . . . . 11 ((𝐼 × 2𝑜) ∈ V → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜))
161141, 160syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜))
16249feq3d 5945 . . . . . . . . . 10 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊 ↔ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜)))
163161, 162mpbird 246 . . . . . . . . 9 ((𝜑𝑡𝑊) → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊)
164 wrdco 13428 . . . . . . . . 9 ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊)
16550, 163, 164syl2anc 691 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊)
16633adantr 480 . . . . . . . . . . . 12 ((𝜑𝑡𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
167166mpteq1d 4666 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ))
168 eqid 2610 . . . . . . . . . . . . 13 (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) = (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] )
16920, 30, 14, 13, 168frgpmhm 18001 . . . . . . . . . . . 12 (𝐼𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
170140, 169syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
171167, 170eqeltrd 2688 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺))
17230, 2mhmf 17163 . . . . . . . . . 10 ((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋)
173171, 172syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋)
174166feq2d 5944 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ):𝑊𝑋 ↔ (𝑤𝑊 ↦ [𝑤] ):(Base‘(freeMnd‘(𝐼 × 2𝑜)))⟶𝑋))
175173, 174mpbird 246 . . . . . . . 8 ((𝜑𝑡𝑊) → (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋)
176 wrdco 13428 . . . . . . . 8 ((((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word 𝑊 ∧ (𝑤𝑊 ↦ [𝑤] ):𝑊𝑋) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋)
177165, 175, 176syl2anc 691 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋)
1782gsumwmhm 17205 . . . . . . 7 ((𝐾 ∈ (𝐺 MndHom 𝐻) ∧ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) ∈ Word 𝑋) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
179159, 177, 178syl2anc 691 . . . . . 6 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
180156, 157, 1793eqtr4d 2654 . . . . 5 ((𝜑𝑡𝑊) → (𝐸‘[𝑡] ) = (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))))
18120, 142frmdgsum 17222 . . . . . . . . 9 (((𝐼 × 2𝑜) ∈ V ∧ 𝑡 ∈ Word (𝐼 × 2𝑜)) → ((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = 𝑡)
182141, 50, 181syl2anc 691 . . . . . . . 8 ((𝜑𝑡𝑊) → ((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)) = 𝑡)
183182fveq2d 6107 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = ((𝑤𝑊 ↦ [𝑤] )‘𝑡))
184 wrdco 13428 . . . . . . . . . 10 ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ (varFMnd‘(𝐼 × 2𝑜)):(𝐼 × 2𝑜)⟶Word (𝐼 × 2𝑜)) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word Word (𝐼 × 2𝑜))
18550, 161, 184syl2anc 691 . . . . . . . . 9 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word Word (𝐼 × 2𝑜))
18632adantr 480 . . . . . . . . . 10 ((𝜑𝑡𝑊) → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
187 wrdeq 13182 . . . . . . . . . 10 ((Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜) → Word (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word Word (𝐼 × 2𝑜))
188186, 187syl 17 . . . . . . . . 9 ((𝜑𝑡𝑊) → Word (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word Word (𝐼 × 2𝑜))
189185, 188eleqtrrd 2691 . . . . . . . 8 ((𝜑𝑡𝑊) → ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2𝑜))))
19030gsumwmhm 17205 . . . . . . . 8 (((𝑤𝑊 ↦ [𝑤] ) ∈ ((freeMnd‘(𝐼 × 2𝑜)) MndHom 𝐺) ∧ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡) ∈ Word (Base‘(freeMnd‘(𝐼 × 2𝑜)))) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
191171, 189, 190syl2anc 691 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘((freeMnd‘(𝐼 × 2𝑜)) Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))))
19212, 13efger 17954 . . . . . . . . 9 Er 𝑊
193192a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → Er 𝑊)
194 fvex 6113 . . . . . . . . . 10 ( I ‘Word (𝐼 × 2𝑜)) ∈ V
19512, 194eqeltri 2684 . . . . . . . . 9 𝑊 ∈ V
196195a1i 11 . . . . . . . 8 ((𝜑𝑡𝑊) → 𝑊 ∈ V)
197 eqid 2610 . . . . . . . 8 (𝑤𝑊 ↦ [𝑤] ) = (𝑤𝑊 ↦ [𝑤] )
198193, 196, 197divsfval 16030 . . . . . . 7 ((𝜑𝑡𝑊) → ((𝑤𝑊 ↦ [𝑤] )‘𝑡) = [𝑡] )
199183, 191, 1983eqtr3d 2652 . . . . . 6 ((𝜑𝑡𝑊) → (𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡))) = [𝑡] )
200199fveq2d 6107 . . . . 5 ((𝜑𝑡𝑊) → (𝐾‘(𝐺 Σg ((𝑤𝑊 ↦ [𝑤] ) ∘ ((varFMnd‘(𝐼 × 2𝑜)) ∘ 𝑡)))) = (𝐾‘[𝑡] ))
201180, 200eqtr2d 2645 . . . 4 ((𝜑𝑡𝑊) → (𝐾‘[𝑡] ) = (𝐸‘[𝑡] ))
20244, 47, 201ectocld 7701 . . 3 ((𝜑𝑎 ∈ (𝑊 / )) → (𝐾𝑎) = (𝐸𝑎))
20343, 202syldan 486 . 2 ((𝜑𝑎𝑋) → (𝐾𝑎) = (𝐸𝑎))
2046, 19, 203eqfnfvd 6222 1 (𝜑𝐾 = 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383   = wceq 1475  wcel 1977  wne 2780  wrex 2897  Vcvv 3173  wss 3540  c0 3874  ifcif 4036  {cpr 4127  cop 4131  cmpt 4643   I cid 4948   × cxp 5036  ran crn 5039  ccom 5042  Oncon0 5640   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  cmpt2 6551  1𝑜c1o 7440  2𝑜c2o 7441   Er wer 7626  [cec 7627   / cqs 7628  0cc0 9815  ..^cfzo 12334  #chash 12979  Word cword 13146  ⟨“cs1 13149  Basecbs 15695   Σg cgsu 15924   /s cqus 15988   MndHom cmhm 17156  freeMndcfrmd 17207  varFMndcvrmd 17208  Grpcgrp 17245  invgcminusg 17246   GrpHom cghm 17480   ~FG cefg 17942  freeGrpcfrgp 17943  varFGrpcvrgp 17944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-ot 4134  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-ec 7631  df-qs 7635  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-xnn0 11241  df-z 11255  df-dec 11370  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-word 13154  df-lsw 13155  df-concat 13156  df-s1 13157  df-substr 13158  df-splice 13159  df-reverse 13160  df-s2 13444  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-0g 15925  df-gsum 15926  df-imas 15991  df-qus 15992  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-submnd 17159  df-frmd 17209  df-vrmd 17210  df-grp 17248  df-minusg 17249  df-ghm 17481  df-efg 17945  df-frgp 17946  df-vrgp 17947
This theorem is referenced by:  frgpup3  18014
  Copyright terms: Public domain W3C validator