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 + ˙ = + M
Assertion mgmb1mgm1 M Mgm Z B + ˙ Fn B × B B = Z + ˙ = Z Z Z

Proof

Step Hyp Ref Expression
1 mgmb1mgm1.b B = Base M
2 mgmb1mgm1.p + ˙ = + M
3 eqid + 𝑓 M = + 𝑓 M
4 1 2 3 plusfeq + ˙ Fn B × B + 𝑓 M = + ˙
5 1 3 mgmplusf M Mgm + 𝑓 M : B × B B
6 feq1 + 𝑓 M = + ˙ + 𝑓 M : B × B B + ˙ : B × B B
7 5 6 syl5ib + 𝑓 M = + ˙ M Mgm + ˙ : B × B B
8 4 7 syl + ˙ Fn B × B M Mgm + ˙ : B × B B
9 8 impcom M Mgm + ˙ Fn B × B + ˙ : B × B B
10 9 3adant2 M Mgm Z B + ˙ Fn B × B + ˙ : B × B B
11 simp2 M Mgm Z B + ˙ Fn B × B Z B
12 intopsn + ˙ : B × B B Z B B = Z + ˙ = Z Z Z
13 10 11 12 syl2anc M Mgm Z B + ˙ Fn B × B B = Z + ˙ = Z Z Z