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 ffvelrnd ( ( ( 1o𝐼 ∧ ( 𝑎𝐼𝑏𝐼 ) ) ∧ 𝐺 ∈ Abel ) → ( ( varFGrp𝐼 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐺 ) )
22 20 16 ffvelrnd ( ( ( 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 )