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 ffvelrnda ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵m 𝐼 ) ) ∧ 𝑦𝐼 ) → ( 𝑋𝑦 ) ∈ 𝐵 )
8 elmapi ( 𝑌 ∈ ( 𝐵m 𝐼 ) → 𝑌 : 𝐼𝐵 )
9 8 3ad2ant3 ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( 𝐵m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵m 𝐼 ) ) → 𝑌 : 𝐼𝐵 )
10 9 ffvelrnda ( ( ( 𝐹 ∈ ( 𝑀 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 ( 𝐹𝑌 ) ) )