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

Metamath Proof Explorer

Theorem resmgmhm

Description: Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 resmgmhm.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑋 )
2 mgmhmrcl ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
3 2 simprd ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝑇 ∈ Mgm )
4 1 submgmmgm ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → 𝑈 ∈ Mgm )
5 3 4 anim12ci ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝑈 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
6 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
8 6 7 mgmhmf ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
9 6 submgmss ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
10 fssres ⊢ ( ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) )
11 8 9 10 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) )
12 9 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
13 1 6 ressbas2 ⊢ ( 𝑋 ⊆ ( Base ‘ 𝑆 ) → 𝑋 = ( Base ‘ 𝑈 ) )
14 12 13 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → 𝑋 = ( Base ‘ 𝑈 ) )
15 14 feq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) ↔ ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ) )
16 11 15 mpbid ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) )
17 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) )
18 9 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
19 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
20 18 19 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
21 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
22 18 21 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
23 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
24 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
25 6 23 24 mgmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
26 17 20 22 25 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
27 23 submgmcl ⊢ ( ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 )
28 27 3expb ⊢ ( ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 )
29 28 adantll ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 )
30 fvres ⊢ ( ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
31 29 30 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
32 fvres ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
33 fvres ⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
34 32 33 oveqan12d ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
35 34 adantl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
36 26 31 35 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) )
37 36 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) )
38 1 23 ressplusg ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑈 ) )
39 38 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑈 ) )
40 39 oveqd ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) )
41 40 fveqeq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
42 14 41 raleqbidv ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
43 14 42 raleqbidv ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
44 37 43 mpbid ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) )
45 16 44 jca ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
46 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
47 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
48 46 7 47 24 ismgmhm ⊢ ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 MgmHom 𝑇 ) ↔ ( ( 𝑈 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) ) )
49 5 45 48 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 MgmHom 𝑇 ) )