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 ) |