Step |
Hyp |
Ref |
Expression |
1 |
|
abl1.m |
⊢ 𝑀 = { 〈 ( Base ‘ ndx ) , { 𝐼 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 〉 } |
2 |
1
|
grp1 |
⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Grp ) |
3 |
|
eqidd |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) |
4 |
|
oveq1 |
⊢ ( 𝑎 = 𝐼 → ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) ) |
5 |
|
oveq2 |
⊢ ( 𝑎 = 𝐼 → ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) |
6 |
4 5
|
eqeq12d |
⊢ ( 𝑎 = 𝐼 → ( ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) ) |
7 |
6
|
ralbidv |
⊢ ( 𝑎 = 𝐼 → ( ∀ 𝑏 ∈ { 𝐼 } ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) ↔ ∀ 𝑏 ∈ { 𝐼 } ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) ) |
8 |
7
|
ralsng |
⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑎 ∈ { 𝐼 } ∀ 𝑏 ∈ { 𝐼 } ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) ↔ ∀ 𝑏 ∈ { 𝐼 } ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) ) |
9 |
|
oveq2 |
⊢ ( 𝑏 = 𝐼 → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) |
10 |
|
oveq1 |
⊢ ( 𝑏 = 𝐼 → ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) |
11 |
9 10
|
eqeq12d |
⊢ ( 𝑏 = 𝐼 → ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) ) |
12 |
11
|
ralsng |
⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑏 ∈ { 𝐼 } ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) ) |
13 |
8 12
|
bitrd |
⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑎 ∈ { 𝐼 } ∀ 𝑏 ∈ { 𝐼 } ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) ) |
14 |
3 13
|
mpbird |
⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑎 ∈ { 𝐼 } ∀ 𝑏 ∈ { 𝐼 } ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) ) |
15 |
|
snex |
⊢ { 𝐼 } ∈ V |
16 |
1
|
grpbase |
⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) ) |
17 |
15 16
|
ax-mp |
⊢ { 𝐼 } = ( Base ‘ 𝑀 ) |
18 |
|
snex |
⊢ { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ∈ V |
19 |
1
|
grpplusg |
⊢ ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ∈ V → { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } = ( +g ‘ 𝑀 ) ) |
20 |
18 19
|
ax-mp |
⊢ { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } = ( +g ‘ 𝑀 ) |
21 |
17 20
|
isabl2 |
⊢ ( 𝑀 ∈ Abel ↔ ( 𝑀 ∈ Grp ∧ ∀ 𝑎 ∈ { 𝐼 } ∀ 𝑏 ∈ { 𝐼 } ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑏 ) = ( 𝑏 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) ) ) |
22 |
2 14 21
|
sylanbrc |
⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Abel ) |