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 ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
lssnlm.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lssnlm ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmMod )

Proof

Step Hyp Ref Expression
1 lssnlm.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 lssnlm.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
4 nlmlmod ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ LMod )
5 2 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
6 4 5 sylan ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
7 1 subgngp ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑋 ∈ NrmGrp )
8 3 6 7 syl2an2r ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmGrp )
9 1 2 lsslmod ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LMod )
10 4 9 sylan ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LMod )
11 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12 1 11 resssca ⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
13 12 adantl ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
14 11 nlmnrg ⊢ ( 𝑊 ∈ NrmMod → ( Scalar ‘ 𝑊 ) ∈ NrmRing )
15 14 adantr ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) ∈ NrmRing )
16 13 15 eqeltrrd ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑋 ) ∈ NrmRing )
17 8 10 16 3jca ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ NrmGrp ∧ 𝑋 ∈ LMod ∧ ( Scalar ‘ 𝑋 ) ∈ NrmRing ) )
18 simpll ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑊 ∈ NrmMod )
19 simprl ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) )
20 13 adantr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
21 20 fveq2d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑋 ) ) )
22 19 21 eleqtrrd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23 6 adantr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
24 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
25 24 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
26 23 25 syl ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
27 simprr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑋 ) )
28 1 subgbas ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) )
29 23 28 syl ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑈 = ( Base ‘ 𝑋 ) )
30 27 29 eleqtrrd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑦 ∈ 𝑈 )
31 26 30 sseldd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
32 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
33 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
34 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
35 eqid ⊢ ( norm ‘ ( Scalar ‘ 𝑊 ) ) = ( norm ‘ ( Scalar ‘ 𝑊 ) )
36 24 32 33 11 34 35 nmvs ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ( norm ‘ 𝑊 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑥 ) · ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) ) )
37 18 22 31 36 syl3anc ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( norm ‘ 𝑊 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑥 ) · ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) ) )
38 simplr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑈 ∈ 𝑆 )
39 1 33 ressvsca ⊢ ( 𝑈 ∈ 𝑆 → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑋 ) )
40 38 39 syl ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑋 ) )
41 40 oveqd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑋 ) 𝑦 ) )
42 41 fveq2d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( norm ‘ 𝑋 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( ( norm ‘ 𝑋 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑋 ) 𝑦 ) ) )
43 4 ad2antrr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑊 ∈ LMod )
44 11 33 34 2 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 )
45 43 38 22 30 44 syl22anc ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 )
46 eqid ⊢ ( norm ‘ 𝑋 ) = ( norm ‘ 𝑋 )
47 1 32 46 subgnm2 ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 ) → ( ( norm ‘ 𝑋 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( ( norm ‘ 𝑊 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) )
48 6 45 47 syl2an2r ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( norm ‘ 𝑋 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( ( norm ‘ 𝑊 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) )
49 42 48 eqtr3d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( norm ‘ 𝑋 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑋 ) 𝑦 ) ) = ( ( norm ‘ 𝑊 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) )
50 20 eqcomd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑊 ) )
51 50 fveq2d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( norm ‘ ( Scalar ‘ 𝑋 ) ) = ( norm ‘ ( Scalar ‘ 𝑊 ) ) )
52 51 fveq1d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( norm ‘ ( Scalar ‘ 𝑋 ) ) ‘ 𝑥 ) = ( ( norm ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑥 ) )
53 1 32 46 subgnm2 ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑦 ∈ 𝑈 ) → ( ( norm ‘ 𝑋 ) ‘ 𝑦 ) = ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) )
54 6 30 53 syl2an2r ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( norm ‘ 𝑋 ) ‘ 𝑦 ) = ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) )
55 52 54 oveq12d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( ( norm ‘ ( Scalar ‘ 𝑋 ) ) ‘ 𝑥 ) · ( ( norm ‘ 𝑋 ) ‘ 𝑦 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑥 ) · ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) ) )
56 37 49 55 3eqtr4d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( norm ‘ 𝑋 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑋 ) 𝑦 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑋 ) ) ‘ 𝑥 ) · ( ( norm ‘ 𝑋 ) ‘ 𝑦 ) ) )
57 56 ralrimivva ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) ( ( norm ‘ 𝑋 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑋 ) 𝑦 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑋 ) ) ‘ 𝑥 ) · ( ( norm ‘ 𝑋 ) ‘ 𝑦 ) ) )
58 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
59 eqid ⊢ ( ·𝑠 ‘ 𝑋 ) = ( ·𝑠 ‘ 𝑋 )
60 eqid ⊢ ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑋 )
61 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑋 ) ) = ( Base ‘ ( Scalar ‘ 𝑋 ) )
62 eqid ⊢ ( norm ‘ ( Scalar ‘ 𝑋 ) ) = ( norm ‘ ( Scalar ‘ 𝑋 ) )
63 58 46 59 60 61 62 isnlm ⊢ ( 𝑋 ∈ NrmMod ↔ ( ( 𝑋 ∈ NrmGrp ∧ 𝑋 ∈ LMod ∧ ( Scalar ‘ 𝑋 ) ∈ NrmRing ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) ( ( norm ‘ 𝑋 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑋 ) 𝑦 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑋 ) ) ‘ 𝑥 ) · ( ( norm ‘ 𝑋 ) ‘ 𝑦 ) ) ) )
64 17 57 63 sylanbrc ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmMod )