Metamath Proof Explorer

Theorem reslmhm

Description: Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses reslmhm.u ⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
reslmhm.r ⊢ 𝑅 = ( 𝑆 ↾s 𝑋 )
Assertion reslmhm ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 LMHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 reslmhm.u ⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
2 reslmhm.r ⊢ 𝑅 = ( 𝑆 ↾s 𝑋 )
3 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
4 2 1 lsslmod ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈 ) → 𝑅 ∈ LMod )
5 3 4 sylan ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑅 ∈ LMod )
6 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
7 6 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑇 ∈ LMod )
8 lmghm ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
9 1 lsssubg ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( SubGrp ‘ 𝑆 ) )
10 3 9 sylan ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( SubGrp ‘ 𝑆 ) )
11 2 resghm ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 GrpHom 𝑇 ) )
12 8 10 11 syl2an2r ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 GrpHom 𝑇 ) )
13 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
14 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
15 13 14 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
16 2 13 resssca ⊢ ( 𝑋 ∈ 𝑈 → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑅 ) )
17 15 16 sylan9eq ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑅 ) )
18 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
19 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
20 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21 20 1 lssss ⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
22 21 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
23 22 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
24 2 20 ressbas2 ⊢ ( 𝑋 ⊆ ( Base ‘ 𝑆 ) → 𝑋 = ( Base ‘ 𝑅 ) )
25 22 24 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 = ( Base ‘ 𝑅 ) )
26 25 eleq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝑏 ∈ 𝑋 ↔ 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
27 26 biimpar ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → 𝑏 ∈ 𝑋 )
28 27 adantrl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑏 ∈ 𝑋 )
29 23 28 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
30 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
31 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
32 eqid ⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
33 13 30 20 31 32 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
34 18 19 29 33 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
35 3 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑆 ∈ LMod )
36 35 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑆 ∈ LMod )
37 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑋 ∈ 𝑈 )
38 13 31 30 1 lssvscl ⊢ ( ( ( 𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ 𝑋 )
39 36 37 19 28 38 syl22anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ 𝑋 )
40 39 fvresd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) )
41 fvres ⊢ ( 𝑏 ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
42 41 oveq2d ⊢ ( 𝑏 ∈ 𝑋 → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
43 28 42 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
44 34 40 43 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) )
45 44 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) )
46 16 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑅 ) )
47 46 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) ) )
48 2 31 ressvsca ⊢ ( 𝑋 ∈ 𝑈 → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑅 ) )
49 48 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑅 ) )
50 49 oveqd ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) = ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) )
51 50 fveqeq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ↔ ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) )
52 51 ralbidv ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) )
53 47 52 raleqbidv ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) )
54 45 53 mpbid ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) )
55 12 17 54 3jca ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 GrpHom 𝑇 ) ∧ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) )
56 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
57 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑅 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
58 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
59 eqid ⊢ ( ·𝑠 ‘ 𝑅 ) = ( ·𝑠 ‘ 𝑅 )
60 56 14 57 58 59 32 islmhm ⊢ ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 LMHom 𝑇 ) ↔ ( ( 𝑅 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 GrpHom 𝑇 ) ∧ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) ) )
61 5 7 55 60 syl21anbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 LMHom 𝑇 ) )