Metamath Proof Explorer

Theorem frgp0

Description: The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses frgp0.m ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
frgp0.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
Assertion frgp0 ( 𝐼 ∈ 𝑉 → ( 𝐺 ∈ Grp ∧ [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 frgp0.m ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2 frgp0.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 eqid ⊢ ( freeMnd ‘ ( 𝐼 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) )
4 1 3 2 frgpval ⊢ ( 𝐼 ∈ 𝑉 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
5 2on ⊢ 2o ∈ On
6 xpexg ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
7 5 6 mpan2 ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × 2o ) ∈ V )
8 eqid ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
9 3 8 frmdbas ⊢ ( ( 𝐼 × 2o ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
10 7 9 syl ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
11 10 eqcomd ⊢ ( 𝐼 ∈ 𝑉 → Word ( 𝐼 × 2o ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
12 eqidd ⊢ ( 𝐼 ∈ 𝑉 → ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
13 eqid ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
14 13 2 efger ⊢ ∼ Er ( I ‘ Word ( 𝐼 × 2o ) )
15 wrdexg ⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
16 fvi ⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
17 7 15 16 3syl ⊢ ( 𝐼 ∈ 𝑉 → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
18 ereq2 ⊢ ( ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) → ( ∼ Er ( I ‘ Word ( 𝐼 × 2o ) ) ↔ ∼ Er Word ( 𝐼 × 2o ) ) )
19 17 18 syl ⊢ ( 𝐼 ∈ 𝑉 → ( ∼ Er ( I ‘ Word ( 𝐼 × 2o ) ) ↔ ∼ Er Word ( 𝐼 × 2o ) ) )
20 14 19 mpbii ⊢ ( 𝐼 ∈ 𝑉 → ∼ Er Word ( 𝐼 × 2o ) )
21 fvexd ⊢ ( 𝐼 ∈ 𝑉 → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ V )
22 eqid ⊢ ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
23 1 3 2 22 frgpcpbl ⊢ ( ( 𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑 ) → ( 𝑎 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑐 ) ∼ ( 𝑏 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑑 ) )
24 23 a1i ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑 ) → ( 𝑎 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑐 ) ∼ ( 𝑏 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑑 ) ) )
25 3 frmdmnd ⊢ ( ( 𝐼 × 2o ) ∈ V → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd )
26 7 25 syl ⊢ ( 𝐼 ∈ 𝑉 → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd )
27 26 3ad2ant1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ) → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd )
28 simp2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ) → 𝑥 ∈ Word ( 𝐼 × 2o ) )
29 11 3ad2ant1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ) → Word ( 𝐼 × 2o ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
30 28 29 eleqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ) → 𝑥 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
31 simp3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ) → 𝑦 ∈ Word ( 𝐼 × 2o ) )
32 31 29 eleqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ) → 𝑦 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
33 8 22 mndcl ⊢ ( ( ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ) → ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
34 27 30 32 33 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ) → ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
35 34 29 eleqtrrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ) → ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ∈ Word ( 𝐼 × 2o ) )
36 20 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → ∼ Er Word ( 𝐼 × 2o ) )
37 26 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd )
38 34 3adant3r3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
39 simpr3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → 𝑧 ∈ Word ( 𝐼 × 2o ) )
40 11 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → Word ( 𝐼 × 2o ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
41 39 40 eleqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → 𝑧 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
42 8 22 mndcl ⊢ ( ( ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd ∧ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ∧ 𝑧 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ) → ( ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
43 37 38 41 42 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → ( ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
44 43 40 eleqtrrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → ( ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) ∈ Word ( 𝐼 × 2o ) )
45 36 44 erref ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → ( ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) ∼ ( ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) )
46 30 3adant3r3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → 𝑥 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
47 32 3adant3r3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → 𝑦 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
48 8 22 mndass ⊢ ( ( ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ∧ 𝑧 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ) ) → ( ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) = ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ( 𝑦 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) ) )
49 37 46 47 41 48 syl13anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → ( ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) = ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ( 𝑦 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) ) )
50 45 49 breqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑦 ∈ Word ( 𝐼 × 2o ) ∧ 𝑧 ∈ Word ( 𝐼 × 2o ) ) ) → ( ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑦 ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) ∼ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ( 𝑦 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑧 ) ) )
51 wrd0 ⊢ ∅ ∈ Word ( 𝐼 × 2o )
52 51 a1i ⊢ ( 𝐼 ∈ 𝑉 → ∅ ∈ Word ( 𝐼 × 2o ) )
53 51 11 eleqtrid ⊢ ( 𝐼 ∈ 𝑉 → ∅ ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
54 53 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ∅ ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
55 11 eleq2d ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ Word ( 𝐼 × 2o ) ↔ 𝑥 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ) )
56 55 biimpa ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → 𝑥 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
57 3 8 22 frmdadd ⊢ ( ( ∅ ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ) → ( ∅ ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑥 ) = ( ∅ ++ 𝑥 ) )
58 54 56 57 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ∅ ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑥 ) = ( ∅ ++ 𝑥 ) )
59 ccatlid ⊢ ( 𝑥 ∈ Word ( 𝐼 × 2o ) → ( ∅ ++ 𝑥 ) = 𝑥 )
60 59 adantl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ∅ ++ 𝑥 ) = 𝑥 )
61 58 60 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ∅ ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑥 ) = 𝑥 )
62 20 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ∼ Er Word ( 𝐼 × 2o ) )
63 simpr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → 𝑥 ∈ Word ( 𝐼 × 2o ) )
64 62 63 erref ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → 𝑥 ∼ 𝑥 )
65 61 64 eqbrtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ∅ ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑥 ) ∼ 𝑥 )
66 revcl ⊢ ( 𝑥 ∈ Word ( 𝐼 × 2o ) → ( reverse ‘ 𝑥 ) ∈ Word ( 𝐼 × 2o ) )
67 66 adantl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( reverse ‘ 𝑥 ) ∈ Word ( 𝐼 × 2o ) )
68 eqid ⊢ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
69 68 efgmf ⊢ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
70 69 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) )
71 wrdco ⊢ ( ( ( reverse ‘ 𝑥 ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ∈ Word ( 𝐼 × 2o ) )
72 67 70 71 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ∈ Word ( 𝐼 × 2o ) )
73 11 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → Word ( 𝐼 × 2o ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
74 72 73 eleqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
75 3 8 22 frmdadd ⊢ ( ( ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ) → ( ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑥 ) = ( ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ++ 𝑥 ) )
76 74 56 75 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑥 ) = ( ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ++ 𝑥 ) )
77 17 eleq2d ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↔ 𝑥 ∈ Word ( 𝐼 × 2o ) ) )
78 77 biimpar ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
79 eqid ⊢ ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) = ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) )
80 13 2 68 79 efginvrel1 ⊢ ( 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → ( ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ++ 𝑥 ) ∼ ∅ )
81 78 80 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ++ 𝑥 ) ∼ ∅ )
82 76 81 eqbrtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ∘ ( reverse ‘ 𝑥 ) ) ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑥 ) ∼ ∅ )
83 4 11 12 20 21 24 35 50 52 65 72 82 qusgrp2 ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐺 ∈ Grp ∧ [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) ) )