Metamath Proof Explorer

Theorem frgpnabl

Description: The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypothesis frgpnabl.g ⊢ G = freeGrp ⁡ I
Assertion frgpnabl ⊢ 1 𝑜 ≺ I → ¬ G ∈ Abel

Proof

Step Hyp Ref Expression
1 frgpnabl.g ⊢ G = freeGrp ⁡ I
2 relsdom ⊢ Rel ⁡ ≺
3 2 brrelex2i ⊢ 1 𝑜 ≺ I → I ∈ V
4 1sdom ⊢ I ∈ V → 1 𝑜 ≺ I ↔ ∃ a ∈ I ∃ b ∈ I ¬ a = b
5 3 4 syl ⊢ 1 𝑜 ≺ I → 1 𝑜 ≺ I ↔ ∃ a ∈ I ∃ b ∈ I ¬ a = b
6 5 ibi ⊢ 1 𝑜 ≺ I → ∃ a ∈ I ∃ b ∈ I ¬ a = b
7 eqid ⊢ I ⁡ Word I × 2 𝑜 = I ⁡ Word I × 2 𝑜
8 eqid ⊢ ~ FG ⁡ I = ~ FG ⁡ I
9 eqid ⊢ + G = + G
10 eqid ⊢ y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
11 eqid ⊢ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ = v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩
12 eqid ⊢ I ⁡ Word I × 2 𝑜 ∖ ⋃ x ∈ I ⁡ Word I × 2 𝑜 ran ⁡ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ ⁡ x = I ⁡ Word I × 2 𝑜 ∖ ⋃ x ∈ I ⁡ Word I × 2 𝑜 ran ⁡ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ ⁡ x
13 eqid ⊢ var FGrp ⁡ I = var FGrp ⁡ I
14 3 ad2antrr ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → I ∈ V
15 simplrl ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → a ∈ I
16 simplrr ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → b ∈ I
17 simpr ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → G ∈ Abel
18 eqid ⊢ Base G = Base G
19 8 13 1 18 vrgpf ⊢ I ∈ V → var FGrp ⁡ I : I ⟶ Base G
20 14 19 syl ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → var FGrp ⁡ I : I ⟶ Base G
21 20 15 ffvelrnd ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → var FGrp ⁡ I ⁡ a ∈ Base G
22 20 16 ffvelrnd ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → var FGrp ⁡ I ⁡ b ∈ Base G
23 18 9 ablcom ⊢ G ∈ Abel ∧ var FGrp ⁡ I ⁡ a ∈ Base G ∧ var FGrp ⁡ I ⁡ b ∈ Base G → var FGrp ⁡ I ⁡ a + G var FGrp ⁡ I ⁡ b = var FGrp ⁡ I ⁡ b + G var FGrp ⁡ I ⁡ a
24 17 21 22 23 syl3anc ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → var FGrp ⁡ I ⁡ a + G var FGrp ⁡ I ⁡ b = var FGrp ⁡ I ⁡ b + G var FGrp ⁡ I ⁡ a
25 1 7 8 9 10 11 12 13 14 15 16 24 frgpnabllem2 ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I ∧ G ∈ Abel → a = b
26 25 ex ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I → G ∈ Abel → a = b
27 26 con3d ⊢ 1 𝑜 ≺ I ∧ a ∈ I ∧ b ∈ I → ¬ a = b → ¬ G ∈ Abel
28 27 rexlimdvva ⊢ 1 𝑜 ≺ I → ∃ a ∈ I ∃ b ∈ I ¬ a = b → ¬ G ∈ Abel
29 6 28 mpd ⊢ 1 𝑜 ≺ I → ¬ G ∈ Abel