Metamath Proof Explorer

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 ∧ ∅ ∉ ðĩ ) → ( + â†ū ( ðĩ × ðĩ ) ) = âĻĢ )