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 âĻĢ ( ðđ ∘ 𝑌 ) ) )