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

Metamath Proof Explorer

Theorem mgmhmlin

Description: A magma homomorphism preserves the binary operation. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmhmlin.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
mgmhmlin.p ⊢ + = ( +g ‘ 𝑆 )
mgmhmlin.q ⊢ ⨣ = ( +g ‘ 𝑇 )
Assertion mgmhmlin ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mgmhmlin.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 mgmhmlin.p ⊢ + = ( +g ‘ 𝑆 )
3 mgmhmlin.q ⊢ ⨣ = ( +g ‘ 𝑇 )
4 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
5 1 4 2 3 ismgmhm ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ) )
6 fvoveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
8 7 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
9 6 8 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) )
10 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 + 𝑦 ) = ( 𝑋 + 𝑌 ) )
11 10 fveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) )
12 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
13 12 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) )
14 11 13 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) ) )
15 9 14 rspc2v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) ) )
16 15 com12 ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) ) )
17 16 ad2antll ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) ) )
18 5 17 sylbi ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) ) )
19 18 3impib ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) )