| Step | Hyp | Ref
| Expression |
| 1 | | nlmngp 24698 |
. . . 4
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
| 2 | | nlmlmod 24699 |
. . . . 5
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod) |
| 3 | | lssnlm.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑊) |
| 4 | 3 | lsssubg 20955 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 5 | 2, 4 | sylan 580 |
. . . 4
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 6 | | lssnlm.x |
. . . . 5
⊢ 𝑋 = (𝑊 ↾s 𝑈) |
| 7 | 6 | subgngp 24648 |
. . . 4
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑈 ∈ (SubGrp‘𝑊)) → 𝑋 ∈ NrmGrp) |
| 8 | 1, 5, 7 | syl2an2r 685 |
. . 3
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmGrp) |
| 9 | 6, 3 | lsslmod 20958 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod) |
| 10 | 2, 9 | sylan 580 |
. . 3
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod) |
| 11 | | eqid 2737 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 12 | 6, 11 | resssca 17387 |
. . . . 5
⊢ (𝑈 ∈ 𝑆 → (Scalar‘𝑊) = (Scalar‘𝑋)) |
| 13 | 12 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → (Scalar‘𝑊) = (Scalar‘𝑋)) |
| 14 | 11 | nlmnrg 24700 |
. . . . 5
⊢ (𝑊 ∈ NrmMod →
(Scalar‘𝑊) ∈
NrmRing) |
| 15 | 14 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → (Scalar‘𝑊) ∈ NrmRing) |
| 16 | 13, 15 | eqeltrrd 2842 |
. . 3
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → (Scalar‘𝑋) ∈ NrmRing) |
| 17 | 8, 10, 16 | 3jca 1129 |
. 2
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ NrmGrp ∧ 𝑋 ∈ LMod ∧ (Scalar‘𝑋) ∈
NrmRing)) |
| 18 | | simpll 767 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑊 ∈ NrmMod) |
| 19 | | simprl 771 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑥 ∈ (Base‘(Scalar‘𝑋))) |
| 20 | 13 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (Scalar‘𝑊) = (Scalar‘𝑋)) |
| 21 | 20 | fveq2d 6910 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑋))) |
| 22 | 19, 21 | eleqtrrd 2844 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
| 23 | 5 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 24 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 25 | 24 | subgss 19145 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝑊) → 𝑈 ⊆ (Base‘𝑊)) |
| 26 | 23, 25 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑈 ⊆ (Base‘𝑊)) |
| 27 | | simprr 773 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑦 ∈ (Base‘𝑋)) |
| 28 | 6 | subgbas 19148 |
. . . . . . . 8
⊢ (𝑈 ∈ (SubGrp‘𝑊) → 𝑈 = (Base‘𝑋)) |
| 29 | 23, 28 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑈 = (Base‘𝑋)) |
| 30 | 27, 29 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑦 ∈ 𝑈) |
| 31 | 26, 30 | sseldd 3984 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑦 ∈ (Base‘𝑊)) |
| 32 | | eqid 2737 |
. . . . . 6
⊢
(norm‘𝑊) =
(norm‘𝑊) |
| 33 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 34 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 35 | | eqid 2737 |
. . . . . 6
⊢
(norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊)) |
| 36 | 24, 32, 33, 11, 34, 35 | nmvs 24697 |
. . . . 5
⊢ ((𝑊 ∈ NrmMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))) |
| 37 | 18, 22, 31, 36 | syl3anc 1373 |
. . . 4
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))) |
| 38 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑈 ∈ 𝑆) |
| 39 | 6, 33 | ressvsca 17388 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑆 → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) |
| 40 | 38, 39 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) |
| 41 | 40 | oveqd 7448 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (𝑥( ·𝑠
‘𝑊)𝑦) = (𝑥( ·𝑠
‘𝑋)𝑦)) |
| 42 | 41 | fveq2d 6910 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦))) |
| 43 | 2 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → 𝑊 ∈ LMod) |
| 44 | 11, 33, 34, 3 | lssvscl 20953 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑈) |
| 45 | 43, 38, 22, 30, 44 | syl22anc 839 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑈) |
| 46 | | eqid 2737 |
. . . . . . 7
⊢
(norm‘𝑋) =
(norm‘𝑋) |
| 47 | 6, 32, 46 | subgnm2 24647 |
. . . . . 6
⊢ ((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑈) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦))) |
| 48 | 5, 45, 47 | syl2an2r 685 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑊)𝑦)) = ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦))) |
| 49 | 42, 48 | eqtr3d 2779 |
. . . 4
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦)) = ((norm‘𝑊)‘(𝑥( ·𝑠
‘𝑊)𝑦))) |
| 50 | 20 | eqcomd 2743 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (Scalar‘𝑋) = (Scalar‘𝑊)) |
| 51 | 50 | fveq2d 6910 |
. . . . . 6
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (norm‘(Scalar‘𝑋)) =
(norm‘(Scalar‘𝑊))) |
| 52 | 51 | fveq1d 6908 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘(Scalar‘𝑋))‘𝑥) = ((norm‘(Scalar‘𝑊))‘𝑥)) |
| 53 | 6, 32, 46 | subgnm2 24647 |
. . . . . 6
⊢ ((𝑈 ∈ (SubGrp‘𝑊) ∧ 𝑦 ∈ 𝑈) → ((norm‘𝑋)‘𝑦) = ((norm‘𝑊)‘𝑦)) |
| 54 | 5, 30, 53 | syl2an2r 685 |
. . . . 5
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘𝑦) = ((norm‘𝑊)‘𝑦)) |
| 55 | 52, 54 | oveq12d 7449 |
. . . 4
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → (((norm‘(Scalar‘𝑋))‘𝑥) · ((norm‘𝑋)‘𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))) |
| 56 | 37, 49, 55 | 3eqtr4d 2787 |
. . 3
⊢ (((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑦 ∈ (Base‘𝑋))) → ((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦)) = (((norm‘(Scalar‘𝑋))‘𝑥) · ((norm‘𝑋)‘𝑦))) |
| 57 | 56 | ralrimivva 3202 |
. 2
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → ∀𝑥 ∈ (Base‘(Scalar‘𝑋))∀𝑦 ∈ (Base‘𝑋)((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦)) = (((norm‘(Scalar‘𝑋))‘𝑥) · ((norm‘𝑋)‘𝑦))) |
| 58 | | eqid 2737 |
. . 3
⊢
(Base‘𝑋) =
(Base‘𝑋) |
| 59 | | eqid 2737 |
. . 3
⊢ (
·𝑠 ‘𝑋) = ( ·𝑠
‘𝑋) |
| 60 | | eqid 2737 |
. . 3
⊢
(Scalar‘𝑋) =
(Scalar‘𝑋) |
| 61 | | eqid 2737 |
. . 3
⊢
(Base‘(Scalar‘𝑋)) = (Base‘(Scalar‘𝑋)) |
| 62 | | eqid 2737 |
. . 3
⊢
(norm‘(Scalar‘𝑋)) = (norm‘(Scalar‘𝑋)) |
| 63 | 58, 46, 59, 60, 61, 62 | isnlm 24696 |
. 2
⊢ (𝑋 ∈ NrmMod ↔ ((𝑋 ∈ NrmGrp ∧ 𝑋 ∈ LMod ∧
(Scalar‘𝑋) ∈
NrmRing) ∧ ∀𝑥
∈ (Base‘(Scalar‘𝑋))∀𝑦 ∈ (Base‘𝑋)((norm‘𝑋)‘(𝑥( ·𝑠
‘𝑋)𝑦)) = (((norm‘(Scalar‘𝑋))‘𝑥) · ((norm‘𝑋)‘𝑦)))) |
| 64 | 17, 57, 63 | sylanbrc 583 |
1
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) |