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

Metamath Proof Explorer

Theorem mhmvlin

Description: Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses mhmvlin.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
mhmvlin.p ⊢ + = ( +g ‘ 𝑀 )
mhmvlin.q ⊢ ⨣ = ( +g ‘ 𝑁 )
Assertion mhmvlin ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝐹 ∘ ( 𝑋 ∘f + 𝑌 ) ) = ( ( 𝐹 ∘ 𝑋 ) ∘f ⨣ ( 𝐹 ∘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mhmvlin.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 mhmvlin.p ⊢ + = ( +g ‘ 𝑀 )
3 mhmvlin.q ⊢ ⨣ = ( +g ‘ 𝑁 )
4 simpl1 ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )
5 elmapi ⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑋 : 𝐼 ⟶ 𝐵 )
6 5 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑋 : 𝐼 ⟶ 𝐵 )
7 6 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑦 ) ∈ 𝐵 )
8 elmapi ⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑌 : 𝐼 ⟶ 𝐵 )
9 8 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑌 : 𝐼 ⟶ 𝐵 )
10 9 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑦 ) ∈ 𝐵 )
11 1 2 3 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ ( 𝑋 ‘ 𝑦 ) ∈ 𝐵 ∧ ( 𝑌 ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 ‘ 𝑦 ) ) ⨣ ( 𝐹 ‘ ( 𝑌 ‘ 𝑦 ) ) ) )
12 4 7 10 11 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝐹 ‘ ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 ‘ 𝑦 ) ) ⨣ ( 𝐹 ‘ ( 𝑌 ‘ 𝑦 ) ) ) )
13 12 mpteq2dva ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝐹 ‘ ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝐹 ‘ ( 𝑋 ‘ 𝑦 ) ) ⨣ ( 𝐹 ‘ ( 𝑌 ‘ 𝑦 ) ) ) ) )
14 mhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) → 𝑀 ∈ Mnd )
15 14 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑀 ∈ Mnd )
16 15 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑀 ∈ Mnd )
17 1 2 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑋 ‘ 𝑦 ) ∈ 𝐵 ∧ ( 𝑌 ‘ 𝑦 ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) ∈ 𝐵 )
18 16 7 10 17 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) ∈ 𝐵 )
19 elmapex ⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) → ( 𝐵 ∈ V ∧ 𝐼 ∈ V ) )
20 19 simprd ⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) → 𝐼 ∈ V )
21 20 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝐼 ∈ V )
22 6 feqmptd ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑋 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) )
23 9 feqmptd ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑌 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑦 ) ) )
24 21 7 10 22 23 offval2 ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f + 𝑌 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) ) )
25 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
26 1 25 mhmf ⊢ ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑁 ) )
27 26 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑁 ) )
28 27 feqmptd ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝐹 = ( 𝑧 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑧 ) ) )
29 fveq2 ⊢ ( 𝑧 = ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) ) )
30 18 24 28 29 fmptco ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝐹 ∘ ( 𝑋 ∘f + 𝑌 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝐹 ‘ ( ( 𝑋 ‘ 𝑦 ) + ( 𝑌 ‘ 𝑦 ) ) ) ) )
31 fvexd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝐹 ‘ ( 𝑋 ‘ 𝑦 ) ) ∈ V )
32 fvexd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝐹 ‘ ( 𝑌 ‘ 𝑦 ) ) ∈ V )
33 fcompt ⊢ ( ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑁 ) ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑋 ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝐹 ‘ ( 𝑋 ‘ 𝑦 ) ) ) )
34 27 6 33 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝐹 ∘ 𝑋 ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝐹 ‘ ( 𝑋 ‘ 𝑦 ) ) ) )
35 fcompt ⊢ ( ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑁 ) ∧ 𝑌 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑌 ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝐹 ‘ ( 𝑌 ‘ 𝑦 ) ) ) )
36 27 9 35 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝐹 ∘ 𝑌 ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝐹 ‘ ( 𝑌 ‘ 𝑦 ) ) ) )
37 21 31 32 34 36 offval2 ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ( 𝐹 ∘ 𝑋 ) ∘f ⨣ ( 𝐹 ∘ 𝑌 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝐹 ‘ ( 𝑋 ‘ 𝑦 ) ) ⨣ ( 𝐹 ‘ ( 𝑌 ‘ 𝑦 ) ) ) ) )
38 13 30 37 3eqtr4d ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝐹 ∘ ( 𝑋 ∘f + 𝑌 ) ) = ( ( 𝐹 ∘ 𝑋 ) ∘f ⨣ ( 𝐹 ∘ 𝑌 ) ) )