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 )