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 ⊢ U = LSubSp ⁡ S
reslmhm.r ⊢ R = S ↾ 𝑠 X
Assertion reslmhm ⊢ F ∈ S LMHom T ∧ X ∈ U → F ↾ X ∈ R LMHom T

Proof

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