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	$⊢ G = freeGrp (I)$
	frgp0.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
Assertion	frgp0	$⊢ I \in V \to (G \in Grp \land [\emptyset] \underset{˙}{\sim} = 0_{G})$

Proof

Step	Hyp	Ref	Expression
1		frgp0.m	$⊢ G = freeGrp (I)$
2		frgp0.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		eqid	$⊢ freeMnd (I \times 2_{𝑜}) = freeMnd (I \times 2_{𝑜})$
4	1 3 2	frgpval	$⊢ I \in V \to G = freeMnd (I \times 2_{𝑜}) /_{𝑠} \underset{˙}{\sim}$
5		2on	$⊢ 2_{𝑜} \in On$
6		xpexg	$⊢ (I \in V \land 2_{𝑜} \in On) \to I \times 2_{𝑜} \in V$
7	5 6	mpan2	$⊢ I \in V \to I \times 2_{𝑜} \in V$
8		eqid	$⊢ {Base}_{freeMnd (I \times 2_{𝑜})} = {Base}_{freeMnd (I \times 2_{𝑜})}$
9	3 8	frmdbas	$⊢ I \times 2_{𝑜} \in V \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
10	7 9	syl	$⊢ I \in V \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
11	10	eqcomd	$⊢ I \in V \to Word (I \times 2_{𝑜}) = {Base}_{freeMnd (I \times 2_{𝑜})}$
12		eqidd	$⊢ I \in V \to +_{freeMnd (I \times 2_{𝑜})} = +_{freeMnd (I \times 2_{𝑜})}$
13		eqid	$⊢ I (Word (I \times 2_{𝑜})) = I (Word (I \times 2_{𝑜}))$
14	13 2	efger	$⊢ \underset{˙}{\sim} Er I (Word (I \times 2_{𝑜}))$
15		wrdexg	$⊢ I \times 2_{𝑜} \in V \to Word (I \times 2_{𝑜}) \in V$
16		fvi	$⊢ Word (I \times 2_{𝑜}) \in V \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
17	7 15 16	3syl	$⊢ I \in V \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
18		ereq2	$⊢ I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜}) \to (\underset{˙}{\sim} Er I (Word (I \times 2_{𝑜})) \leftrightarrow \underset{˙}{\sim} Er Word (I \times 2_{𝑜}))$
19	17 18	syl	$⊢ I \in V \to (\underset{˙}{\sim} Er I (Word (I \times 2_{𝑜})) \leftrightarrow \underset{˙}{\sim} Er Word (I \times 2_{𝑜}))$
20	14 19	mpbii	$⊢ I \in V \to \underset{˙}{\sim} Er Word (I \times 2_{𝑜})$
21		fvexd	$⊢ I \in V \to freeMnd (I \times 2_{𝑜}) \in V$
22		eqid	$⊢ +_{freeMnd (I \times 2_{𝑜})} = +_{freeMnd (I \times 2_{𝑜})}$
23	1 3 2 22	frgpcpbl	$⊢ (a \underset{˙}{\sim} b \land c \underset{˙}{\sim} d) \to (a +_{freeMnd (I \times 2_{𝑜})} c) \underset{˙}{\sim} (b +_{freeMnd (I \times 2_{𝑜})} d)$
24	23	a1i	$⊢ I \in V \to ((a \underset{˙}{\sim} b \land c \underset{˙}{\sim} d) \to (a +_{freeMnd (I \times 2_{𝑜})} c) \underset{˙}{\sim} (b +_{freeMnd (I \times 2_{𝑜})} d))$
25	3	frmdmnd	$⊢ I \times 2_{𝑜} \in V \to freeMnd (I \times 2_{𝑜}) \in Mnd$
26	7 25	syl	$⊢ I \in V \to freeMnd (I \times 2_{𝑜}) \in Mnd$
27	26	3ad2ant1	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜})) \to freeMnd (I \times 2_{𝑜}) \in Mnd$
28		simp2	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜})) \to x \in Word (I \times 2_{𝑜})$
29	11	3ad2ant1	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜})) \to Word (I \times 2_{𝑜}) = {Base}_{freeMnd (I \times 2_{𝑜})}$
30	28 29	eleqtrd	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜})) \to x \in {Base}_{freeMnd (I \times 2_{𝑜})}$
31		simp3	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜})) \to y \in Word (I \times 2_{𝑜})$
32	31 29	eleqtrd	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜})) \to y \in {Base}_{freeMnd (I \times 2_{𝑜})}$
33	8 22	mndcl	$⊢ (freeMnd (I \times 2_{𝑜}) \in Mnd \land x \in {Base}_{freeMnd (I \times 2_{𝑜})} \land y \in {Base}_{freeMnd (I \times 2_{𝑜})}) \to x +_{freeMnd (I \times 2_{𝑜})} y \in {Base}_{freeMnd (I \times 2_{𝑜})}$
34	27 30 32 33	syl3anc	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜})) \to x +_{freeMnd (I \times 2_{𝑜})} y \in {Base}_{freeMnd (I \times 2_{𝑜})}$
35	34 29	eleqtrrd	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜})) \to x +_{freeMnd (I \times 2_{𝑜})} y \in Word (I \times 2_{𝑜})$
36	20	adantr	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to \underset{˙}{\sim} Er Word (I \times 2_{𝑜})$
37	26	adantr	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to freeMnd (I \times 2_{𝑜}) \in Mnd$
38	34	3adant3r3	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to x +_{freeMnd (I \times 2_{𝑜})} y \in {Base}_{freeMnd (I \times 2_{𝑜})}$
39		simpr3	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to z \in Word (I \times 2_{𝑜})$
40	11	adantr	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to Word (I \times 2_{𝑜}) = {Base}_{freeMnd (I \times 2_{𝑜})}$
41	39 40	eleqtrd	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to z \in {Base}_{freeMnd (I \times 2_{𝑜})}$
42	8 22	mndcl	$⊢ (freeMnd (I \times 2_{𝑜}) \in Mnd \land x +_{freeMnd (I \times 2_{𝑜})} y \in {Base}_{freeMnd (I \times 2_{𝑜})} \land z \in {Base}_{freeMnd (I \times 2_{𝑜})}) \to (x +_{freeMnd (I \times 2_{𝑜})} y) +_{freeMnd (I \times 2_{𝑜})} z \in {Base}_{freeMnd (I \times 2_{𝑜})}$
43	37 38 41 42	syl3anc	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to (x +_{freeMnd (I \times 2_{𝑜})} y) +_{freeMnd (I \times 2_{𝑜})} z \in {Base}_{freeMnd (I \times 2_{𝑜})}$
44	43 40	eleqtrrd	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to (x +_{freeMnd (I \times 2_{𝑜})} y) +_{freeMnd (I \times 2_{𝑜})} z \in Word (I \times 2_{𝑜})$
45	36 44	erref	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to ((x +_{freeMnd (I \times 2_{𝑜})} y) +_{freeMnd (I \times 2_{𝑜})} z) \underset{˙}{\sim} ((x +_{freeMnd (I \times 2_{𝑜})} y) +_{freeMnd (I \times 2_{𝑜})} z)$
46	30	3adant3r3	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to x \in {Base}_{freeMnd (I \times 2_{𝑜})}$
47	32	3adant3r3	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to y \in {Base}_{freeMnd (I \times 2_{𝑜})}$
48	8 22	mndass	$⊢ (freeMnd (I \times 2_{𝑜}) \in Mnd \land (x \in {Base}_{freeMnd (I \times 2_{𝑜})} \land y \in {Base}_{freeMnd (I \times 2_{𝑜})} \land z \in {Base}_{freeMnd (I \times 2_{𝑜})})) \to (x +_{freeMnd (I \times 2_{𝑜})} y) +_{freeMnd (I \times 2_{𝑜})} z = x +_{freeMnd (I \times 2_{𝑜})} (y +_{freeMnd (I \times 2_{𝑜})} z)$
49	37 46 47 41 48	syl13anc	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to (x +_{freeMnd (I \times 2_{𝑜})} y) +_{freeMnd (I \times 2_{𝑜})} z = x +_{freeMnd (I \times 2_{𝑜})} (y +_{freeMnd (I \times 2_{𝑜})} z)$
50	45 49	breqtrd	$⊢ (I \in V \land (x \in Word (I \times 2_{𝑜}) \land y \in Word (I \times 2_{𝑜}) \land z \in Word (I \times 2_{𝑜}))) \to ((x +_{freeMnd (I \times 2_{𝑜})} y) +_{freeMnd (I \times 2_{𝑜})} z) \underset{˙}{\sim} (x +_{freeMnd (I \times 2_{𝑜})} (y +_{freeMnd (I \times 2_{𝑜})} z))$
51		wrd0	$⊢ \emptyset \in Word (I \times 2_{𝑜})$
52	51	a1i	$⊢ I \in V \to \emptyset \in Word (I \times 2_{𝑜})$
53	51 11	eleqtrid	$⊢ I \in V \to \emptyset \in {Base}_{freeMnd (I \times 2_{𝑜})}$
54	53	adantr	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to \emptyset \in {Base}_{freeMnd (I \times 2_{𝑜})}$
55	11	eleq2d	$⊢ I \in V \to (x \in Word (I \times 2_{𝑜}) \leftrightarrow x \in {Base}_{freeMnd (I \times 2_{𝑜})})$
56	55	biimpa	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to x \in {Base}_{freeMnd (I \times 2_{𝑜})}$
57	3 8 22	frmdadd	$⊢ (\emptyset \in {Base}_{freeMnd (I \times 2_{𝑜})} \land x \in {Base}_{freeMnd (I \times 2_{𝑜})}) \to \emptyset +_{freeMnd (I \times 2_{𝑜})} x = \emptyset ++ x$
58	54 56 57	syl2anc	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to \emptyset +_{freeMnd (I \times 2_{𝑜})} x = \emptyset ++ x$
59		ccatlid	$⊢ x \in Word (I \times 2_{𝑜}) \to \emptyset ++ x = x$
60	59	adantl	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to \emptyset ++ x = x$
61	58 60	eqtrd	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to \emptyset +_{freeMnd (I \times 2_{𝑜})} x = x$
62	20	adantr	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to \underset{˙}{\sim} Er Word (I \times 2_{𝑜})$
63		simpr	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to x \in Word (I \times 2_{𝑜})$
64	62 63	erref	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to x \underset{˙}{\sim} x$
65	61 64	eqbrtrd	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to (\emptyset +_{freeMnd (I \times 2_{𝑜})} x) \underset{˙}{\sim} x$
66		revcl	$⊢ x \in Word (I \times 2_{𝑜}) \to reverse (x) \in Word (I \times 2_{𝑜})$
67	66	adantl	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to reverse (x) \in Word (I \times 2_{𝑜})$
68		eqid	$⊢ (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
69	68	efgmf	$⊢ (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
70	69	a1i	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
71		wrdco	$⊢ (reverse (x) \in Word (I \times 2_{𝑜}) \land (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}) \to (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x) \in Word (I \times 2_{𝑜})$
72	67 70 71	syl2anc	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x) \in Word (I \times 2_{𝑜})$
73	11	adantr	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to Word (I \times 2_{𝑜}) = {Base}_{freeMnd (I \times 2_{𝑜})}$
74	72 73	eleqtrd	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x) \in {Base}_{freeMnd (I \times 2_{𝑜})}$
75	3 8 22	frmdadd	$⊢ ((y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x) \in {Base}_{freeMnd (I \times 2_{𝑜})} \land x \in {Base}_{freeMnd (I \times 2_{𝑜})}) \to ((y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x)) +_{freeMnd (I \times 2_{𝑜})} x = ((y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x)) ++ x$
76	74 56 75	syl2anc	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to ((y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x)) +_{freeMnd (I \times 2_{𝑜})} x = ((y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x)) ++ x$
77	17	eleq2d	$⊢ I \in V \to (x \in I (Word (I \times 2_{𝑜})) \leftrightarrow x \in Word (I \times 2_{𝑜}))$
78	77	biimpar	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to x \in I (Word (I \times 2_{𝑜}))$
79		eqid	$⊢ (v \in I (Word (I \times 2_{𝑜})) ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) (w) ”⟩⟩)) = (v \in I (Word (I \times 2_{𝑜})) ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) (w) ”⟩⟩))$
80	13 2 68 79	efginvrel1	$⊢ x \in I (Word (I \times 2_{𝑜})) \to (((y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x)) ++ x) \underset{˙}{\sim} \emptyset$
81	78 80	syl	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to (((y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x)) ++ x) \underset{˙}{\sim} \emptyset$
82	76 81	eqbrtrd	$⊢ (I \in V \land x \in Word (I \times 2_{𝑜})) \to (((y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) \circ reverse (x)) +_{freeMnd (I \times 2_{𝑜})} x) \underset{˙}{\sim} \emptyset$
83	4 11 12 20 21 24 35 50 52 65 72 82	qusgrp2	$⊢ I \in V \to (G \in Grp \land [\emptyset] \underset{˙}{\sim} = 0_{G})$

Metamath Proof Explorer

Theorem frgp0

Proof