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	|- B = ( Base ` M )
	plusfreseq.2	|- .+ = ( +g ` M )
	plusfreseq.3	|- .+^ = ( +f ` M )
Assertion	mgmplusfreseq	|- ( ( M e. Mgm /\ (/) e/ B ) -> ( .+ |` ( B X. B ) ) = .+^ )

Proof

Step	Hyp	Ref	Expression
1		plusfreseq.1	|- B = ( Base ` M )
2		plusfreseq.2	|- .+ = ( +g ` M )
3		plusfreseq.3	|- .+^ = ( +f ` M )
4	1 3	mgmplusf	|- ( M e. Mgm -> .+^ : ( B X. B ) --> B )
5		frn	|- ( .+^ : ( B X. B ) --> B -> ran .+^ C_ B )
6		ssel	|- ( ran .+^ C_ B -> ( (/) e. ran .+^ -> (/) e. B ) )
7	6	nelcon3d	|- ( ran .+^ C_ B -> ( (/) e/ B -> (/) e/ ran .+^ ) )
8	4 5 7	3syl	|- ( M e. Mgm -> ( (/) e/ B -> (/) e/ ran .+^ ) )
9	8	imp	|- ( ( M e. Mgm /\ (/) e/ B ) -> (/) e/ ran .+^ )
10	1 2 3	plusfreseq	|- ( (/) e/ ran .+^ -> ( .+ |` ( B X. B ) ) = .+^ )
11	9 10	syl	|- ( ( M e. Mgm /\ (/) e/ B ) -> ( .+ |` ( B X. B ) ) = .+^ )