Metamath Proof Explorer

Theorem lssnlm

Description: A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses lssnlm.x 
|- X = ( W |`s U )
lssnlm.s 
|- S = ( LSubSp ` W )
Assertion lssnlm 
|- ( ( W e. NrmMod /\ U e. S ) -> X e. NrmMod )

Proof

Step Hyp Ref Expression
1 lssnlm.x 
 |-  X = ( W |`s U )
2 lssnlm.s 
 |-  S = ( LSubSp ` W )
3 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
4 nlmlmod 
 |-  ( W e. NrmMod -> W e. LMod )
5 2 lsssubg 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
6 4 5 sylan 
 |-  ( ( W e. NrmMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
7 1 subgngp 
 |-  ( ( W e. NrmGrp /\ U e. ( SubGrp ` W ) ) -> X e. NrmGrp )
8 3 6 7 syl2an2r 
 |-  ( ( W e. NrmMod /\ U e. S ) -> X e. NrmGrp )
9 1 2 lsslmod 
 |-  ( ( W e. LMod /\ U e. S ) -> X e. LMod )
10 4 9 sylan 
 |-  ( ( W e. NrmMod /\ U e. S ) -> X e. LMod )
11 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
12 1 11 resssca 
 |-  ( U e. S -> ( Scalar ` W ) = ( Scalar ` X ) )
13 12 adantl 
 |-  ( ( W e. NrmMod /\ U e. S ) -> ( Scalar ` W ) = ( Scalar ` X ) )
14 11 nlmnrg 
 |-  ( W e. NrmMod -> ( Scalar ` W ) e. NrmRing )
15 14 adantr 
 |-  ( ( W e. NrmMod /\ U e. S ) -> ( Scalar ` W ) e. NrmRing )
16 13 15 eqeltrrd 
 |-  ( ( W e. NrmMod /\ U e. S ) -> ( Scalar ` X ) e. NrmRing )
17 8 10 16 3jca 
 |-  ( ( W e. NrmMod /\ U e. S ) -> ( X e. NrmGrp /\ X e. LMod /\ ( Scalar ` X ) e. NrmRing ) )
18 simpll 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> W e. NrmMod )
19 simprl 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> x e. ( Base ` ( Scalar ` X ) ) )
20 13 adantr 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( Scalar ` W ) = ( Scalar ` X ) )
21 20 fveq2d 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` X ) ) )
22 19 21 eleqtrrd 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> x e. ( Base ` ( Scalar ` W ) ) )
23 6 adantr 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> U e. ( SubGrp ` W ) )
24 eqid 
 |-  ( Base ` W ) = ( Base ` W )
25 24 subgss 
 |-  ( U e. ( SubGrp ` W ) -> U C_ ( Base ` W ) )
26 23 25 syl 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> U C_ ( Base ` W ) )
27 simprr 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> y e. ( Base ` X ) )
28 1 subgbas 
 |-  ( U e. ( SubGrp ` W ) -> U = ( Base ` X ) )
29 23 28 syl 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> U = ( Base ` X ) )
30 27 29 eleqtrrd 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> y e. U )
31 26 30 sseldd 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> y e. ( Base ` W ) )
32 eqid 
 |-  ( norm ` W ) = ( norm ` W )
33 eqid 
 |-  ( .s ` W ) = ( .s ` W )
34 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
35 eqid 
 |-  ( norm ` ( Scalar ` W ) ) = ( norm ` ( Scalar ` W ) )
36 24 32 33 11 34 35 nmvs 
 |-  ( ( W e. NrmMod /\ x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) -> ( ( norm ` W ) ` ( x ( .s ` W ) y ) ) = ( ( ( norm ` ( Scalar ` W ) ) ` x ) x. ( ( norm ` W ) ` y ) ) )
37 18 22 31 36 syl3anc 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( ( norm ` W ) ` ( x ( .s ` W ) y ) ) = ( ( ( norm ` ( Scalar ` W ) ) ` x ) x. ( ( norm ` W ) ` y ) ) )
38 simplr 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> U e. S )
39 1 33 ressvsca 
 |-  ( U e. S -> ( .s ` W ) = ( .s ` X ) )
40 38 39 syl 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( .s ` W ) = ( .s ` X ) )
41 40 oveqd 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( x ( .s ` W ) y ) = ( x ( .s ` X ) y ) )
42 41 fveq2d 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( ( norm ` X ) ` ( x ( .s ` W ) y ) ) = ( ( norm ` X ) ` ( x ( .s ` X ) y ) ) )
43 4 ad2antrr 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> W e. LMod )
44 11 33 34 2 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. U ) ) -> ( x ( .s ` W ) y ) e. U )
45 43 38 22 30 44 syl22anc 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( x ( .s ` W ) y ) e. U )
46 eqid 
 |-  ( norm ` X ) = ( norm ` X )
47 1 32 46 subgnm2 
 |-  ( ( U e. ( SubGrp ` W ) /\ ( x ( .s ` W ) y ) e. U ) -> ( ( norm ` X ) ` ( x ( .s ` W ) y ) ) = ( ( norm ` W ) ` ( x ( .s ` W ) y ) ) )
48 6 45 47 syl2an2r 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( ( norm ` X ) ` ( x ( .s ` W ) y ) ) = ( ( norm ` W ) ` ( x ( .s ` W ) y ) ) )
49 42 48 eqtr3d 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( ( norm ` X ) ` ( x ( .s ` X ) y ) ) = ( ( norm ` W ) ` ( x ( .s ` W ) y ) ) )
50 20 eqcomd 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( Scalar ` X ) = ( Scalar ` W ) )
51 50 fveq2d 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( norm ` ( Scalar ` X ) ) = ( norm ` ( Scalar ` W ) ) )
52 51 fveq1d 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( ( norm ` ( Scalar ` X ) ) ` x ) = ( ( norm ` ( Scalar ` W ) ) ` x ) )
53 1 32 46 subgnm2 
 |-  ( ( U e. ( SubGrp ` W ) /\ y e. U ) -> ( ( norm ` X ) ` y ) = ( ( norm ` W ) ` y ) )
54 6 30 53 syl2an2r 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( ( norm ` X ) ` y ) = ( ( norm ` W ) ` y ) )
55 52 54 oveq12d 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( ( ( norm ` ( Scalar ` X ) ) ` x ) x. ( ( norm ` X ) ` y ) ) = ( ( ( norm ` ( Scalar ` W ) ) ` x ) x. ( ( norm ` W ) ` y ) ) )
56 37 49 55 3eqtr4d 
 |-  ( ( ( W e. NrmMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ y e. ( Base ` X ) ) ) -> ( ( norm ` X ) ` ( x ( .s ` X ) y ) ) = ( ( ( norm ` ( Scalar ` X ) ) ` x ) x. ( ( norm ` X ) ` y ) ) )
57 56 ralrimivva 
 |-  ( ( W e. NrmMod /\ U e. S ) -> A. x e. ( Base ` ( Scalar ` X ) ) A. y e. ( Base ` X ) ( ( norm ` X ) ` ( x ( .s ` X ) y ) ) = ( ( ( norm ` ( Scalar ` X ) ) ` x ) x. ( ( norm ` X ) ` y ) ) )
58 eqid 
 |-  ( Base ` X ) = ( Base ` X )
59 eqid 
 |-  ( .s ` X ) = ( .s ` X )
60 eqid 
 |-  ( Scalar ` X ) = ( Scalar ` X )
61 eqid 
 |-  ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` X ) )
62 eqid 
 |-  ( norm ` ( Scalar ` X ) ) = ( norm ` ( Scalar ` X ) )
63 58 46 59 60 61 62 isnlm 
 |-  ( X e. NrmMod <-> ( ( X e. NrmGrp /\ X e. LMod /\ ( Scalar ` X ) e. NrmRing ) /\ A. x e. ( Base ` ( Scalar ` X ) ) A. y e. ( Base ` X ) ( ( norm ` X ) ` ( x ( .s ` X ) y ) ) = ( ( ( norm ` ( Scalar ` X ) ) ` x ) x. ( ( norm ` X ) ` y ) ) ) )
64 17 57 63 sylanbrc 
 |-  ( ( W e. NrmMod /\ U e. S ) -> X e. NrmMod )