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

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 𝑈 ) ) )