Metamath Proof Explorer


Theorem abl1

Description: The (smallest) structure representing atrivial abelian group. (Contributed by AV, 28-Apr-2019)

Ref Expression
Hypothesis abl1.m 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
Assertion abl1 ( 𝐼𝑉𝑀 ∈ Abel )

Proof

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 )