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	$⊢ \underset{˙}{+} = +_{M}$
	Assertion	mgmb1mgm1	$⊢ (M \in Mgm \land Z \in B \land \underset{˙}{+} Fn (B \times B)) \to (B = \{Z\} \leftrightarrow \underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\})$

Proof

Step	Hyp	Ref	Expression
1		mgmb1mgm1.b	$⊢ B = {Base}_{M}$
2		mgmb1mgm1.p	$⊢ \underset{˙}{+} = +_{M}$
3		eqid	$⊢ +_{𝑓} (M) = +_{𝑓} (M)$
4	1 2 3	plusfeq	$⊢ \underset{˙}{+} Fn (B \times B) \to +_{𝑓} (M) = \underset{˙}{+}$
5	1 3	mgmplusf	$⊢ M \in Mgm \to +_{𝑓} (M) : B \times B ⟶ B$
6		feq1	$⊢ +_{𝑓} (M) = \underset{˙}{+} \to (+_{𝑓} (M) : B \times B ⟶ B \leftrightarrow \underset{˙}{+} : B \times B ⟶ B)$
7	5 6	imbitrid	$⊢ +_{𝑓} (M) = \underset{˙}{+} \to (M \in Mgm \to \underset{˙}{+} : B \times B ⟶ B)$
8	4 7	syl	$⊢ \underset{˙}{+} Fn (B \times B) \to (M \in Mgm \to \underset{˙}{+} : B \times B ⟶ B)$
9	8	impcom	$⊢ (M \in Mgm \land \underset{˙}{+} Fn (B \times B)) \to \underset{˙}{+} : B \times B ⟶ B$
10	9	3adant2	$⊢ (M \in Mgm \land Z \in B \land \underset{˙}{+} Fn (B \times B)) \to \underset{˙}{+} : B \times B ⟶ B$
11		simp2	$⊢ (M \in Mgm \land Z \in B \land \underset{˙}{+} Fn (B \times B)) \to Z \in B$
12		intopsn	$⊢ (\underset{˙}{+} : B \times B ⟶ B \land Z \in B) \to (B = \{Z\} \leftrightarrow \underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\})$
13	10 11 12	syl2anc	$⊢ (M \in Mgm \land Z \in B \land \underset{˙}{+} Fn (B \times B)) \to (B = \{Z\} \leftrightarrow \underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\})$