Metamath Proof Explorer

Theorem resmgmhm2b

Description: Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis resmgmhm2.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
Assertion resmgmhm2b ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 resmgmhm2.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
2 mgmhmrcl ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
3 2 simpld ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝑆 ∈ Mgm )
4 3 adantl ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝑆 ∈ Mgm )
5 1 submgmmgm ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) → 𝑈 ∈ Mgm )
6 5 ad2antrr ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝑈 ∈ Mgm )
7 4 6 jca ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( 𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm ) )
8 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
10 8 9 mgmhmf ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
11 10 adantl ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
12 11 ffnd ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
13 simplr ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ran 𝐹 ⊆ 𝑋 )
14 df-f ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝑋 ↔ ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ ran 𝐹 ⊆ 𝑋 ) )
15 12 13 14 sylanbrc ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝑋 )
16 1 submgmbas ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) → 𝑋 = ( Base ‘ 𝑈 ) )
17 16 ad2antrr ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝑋 = ( Base ‘ 𝑈 ) )
18 17 feq3d ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝑋 ↔ 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ) )
19 15 18 mpbid ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) )
20 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
21 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
22 8 20 21 mgmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
23 22 3expb ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
24 23 adantll ⊢ ( ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
25 1 21 ressplusg ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) → ( +g ‘ 𝑇 ) = ( +g ‘ 𝑈 ) )
26 25 ad3antrrr ⊢ ( ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( +g ‘ 𝑇 ) = ( +g ‘ 𝑈 ) )
27 26 oveqd ⊢ ( ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
28 24 27 eqtrd ⊢ ( ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
29 28 ralrimivva ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
30 19 29 jca ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ) )
31 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
32 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
33 8 31 20 32 ismgmhm ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm ) ∧ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
34 7 30 33 sylanbrc ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) )
35 1 resmgmhm2 ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) )
36 35 ancoms ⊢ ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) )
37 36 adantlr ⊢ ( ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ∧ 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) )
38 34 37 impbida ⊢ ( ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ) )