Theorem mgmplusfreseq

Description: If the empty set is not contained in the base set of a magma, the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020)

	Ref	Expression
Hypotheses	plusfreseq.1	⊢ 𝐵 = ( Base ‘ 𝑀 )
	plusfreseq.2	⊢ + = ( +g ‘ 𝑀 )
	plusfreseq.3	⊢ ⨣ = ( +𝑓 ‘ 𝑀 )
Assertion	mgmplusfreseq	⊢ ( ( 𝑀 ∈ Mgm ∧ ∅ ∉ 𝐵 ) → ( + ↾ ( 𝐵 × 𝐵 ) ) = ⨣ )

Proof

Step	Hyp	Ref	Expression
1		plusfreseq.1	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		plusfreseq.2	⊢ + = ( +g ‘ 𝑀 )
3		plusfreseq.3	⊢ ⨣ = ( +𝑓 ‘ 𝑀 )
4	1 3	mgmplusf	⊢ ( 𝑀 ∈ Mgm → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
5		frn	⊢ ( ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 → ran ⨣ ⊆ 𝐵 )
6		ssel	⊢ ( ran ⨣ ⊆ 𝐵 → ( ∅ ∈ ran ⨣ → ∅ ∈ 𝐵 ) )
7	6	nelcon3d	⊢ ( ran ⨣ ⊆ 𝐵 → ( ∅ ∉ 𝐵 → ∅ ∉ ran ⨣ ) )
8	4 5 7	3syl	⊢ ( 𝑀 ∈ Mgm → ( ∅ ∉ 𝐵 → ∅ ∉ ran ⨣ ) )
9	8	imp	⊢ ( ( 𝑀 ∈ Mgm ∧ ∅ ∉ 𝐵 ) → ∅ ∉ ran ⨣ )
10	1 2 3	plusfreseq	⊢ ( ∅ ∉ ran ⨣ → ( + ↾ ( 𝐵 × 𝐵 ) ) = ⨣ )
11	9 10	syl	⊢ ( ( 𝑀 ∈ Mgm ∧ ∅ ∉ 𝐵 ) → ( + ↾ ( 𝐵 × 𝐵 ) ) = ⨣ )