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
|- B = ( Base ` M )
mgmb1mgm1.p
|- .+ = ( +g ` M )
Assertion mgmb1mgm1
|- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )

Proof

Step Hyp Ref Expression
1 mgmb1mgm1.b
 |-  B = ( Base ` M )
2 mgmb1mgm1.p
 |-  .+ = ( +g ` M )
3 eqid
 |-  ( +f ` M ) = ( +f ` M )
4 1 2 3 plusfeq
 |-  ( .+ Fn ( B X. B ) -> ( +f ` M ) = .+ )
5 1 3 mgmplusf
 |-  ( M e. Mgm -> ( +f ` M ) : ( B X. B ) --> B )
6 feq1
 |-  ( ( +f ` M ) = .+ -> ( ( +f ` M ) : ( B X. B ) --> B <-> .+ : ( B X. B ) --> B ) )
7 5 6 syl5ib
 |-  ( ( +f ` M ) = .+ -> ( M e. Mgm -> .+ : ( B X. B ) --> B ) )
8 4 7 syl
 |-  ( .+ Fn ( B X. B ) -> ( M e. Mgm -> .+ : ( B X. B ) --> B ) )
9 8 impcom
 |-  ( ( M e. Mgm /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) --> B )
10 9 3adant2
 |-  ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) --> B )
11 simp2
 |-  ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> Z e. B )
12 intopsn
 |-  ( ( .+ : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )
13 10 11 12 syl2anc
 |-  ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )