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 |`s X )
Assertion reslmhm 
|- ( ( F e. ( S LMHom T ) /\ X e. U ) -> ( F |` X ) e. ( R LMHom T ) )

Proof

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