This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mgmb1mgm1

Description: The only magma with a base set consisting of one element is the trivial magma (at least if its operation is an internal binary operation). (Contributed by AV, 23-Jan-2020) (Revised by AV, 7-Feb-2020)

Ref Expression
Hypotheses mgmb1mgm1.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
mgmb1mgm1.p ⊢ + = ( +g ‘ 𝑀 )
Assertion mgmb1mgm1 ( ( 𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 mgmb1mgm1.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 mgmb1mgm1.p ⊢ + = ( +g ‘ 𝑀 )
3 eqid ⊢ ( +𝑓 ‘ 𝑀 ) = ( +𝑓 ‘ 𝑀 )
4 1 2 3 plusfeq ⊢ ( + Fn ( 𝐵 × 𝐵 ) → ( +𝑓 ‘ 𝑀 ) = + )
5 1 3 mgmplusf ⊢ ( 𝑀 ∈ Mgm → ( +𝑓 ‘ 𝑀 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
6 feq1 ⊢ ( ( +𝑓 ‘ 𝑀 ) = + → ( ( +𝑓 ‘ 𝑀 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ↔ + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
7 5 6 imbitrid ⊢ ( ( +𝑓 ‘ 𝑀 ) = + → ( 𝑀 ∈ Mgm → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
8 4 7 syl ⊢ ( + Fn ( 𝐵 × 𝐵 ) → ( 𝑀 ∈ Mgm → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
9 8 impcom ⊢ ( ( 𝑀 ∈ Mgm ∧ + Fn ( 𝐵 × 𝐵 ) ) → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
10 9 3adant2 ⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
11 simp2 ⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → 𝑍 ∈ 𝐵 )
12 intopsn ⊢ ( ( + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
13 10 11 12 syl2anc ⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )