Metamath Proof Explorer

Theorem mhmlin

Description: A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 mhmlin.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 mhmlin.p ⊢ + = ( +g ‘ 𝑆 )
3 mhmlin.q ⊢ ⨣ = ( +g ‘ 𝑇 )
4 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
5 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
6 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
7 1 4 2 3 5 6 ismhm ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) ) ) )
8 7 simprbi ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) ) )
9 8 simp2d ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
10 fvoveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) )
11 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
12 11 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
13 10 12 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) )
14 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 + 𝑦 ) = ( 𝑋 + 𝑌 ) )
15 14 fveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) )
16 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
17 16 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) )
18 15 17 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) ) )
19 13 18 rspc2v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) ) )
20 9 19 syl5com ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) ) )
21 20 3impib ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) )