Theorem frgp0 18439

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

Hypotheses

Ref	Expression
frgp0.m	⊢ 𝐺 = (freeGrp‘𝐼)
frgp0.r	⊢ ∼ = ( ~FG ‘𝐼)

Assertion

Ref	Expression
frgp0	⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ = (0g‘𝐺)))

Proof of Theorem frgp0

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑥 𝑦 𝑧 𝑛 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frgp0.m	. . 3 ⊢ 𝐺 = (freeGrp‘𝐼)
2		eqid 2765	. . 3 ⊢ (freeMnd‘(𝐼 × 2𝑜)) = (freeMnd‘(𝐼 × 2𝑜))
3		frgp0.r	. . 3 ⊢ ∼ = ( ~FG ‘𝐼)
4	1, 2, 3	frgpval 18437	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ∼ ))
5		2on 7773	. . . . 5 ⊢ 2𝑜 ∈ On
6		xpexg 7158	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 2𝑜 ∈ On) → (𝐼 × 2𝑜) ∈ V)
7	5, 6	mpan2 682	. . . 4 ⊢ (𝐼 ∈ 𝑉 → (𝐼 × 2𝑜) ∈ V)
8		eqid 2765	. . . . 5 ⊢ (Base‘(freeMnd‘(𝐼 × 2𝑜))) = (Base‘(freeMnd‘(𝐼 × 2𝑜)))
9	2, 8	frmdbas 17656	. . . 4 ⊢ ((𝐼 × 2𝑜) ∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
10	7, 9	syl 17	. . 3 ⊢ (𝐼 ∈ 𝑉 → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
11	10	eqcomd 2771	. 2 ⊢ (𝐼 ∈ 𝑉 → Word (𝐼 × 2𝑜) = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
12		eqidd 2766	. 2 ⊢ (𝐼 ∈ 𝑉 → (+g‘(freeMnd‘(𝐼 × 2𝑜))) = (+g‘(freeMnd‘(𝐼 × 2𝑜))))
13		eqid 2765	. . . 4 ⊢ ( I ‘Word (𝐼 × 2𝑜)) = ( I ‘Word (𝐼 × 2𝑜))
14	13, 3	efger 18395	. . 3 ⊢ ∼ Er ( I ‘Word (𝐼 × 2𝑜))
15		wrdexg 13496	. . . . 5 ⊢ ((𝐼 × 2𝑜) ∈ V → Word (𝐼 × 2𝑜) ∈ V)
16		fvi 6444	. . . . 5 ⊢ (Word (𝐼 × 2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
17	7, 15, 16	3syl 18	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
18		ereq2 7955	. . . 4 ⊢ (( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜) → ( ∼ Er ( I ‘Word (𝐼 × 2𝑜)) ↔ ∼ Er Word (𝐼 × 2𝑜)))
19	17, 18	syl 17	. . 3 ⊢ (𝐼 ∈ 𝑉 → ( ∼ Er ( I ‘Word (𝐼 × 2𝑜)) ↔ ∼ Er Word (𝐼 × 2𝑜)))
20	14, 19	mpbii 224	. 2 ⊢ (𝐼 ∈ 𝑉 → ∼ Er Word (𝐼 × 2𝑜))
21		fvexd 6390	. 2 ⊢ (𝐼 ∈ 𝑉 → (freeMnd‘(𝐼 × 2𝑜)) ∈ V)
22		eqid 2765	. . . 4 ⊢ (+g‘(freeMnd‘(𝐼 × 2𝑜))) = (+g‘(freeMnd‘(𝐼 × 2𝑜)))
23	1, 2, 3, 22	frgpcpbl 18438	. . 3 ⊢ ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑐) ∼ (𝑏(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑑))
24	23	a1i 11	. 2 ⊢ (𝐼 ∈ 𝑉 → ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑐) ∼ (𝑏(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑑)))
25	2	frmdmnd 17663	. . . . . 6 ⊢ ((𝐼 × 2𝑜) ∈ V → (freeMnd‘(𝐼 × 2𝑜)) ∈ Mnd)
26	7, 25	syl 17	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → (freeMnd‘(𝐼 × 2𝑜)) ∈ Mnd)
27	26	3ad2ant1 1163	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → (freeMnd‘(𝐼 × 2𝑜)) ∈ Mnd)
28		simp2 1167	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → 𝑥 ∈ Word (𝐼 × 2𝑜))
29	11	3ad2ant1 1163	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → Word (𝐼 × 2𝑜) = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
30	28, 29	eleqtrd 2846	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → 𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
31		simp3 1168	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → 𝑦 ∈ Word (𝐼 × 2𝑜))
32	31, 29	eleqtrd 2846	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → 𝑦 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
33	8, 22	mndcl 17567	. . . 4 ⊢ (((freeMnd‘(𝐼 × 2𝑜)) ∈ Mnd ∧ 𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧ 𝑦 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜)))) → (𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦) ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
34	27, 30, 32, 33	syl3anc 1490	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → (𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦) ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
35	34, 29	eleqtrrd 2847	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → (𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦) ∈ Word (𝐼 × 2𝑜))
36	20	adantr 472	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → ∼ Er Word (𝐼 × 2𝑜))
37	26	adantr 472	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → (freeMnd‘(𝐼 × 2𝑜)) ∈ Mnd)
38	34	3adant3r3 1235	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → (𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦) ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
39		simpr3 1252	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → 𝑧 ∈ Word (𝐼 × 2𝑜))
40	11	adantr 472	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → Word (𝐼 × 2𝑜) = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
41	39, 40	eleqtrd 2846	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → 𝑧 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
42	8, 22	mndcl 17567	. . . . . 6 ⊢ (((freeMnd‘(𝐼 × 2𝑜)) ∈ Mnd ∧ (𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦) ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧ 𝑧 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜)))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧) ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
43	37, 38, 41, 42	syl3anc 1490	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧) ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
44	43, 40	eleqtrrd 2847	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧) ∈ Word (𝐼 × 2𝑜))
45	36, 44	erref 7967	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧) ∼ ((𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧))
46	30	3adant3r3 1235	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → 𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
47	32	3adant3r3 1235	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → 𝑦 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
48	8, 22	mndass 17568	. . . 4 ⊢ (((freeMnd‘(𝐼 × 2𝑜)) ∈ Mnd ∧ (𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧ 𝑦 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧ 𝑧 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧) = (𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))(𝑦(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧)))
49	37, 46, 47, 41, 48	syl13anc 1491	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧) = (𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))(𝑦(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧)))
50	45, 49	breqtrd 4835	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧) ∼ (𝑥(+g‘(freeMnd‘(𝐼 × 2𝑜)))(𝑦(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑧)))
51		wrd0 13511	. . 3 ⊢ ∅ ∈ Word (𝐼 × 2𝑜)
52	51	a1i 11	. 2 ⊢ (𝐼 ∈ 𝑉 → ∅ ∈ Word (𝐼 × 2𝑜))
53	51, 11	syl5eleq 2850	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → ∅ ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
54	53	adantr 472	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → ∅ ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
55	11	eleq2d 2830	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ Word (𝐼 × 2𝑜) ↔ 𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜)))))
56	55	biimpa 468	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → 𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
57	2, 8, 22	frmdadd 17659	. . . . 5 ⊢ ((∅ ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧ 𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜)))) → (∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = (∅ ++ 𝑥))
58	54, 56, 57	syl2anc 579	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = (∅ ++ 𝑥))
59		ccatlid 13557	. . . . 5 ⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) → (∅ ++ 𝑥) = 𝑥)
60	59	adantl 473	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (∅ ++ 𝑥) = 𝑥)
61	58, 60	eqtrd 2799	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = 𝑥)
62	20	adantr 472	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → ∼ Er Word (𝐼 × 2𝑜))
63		simpr 477	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → 𝑥 ∈ Word (𝐼 × 2𝑜))
64	62, 63	erref 7967	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → 𝑥 ∼ 𝑥)
65	61, 64	eqbrtrd 4831	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) ∼ 𝑥)
66		revcl 13785	. . . 4 ⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) → (reverse‘𝑥) ∈ Word (𝐼 × 2𝑜))
67	66	adantl 473	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (reverse‘𝑥) ∈ Word (𝐼 × 2𝑜))
68		eqid 2765	. . . . 5 ⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)
69	68	efgmf 18390	. . . 4 ⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩):(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜)
70	69	a1i 11	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩):(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜))
71		wrdco 13860	. . 3 ⊢ (((reverse‘𝑥) ∈ Word (𝐼 × 2𝑜) ∧ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩):(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜)) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥)) ∈ Word (𝐼 × 2𝑜))
72	67, 70, 71	syl2anc 579	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥)) ∈ Word (𝐼 × 2𝑜))
73	11	adantr 472	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → Word (𝐼 × 2𝑜) = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
74	72, 73	eleqtrd 2846	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥)) ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))))
75	2, 8, 22	frmdadd 17659	. . . 4 ⊢ ((((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥)) ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧ 𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2𝑜)))) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥)) ++ 𝑥))
76	74, 56, 75	syl2anc 579	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥)) ++ 𝑥))
77	17	eleq2d 2830	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ ( I ‘Word (𝐼 × 2𝑜)) ↔ 𝑥 ∈ Word (𝐼 × 2𝑜)))
78	77	biimpar 469	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → 𝑥 ∈ ( I ‘Word (𝐼 × 2𝑜)))
79		eqid 2765	. . . . 5 ⊢ (𝑣 ∈ ( I ‘Word (𝐼 × 2𝑜)) ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘𝑤)”⟩⟩))) = (𝑣 ∈ ( I ‘Word (𝐼 × 2𝑜)) ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘𝑤)”⟩⟩)))
80	13, 3, 68, 79	efginvrel1 18405	. . . 4 ⊢ (𝑥 ∈ ( I ‘Word (𝐼 × 2𝑜)) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥)) ++ 𝑥) ∼ ∅)
81	78, 80	syl 17	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥)) ++ 𝑥) ∼ ∅)
82	76, 81	eqbrtrd 4831	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) ∼ ∅)
83	4, 11, 12, 20, 21, 24, 35, 50, 52, 65, 72, 82	qusgrp2 17800	1 ⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ = (0g‘𝐺)))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1107   = wceq 1652   ∈ wcel 2155  Vcvv 3350   ∖ cdif 3729  ∅c0 4079  ⟨cop 4340  ⟨cotp 4342   class class class wbr 4809   ↦ cmpt 4888   I cid 5184   × cxp 5275   ∘ ccom 5281  Oncon0 5908  ⟶wf 6064  ‘cfv 6068  (class class class)co 6842   ↦ cmpt2 6844  1_𝑜c1o 7757  2_𝑜c2o 7758   Er wer 7944  [cec 7945  0cc0 10189  ...cfz 12533  ♯chash 13321  Word cword 13486   ++ cconcat 13541   splice csplice 13763  reversecreverse 13782  ⟨“cs2 13870  Basecbs 16130  +_gcplusg 16214  0_gc0g 16366  Mndcmnd 17560  freeMndcfrmd 17651  Grpcgrp 17689   ~_FG cefg 18383  freeGrpcfrgp 18384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-ot 4343  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-ec 7949  df-qs 7953  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-inf 8556  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-xnn0 11611  df-z 11625  df-dec 11741  df-uz 11887  df-fz 12534  df-fzo 12674  df-hash 13322  df-word 13487  df-lsw 13534  df-concat 13542  df-s1 13567  df-substr 13617  df-pfx 13662  df-splice 13765  df-reverse 13783  df-s2 13877  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-plusg 16227  df-mulr 16228  df-sca 16230  df-vsca 16231  df-ip 16232  df-tset 16233  df-ple 16234  df-ds 16236  df-0g 16368  df-imas 16434  df-qus 16435  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-frmd 17653  df-grp 17692  df-efg 18386  df-frgp 18387

This theorem is referenced by:  frgpgrp  18441  frgpinv  18443  frgpmhm  18444