This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
Assertion frgpnabl ( 1o ≺ 𝐼 → ¬ 𝐺 ∈ Abel )

Proof

Step Hyp Ref Expression
1 frgpnabl.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2 relsdom ⊢ Rel ≺
3 2 brrelex2i ⊢ ( 1o ≺ 𝐼 → 𝐼 ∈ V )
4 1sdom ⊢ ( 𝐼 ∈ V → ( 1o ≺ 𝐼 ↔ ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 𝐼 ¬ 𝑎 = 𝑏 ) )
5 3 4 syl ⊢ ( 1o ≺ 𝐼 → ( 1o ≺ 𝐼 ↔ ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 𝐼 ¬ 𝑎 = 𝑏 ) )
6 5 ibi ⊢ ( 1o ≺ 𝐼 → ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 𝐼 ¬ 𝑎 = 𝑏 )
7 eqid ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
8 eqid ⊢ ( ~FG ‘ 𝐼 ) = ( ~FG ‘ 𝐼 )
9 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
10 eqid ⊢ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
11 eqid ⊢ ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) = ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) )
12 eqid ⊢ ( ( I ‘ Word ( 𝐼 × 2o ) ) ∖ ∪ 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ran ( ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) ‘ 𝑥 ) ) = ( ( I ‘ Word ( 𝐼 × 2o ) ) ∖ ∪ 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ran ( ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) ‘ 𝑥 ) )
13 eqid ⊢ ( varFGrp ‘ 𝐼 ) = ( varFGrp ‘ 𝐼 )
14 3 ad2antrr ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → 𝐼 ∈ V )
15 simplrl ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → 𝑎 ∈ 𝐼 )
16 simplrr ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → 𝑏 ∈ 𝐼 )
17 simpr ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → 𝐺 ∈ Abel )
18 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
19 8 13 1 18 vrgpf ⊢ ( 𝐼 ∈ V → ( varFGrp ‘ 𝐼 ) : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
20 14 19 syl ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → ( varFGrp ‘ 𝐼 ) : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
21 20 15 ffvelcdmd ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → ( ( varFGrp ‘ 𝐼 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐺 ) )
22 20 16 ffvelcdmd ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → ( ( varFGrp ‘ 𝐼 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝐺 ) )
23 18 9 ablcom ⊢ ( ( 𝐺 ∈ Abel ∧ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐺 ) ∧ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( ( varFGrp ‘ 𝐼 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ 𝑏 ) ) = ( ( ( varFGrp ‘ 𝐼 ) ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ 𝑎 ) ) )
24 17 21 22 23 syl3anc ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → ( ( ( varFGrp ‘ 𝐼 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ 𝑏 ) ) = ( ( ( varFGrp ‘ 𝐼 ) ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ 𝑎 ) ) )
25 1 7 8 9 10 11 12 13 14 15 16 24 frgpnabllem2 ⊢ ( ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) ∧ 𝐺 ∈ Abel ) → 𝑎 = 𝑏 )
26 25 ex ⊢ ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) → ( 𝐺 ∈ Abel → 𝑎 = 𝑏 ) )
27 26 con3d ⊢ ( ( 1o ≺ 𝐼 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) → ( ¬ 𝑎 = 𝑏 → ¬ 𝐺 ∈ Abel ) )
28 27 rexlimdvva ⊢ ( 1o ≺ 𝐼 → ( ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 𝐼 ¬ 𝑎 = 𝑏 → ¬ 𝐺 ∈ Abel ) )
29 6 28 mpd ⊢ ( 1o ≺ 𝐼 → ¬ 𝐺 ∈ Abel )