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 )