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 
|- 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 imbitrid 
 |-  ( ( +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 >. } ) )