Metamath Proof Explorer


Theorem resmhm2b

Description: Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 resmhm2.u 𝑈 = ( 𝑇s 𝑋 )
2 mhmrcl1 ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑆 ∈ Mnd )
3 2 adantl ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑆 ∈ Mnd )
4 1 submmnd ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → 𝑈 ∈ Mnd )
5 4 ad2antrr ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑈 ∈ Mnd )
6 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
8 6 7 mhmf ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
9 8 adantl ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
10 9 ffnd ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
11 simplr ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → ran 𝐹𝑋 )
12 df-f ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝑋 ↔ ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ ran 𝐹𝑋 ) )
13 10 11 12 sylanbrc ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝑋 )
14 1 submbas ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → 𝑋 = ( Base ‘ 𝑈 ) )
15 14 ad2antrr ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑋 = ( Base ‘ 𝑈 ) )
16 15 feq3d ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝑋𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ) )
17 13 16 mpbid ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) )
18 eqid ( +g𝑆 ) = ( +g𝑆 )
19 eqid ( +g𝑇 ) = ( +g𝑇 )
20 6 18 19 mhmlin ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
21 20 3expb ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
22 21 adantll ( ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
23 1 19 ressplusg ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → ( +g𝑇 ) = ( +g𝑈 ) )
24 23 ad3antrrr ( ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( +g𝑇 ) = ( +g𝑈 ) )
25 24 oveqd ( ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) )
26 22 25 eqtrd ( ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) )
27 26 ralrimivva ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) )
28 eqid ( 0g𝑆 ) = ( 0g𝑆 )
29 eqid ( 0g𝑇 ) = ( 0g𝑇 )
30 28 29 mhm0 ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑇 ) )
31 30 adantl ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑇 ) )
32 1 29 subm0 ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) → ( 0g𝑇 ) = ( 0g𝑈 ) )
33 32 ad2antrr ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 0g𝑇 ) = ( 0g𝑈 ) )
34 31 33 eqtrd ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑈 ) )
35 17 27 34 3jca ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑈 ) ) )
36 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
37 eqid ( +g𝑈 ) = ( +g𝑈 )
38 eqid ( 0g𝑈 ) = ( 0g𝑈 )
39 6 36 18 37 28 38 ismhm ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑈 ∈ Mnd ) ∧ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑈 ) ) ) )
40 3 5 35 39 syl21anbrc ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) )
41 1 resmhm2 ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )
42 41 ancoms ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )
43 42 adantlr ( ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )
44 40 43 impbida ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) → ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ) )