Theorem mgmplusf

Description: The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015) (Revisd by AV, 28-Jan-2020.)

	Ref	Expression
Hypotheses	mgmplusf.1	⊢ 𝐵 = ( Base ‘ 𝑀 )
	mgmplusf.2	⊢ ⨣ = ( +𝑓 ‘ 𝑀 )
Assertion	mgmplusf	⊢ ( 𝑀 ∈ Mgm → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mgmplusf.1	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		mgmplusf.2	⊢ ⨣ = ( +𝑓 ‘ 𝑀 )
3		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
4	1 3	mgmcl	⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
5	4	3expb	⊢ ( ( 𝑀 ∈ Mgm ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
6	5	ralrimivva	⊢ ( 𝑀 ∈ Mgm → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
7	1 3 2	plusffval	⊢ ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
8	7	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 ↔ ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
9	6 8	sylib	⊢ ( 𝑀 ∈ Mgm → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )