Metamath Proof Explorer

Theorem resmhm2

Description: One direction of resmhm2b . (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypothesis resmhm2.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
Assertion resmhm2 ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 resmhm2.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
2 mhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) → 𝑆 ∈ Mnd )
3 submrcl ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → 𝑇 ∈ Mnd )
4 2 3 anim12i ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) )
5 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
7 5 6 mhmf ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) )
8 1 submbas ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → 𝑋 = ( Base ‘ 𝑈 ) )
9 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
10 9 submss ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → 𝑋 ⊆ ( Base ‘ 𝑇 ) )
11 8 10 eqsstrrd ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑇 ) )
12 fss ⊢ ( ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
13 7 11 12 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
14 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
15 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
16 5 14 15 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
17 16 3expb ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
18 17 adantlr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
19 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
20 1 19 ressplusg ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → ( +g ‘ 𝑇 ) = ( +g ‘ 𝑈 ) )
21 20 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( +g ‘ 𝑇 ) = ( +g ‘ 𝑈 ) )
22 21 oveqd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
23 18 22 eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
24 23 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
25 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
26 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
27 25 26 mhm0 ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑈 ) )
28 27 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑈 ) )
29 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
30 1 29 subm0 ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑈 ) )
31 30 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑈 ) )
32 28 31 eqtr4d ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
33 13 24 32 3jca ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) ) )
34 5 9 14 19 25 29 ismhm ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) ) ) )
35 4 33 34 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )