Metamath Proof Explorer

Theorem sgrp1

Description: The structure with one element and the only closed internal operation for a singleton is a semigroup. (Contributed by AV, 10-Feb-2020)

Ref Expression
Hypothesis sgrp1.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
Assertion sgrp1 ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Smgrp )

Proof

Step Hyp Ref Expression
1 sgrp1.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
2 1 mgm1 ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mgm )
3 df-ov ⊢ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ )
4 opex ⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
5 fvsng ⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
6 4 5 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
7 3 6 syl5eq ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
8 7 oveq1d ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
9 7 oveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
10 8 9 eqtr4d ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ) )
11 oveq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) )
12 11 oveq1d ⊢ ( 𝑥 = 𝐼 → ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) )
13 oveq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) )
14 12 13 eqeq12d ⊢ ( 𝑥 = 𝐼 → ( ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ) )
15 14 2ralbidv ⊢ ( 𝑥 = 𝐼 → ( ∀ 𝑦 ∈ { 𝐼 } ∀ 𝑧 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ∀ 𝑦 ∈ { 𝐼 } ∀ 𝑧 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ) )
16 15 ralsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ∀ 𝑧 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ∀ 𝑦 ∈ { 𝐼 } ∀ 𝑧 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ) )
17 oveq2 ⊢ ( 𝑦 = 𝐼 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
18 17 oveq1d ⊢ ( 𝑦 = 𝐼 → ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) )
19 oveq1 ⊢ ( 𝑦 = 𝐼 → ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) )
20 19 oveq2d ⊢ ( 𝑦 = 𝐼 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) )
21 18 20 eqeq12d ⊢ ( 𝑦 = 𝐼 → ( ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ) )
22 21 ralbidv ⊢ ( 𝑦 = 𝐼 → ( ∀ 𝑧 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ∀ 𝑧 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ) )
23 22 ralsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑦 ∈ { 𝐼 } ∀ 𝑧 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ∀ 𝑧 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ) )
24 oveq2 ⊢ ( 𝑧 = 𝐼 → ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
25 oveq2 ⊢ ( 𝑧 = 𝐼 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
26 25 oveq2d ⊢ ( 𝑧 = 𝐼 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ) )
27 24 26 eqeq12d ⊢ ( 𝑧 = 𝐼 → ( ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ) ) )
28 27 ralsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑧 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ) ) )
29 16 23 28 3bitrd ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ∀ 𝑧 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ↔ ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ) ) )
30 10 29 mpbird ⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ∀ 𝑧 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) )
31 snex ⊢ { 𝐼 } ∈ V
32 1 grpbase ⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) )
33 31 32 ax-mp ⊢ { 𝐼 } = ( Base ‘ 𝑀 )
34 snex ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
35 1 grpplusg ⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
36 34 35 ax-mp ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 )
37 33 36 issgrp ⊢ ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ∀ 𝑧 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) = ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑧 ) ) ) )
38 2 30 37 sylanbrc ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Smgrp )