Metamath Proof Explorer

Theorem resmgmhm2

Description: One direction of resmgmhm2b . (Contributed by AV, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 resmgmhm2.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
2 mgmhmrcl ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) → ( 𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm ) )
3 2 simpld ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) → 𝑆 ∈ Mgm )
4 submgmrcl ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) → 𝑇 ∈ Mgm )
5 3 4 anim12i ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
6 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
8 6 7 mgmhmf ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) )
9 1 submgmbas ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) → 𝑋 = ( Base ‘ 𝑈 ) )
10 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
11 10 submgmss ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) → 𝑋 ⊆ ( Base ‘ 𝑇 ) )
12 9 11 eqsstrrd ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) → ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑇 ) )
13 fss ⊢ ( ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
14 8 12 13 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
15 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
16 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
17 6 15 16 mgmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
18 17 3expb ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
19 18 adantlr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
20 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
21 1 20 ressplusg ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑇 ) → ( +g ‘ 𝑇 ) = ( +g ‘ 𝑈 ) )
22 21 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( +g ‘ 𝑇 ) = ( +g ‘ 𝑈 ) )
23 22 oveqd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
24 19 23 eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
25 24 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
26 14 25 jca ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) → ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) )
27 6 10 15 20 ismgmhm ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
28 5 26 27 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑈 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) )