This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )