Step | Hyp | Ref
| Expression |
1 | | nlmngp 22291 |
. . . . 5
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑊 ∈ NrmGrp) |
3 | | nlmlmod 22292 |
. . . . 5
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod) |
4 | | lssnlm.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑊) |
5 | 4 | lsssubg 18778 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
6 | 3, 5 | sylan 487 |
. . . 4
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
7 | | lssnlm.x |
. . . . 5
⊢ 𝑋 = (𝑊 ↾s 𝑈) |
8 | 7 | subgngp 22249 |
. . . 4
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑈 ∈ (SubGrp‘𝑊)) → 𝑋 ∈ NrmGrp) |
9 | 2, 6, 8 | syl2anc 691 |
. . 3
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmGrp) |
10 | 7, 4 | lsslmod 18781 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod) |
11 | 3, 10 | sylan 487 |
. . 3
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod) |
12 | | eqid 2610 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
13 | 7, 12 | resssca 15854 |
. . . . 5
⊢ (𝑈 ∈ 𝑆 → (Scalar‘𝑊) = (Scalar‘𝑋)) |
14 | 13 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → (Scalar‘𝑊) = (Scalar‘𝑋)) |
15 | 12 | nlmnrg 22293 |
. . . . 5
⊢ (𝑊 ∈ NrmMod →
(Scalar‘𝑊) ∈
NrmRing) |
16 | 15 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → (Scalar‘𝑊) ∈ NrmRing) |
17 | 14, 16 | eqeltrrd 2689 |
. . 3
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → (Scalar‘𝑋) ∈ NrmRing) |
18 | 9, 11, 17 | 3jca 1235 |
. 2
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ NrmGrp ∧ 𝑋 ∈ LMod ∧ (Scalar‘𝑋) ∈
NrmRing)) |
19 | | simpll 786 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑊 ∈ NrmMod) |
20 | | simprl 790 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑥 ∈ (Base‘(Scalar‘𝑋))) |
21 | 14 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (Scalar‘𝑊) = (Scalar‘𝑋)) |
22 | 21 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑋))) |
23 | 20, 22 | eleqtrrd 2691 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
24 | 6 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑈 ∈ (SubGrp‘𝑊)) |
25 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑊) =
(Base‘𝑊) |
26 | 25 | subgss 17418 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝑊) → 𝑈 ⊆ (Base‘𝑊)) |
27 | 24, 26 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑈 ⊆ (Base‘𝑊)) |
28 | | simprr 792 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑦 ∈ (Base‘𝑋)) |
29 | 7 | subgbas 17421 |
. . . . . . . 8
⊢ (𝑈 ∈ (SubGrp‘𝑊) → 𝑈 = (Base‘𝑋)) |
30 | 24, 29 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑈 = (Base‘𝑋)) |
31 | 28, 30 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑦 ∈ 𝑈) |
32 | 27, 31 | sseldd 3569 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑦 ∈ (Base‘𝑊)) |
33 | | eqid 2610 |
. . . . . 6
⊢
(norm‘𝑊) =
(norm‘𝑊) |
34 | | eqid 2610 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
35 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
36 | | eqid 2610 |
. . . . . 6
⊢
(norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊)) |
37 | 25, 33, 34, 12, 35, 36 | nmvs 22290 |
. . . . 5
⊢ ((𝑊 ∈ NrmMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))) |
38 | 19, 23, 32, 37 | syl3anc 1318 |
. . . 4
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))) |
39 | | simplr 788 |
. . . . . . . 8
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑈 ∈ 𝑆) |
40 | 7, 34 | ressvsca 15855 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑆 → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) |
41 | 39, 40 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) |
42 | 41 | oveqd 6566 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (𝑥( ·𝑠
‘𝑊)𝑦) = (𝑥( ·𝑠
‘𝑋)𝑦)) |
43 | 42 | fveq2d 6107 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦))) |
44 | 3 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑊 ∈ LMod) |
45 | 12, 34, 35, 4 | lssvscl 18776 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑈) |
46 | 44, 39, 23, 31, 45 | syl22anc 1319 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑈) |
47 | | eqid 2610 |
. . . . . . 7
⊢
(norm‘𝑋) =
(norm‘𝑋) |
48 | 7, 33, 47 | subgnm2 22248 |
. . . . . 6
⊢ ((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑈) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦))) |
49 | 24, 46, 48 | syl2anc 691 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦))) |
50 | 43, 49 | eqtr3d 2646 |
. . . 4
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦)) = ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦))) |
51 | 21 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (Scalar‘𝑋) = (Scalar‘𝑊)) |
52 | 51 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (norm‘(Scalar‘𝑋)) =
(norm‘(Scalar‘𝑊))) |
53 | 52 | fveq1d 6105 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘(Scalar‘𝑋))‘𝑥) = ((norm‘(Scalar‘𝑊))‘𝑥)) |
54 | 7, 33, 47 | subgnm2 22248 |
. . . . . 6
⊢ ((𝑈 ∈ (SubGrp‘𝑊) ∧ 𝑦 ∈ 𝑈) → ((norm‘𝑋)‘𝑦) = ((norm‘𝑊)‘𝑦)) |
55 | 24, 31, 54 | syl2anc 691 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘𝑦) = ((norm‘𝑊)‘𝑦)) |
56 | 53, 55 | oveq12d 6567 |
. . . 4
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (((norm‘(Scalar‘𝑋))‘𝑥) · ((norm‘𝑋)‘𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))) |
57 | 38, 50, 56 | 3eqtr4d 2654 |
. . 3
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦)) = (((norm‘(Scalar‘𝑋))‘𝑥) · ((norm‘𝑋)‘𝑦))) |
58 | 57 | ralrimivva 2954 |
. 2
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → ∀𝑥 ∈ (Base‘(Scalar‘𝑋))∀𝑦 ∈ (Base‘𝑋)((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦)) = (((norm‘(Scalar‘𝑋))‘𝑥) · ((norm‘𝑋)‘𝑦))) |
59 | | eqid 2610 |
. . 3
⊢
(Base‘𝑋) =
(Base‘𝑋) |
60 | | eqid 2610 |
. . 3
⊢ (
·𝑠 ‘𝑋) = ( ·𝑠
‘𝑋) |
61 | | eqid 2610 |
. . 3
⊢
(Scalar‘𝑋) =
(Scalar‘𝑋) |
62 | | eqid 2610 |
. . 3
⊢
(Base‘(Scalar‘𝑋)) = (Base‘(Scalar‘𝑋)) |
63 | | eqid 2610 |
. . 3
⊢
(norm‘(Scalar‘𝑋)) = (norm‘(Scalar‘𝑋)) |
64 | 59, 47, 60, 61, 62, 63 | isnlm 22289 |
. 2
⊢ (𝑋 ∈ NrmMod ↔ ((𝑋 ∈ NrmGrp ∧ 𝑋 ∈ LMod ∧
(Scalar‘𝑋) ∈
NrmRing) ∧ ∀𝑥
∈ (Base‘(Scalar‘𝑋))∀𝑦 ∈ (Base‘𝑋)((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦)) = (((norm‘(Scalar‘𝑋))‘𝑥) · ((norm‘𝑋)‘𝑦)))) |
65 | 18, 58, 64 | sylanbrc 695 |
1
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) |