| Step | Hyp | Ref
| Expression |
| 1 | | nrgngp 24683 |
. . . . 5
⊢ (𝑊 ∈ NrmRing → 𝑊 ∈ NrmGrp) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝑊 ∈ NrmGrp) |
| 3 | | eqidd 2738 |
. . . . 5
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (Base‘𝑊) = (Base‘𝑊)) |
| 4 | | sranlm.a |
. . . . . . 7
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) |
| 5 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
| 6 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 7 | 6 | subrgss 20572 |
. . . . . . 7
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 ⊆ (Base‘𝑊)) |
| 8 | 7 | adantl 481 |
. . . . . 6
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝑆 ⊆ (Base‘𝑊)) |
| 9 | 5, 8 | srabase 21177 |
. . . . 5
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (Base‘𝑊) = (Base‘𝐴)) |
| 10 | 5, 8 | sraaddg 21179 |
. . . . . 6
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) →
(+g‘𝑊) =
(+g‘𝐴)) |
| 11 | 10 | oveqdr 7459 |
. . . . 5
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝑥(+g‘𝑊)𝑦) = (𝑥(+g‘𝐴)𝑦)) |
| 12 | 5, 8 | srads 21191 |
. . . . . 6
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (dist‘𝑊) = (dist‘𝐴)) |
| 13 | 12 | reseq1d 5996 |
. . . . 5
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) = ((dist‘𝐴) ↾ ((Base‘𝑊) × (Base‘𝑊)))) |
| 14 | 5, 8 | sratopn 21190 |
. . . . 5
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (TopOpen‘𝑊) = (TopOpen‘𝐴)) |
| 15 | 3, 9, 11, 13, 14 | ngppropd 24650 |
. . . 4
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (𝑊 ∈ NrmGrp ↔ 𝐴 ∈ NrmGrp)) |
| 16 | 2, 15 | mpbid 232 |
. . 3
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝐴 ∈ NrmGrp) |
| 17 | 4 | sralmod 21194 |
. . . 4
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod) |
| 18 | 17 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝐴 ∈ LMod) |
| 19 | 5, 8 | srasca 21183 |
. . . 4
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |
| 20 | | eqid 2737 |
. . . . 5
⊢ (𝑊 ↾s 𝑆) = (𝑊 ↾s 𝑆) |
| 21 | 20 | subrgnrg 24694 |
. . . 4
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (𝑊 ↾s 𝑆) ∈ NrmRing) |
| 22 | 19, 21 | eqeltrrd 2842 |
. . 3
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (Scalar‘𝐴) ∈
NrmRing) |
| 23 | 16, 18, 22 | 3jca 1129 |
. 2
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (𝐴 ∈ NrmGrp ∧ 𝐴 ∈ LMod ∧ (Scalar‘𝐴) ∈
NrmRing)) |
| 24 | | eqid 2737 |
. . . . . . . 8
⊢
(norm‘𝑊) =
(norm‘𝑊) |
| 25 | | eqid 2737 |
. . . . . . . 8
⊢
(AbsVal‘𝑊) =
(AbsVal‘𝑊) |
| 26 | 24, 25 | nrgabv 24682 |
. . . . . . 7
⊢ (𝑊 ∈ NrmRing →
(norm‘𝑊) ∈
(AbsVal‘𝑊)) |
| 27 | 26 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (norm‘𝑊) ∈ (AbsVal‘𝑊)) |
| 28 | 8 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑆 ⊆ (Base‘𝑊)) |
| 29 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑥 ∈ (Base‘(Scalar‘𝐴))) |
| 30 | 20 | subrgbas 20581 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 = (Base‘(𝑊 ↾s 𝑆))) |
| 31 | 30 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝑆 = (Base‘(𝑊 ↾s 𝑆))) |
| 32 | 19 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (Base‘(𝑊 ↾s 𝑆)) =
(Base‘(Scalar‘𝐴))) |
| 33 | 31, 32 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝑆 = (Base‘(Scalar‘𝐴))) |
| 34 | 33 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑆 = (Base‘(Scalar‘𝐴))) |
| 35 | 29, 34 | eleqtrrd 2844 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑥 ∈ 𝑆) |
| 36 | 28, 35 | sseldd 3984 |
. . . . . 6
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑥 ∈ (Base‘𝑊)) |
| 37 | | simprr 773 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑦 ∈ (Base‘𝐴)) |
| 38 | 9 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (Base‘𝑊) = (Base‘𝐴)) |
| 39 | 37, 38 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑦 ∈ (Base‘𝑊)) |
| 40 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑊) = (.r‘𝑊) |
| 41 | 25, 6, 40 | abvmul 20822 |
. . . . . 6
⊢
(((norm‘𝑊)
∈ (AbsVal‘𝑊)
∧ 𝑥 ∈
(Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → ((norm‘𝑊)‘(𝑥(.r‘𝑊)𝑦)) = (((norm‘𝑊)‘𝑥) · ((norm‘𝑊)‘𝑦))) |
| 42 | 27, 36, 39, 41 | syl3anc 1373 |
. . . . 5
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → ((norm‘𝑊)‘(𝑥(.r‘𝑊)𝑦)) = (((norm‘𝑊)‘𝑥) · ((norm‘𝑊)‘𝑦))) |
| 43 | 9, 10, 12 | nmpropd 24607 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → (norm‘𝑊) = (norm‘𝐴)) |
| 44 | 43 | adantr 480 |
. . . . . 6
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (norm‘𝑊) = (norm‘𝐴)) |
| 45 | 5, 8 | sravsca 21185 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) →
(.r‘𝑊) = (
·𝑠 ‘𝐴)) |
| 46 | 45 | oveqdr 7459 |
. . . . . 6
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑥(.r‘𝑊)𝑦) = (𝑥( ·𝑠
‘𝐴)𝑦)) |
| 47 | 44, 46 | fveq12d 6913 |
. . . . 5
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → ((norm‘𝑊)‘(𝑥(.r‘𝑊)𝑦)) = ((norm‘𝐴)‘(𝑥( ·𝑠
‘𝐴)𝑦))) |
| 48 | 42, 47 | eqtr3d 2779 |
. . . 4
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (((norm‘𝑊)‘𝑥) · ((norm‘𝑊)‘𝑦)) = ((norm‘𝐴)‘(𝑥( ·𝑠
‘𝐴)𝑦))) |
| 49 | | subrgsubg 20577 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 ∈ (SubGrp‘𝑊)) |
| 50 | 49 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑆 ∈ (SubGrp‘𝑊)) |
| 51 | | eqid 2737 |
. . . . . . . 8
⊢
(norm‘(𝑊
↾s 𝑆)) =
(norm‘(𝑊
↾s 𝑆)) |
| 52 | 20, 24, 51 | subgnm2 24647 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubGrp‘𝑊) ∧ 𝑥 ∈ 𝑆) → ((norm‘(𝑊 ↾s 𝑆))‘𝑥) = ((norm‘𝑊)‘𝑥)) |
| 53 | 50, 35, 52 | syl2anc 584 |
. . . . . 6
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → ((norm‘(𝑊 ↾s 𝑆))‘𝑥) = ((norm‘𝑊)‘𝑥)) |
| 54 | 19 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |
| 55 | 54 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (norm‘(𝑊 ↾s 𝑆)) = (norm‘(Scalar‘𝐴))) |
| 56 | 55 | fveq1d 6908 |
. . . . . 6
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → ((norm‘(𝑊 ↾s 𝑆))‘𝑥) = ((norm‘(Scalar‘𝐴))‘𝑥)) |
| 57 | 53, 56 | eqtr3d 2779 |
. . . . 5
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → ((norm‘𝑊)‘𝑥) = ((norm‘(Scalar‘𝐴))‘𝑥)) |
| 58 | 44 | fveq1d 6908 |
. . . . 5
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → ((norm‘𝑊)‘𝑦) = ((norm‘𝐴)‘𝑦)) |
| 59 | 57, 58 | oveq12d 7449 |
. . . 4
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (((norm‘𝑊)‘𝑥) · ((norm‘𝑊)‘𝑦)) = (((norm‘(Scalar‘𝐴))‘𝑥) · ((norm‘𝐴)‘𝑦))) |
| 60 | 48, 59 | eqtr3d 2779 |
. . 3
⊢ (((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → ((norm‘𝐴)‘(𝑥( ·𝑠
‘𝐴)𝑦)) = (((norm‘(Scalar‘𝐴))‘𝑥) · ((norm‘𝐴)‘𝑦))) |
| 61 | 60 | ralrimivva 3202 |
. 2
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → ∀𝑥 ∈
(Base‘(Scalar‘𝐴))∀𝑦 ∈ (Base‘𝐴)((norm‘𝐴)‘(𝑥( ·𝑠
‘𝐴)𝑦)) = (((norm‘(Scalar‘𝐴))‘𝑥) · ((norm‘𝐴)‘𝑦))) |
| 62 | | eqid 2737 |
. . 3
⊢
(Base‘𝐴) =
(Base‘𝐴) |
| 63 | | eqid 2737 |
. . 3
⊢
(norm‘𝐴) =
(norm‘𝐴) |
| 64 | | eqid 2737 |
. . 3
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
| 65 | | eqid 2737 |
. . 3
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
| 66 | | eqid 2737 |
. . 3
⊢
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴)) |
| 67 | | eqid 2737 |
. . 3
⊢
(norm‘(Scalar‘𝐴)) = (norm‘(Scalar‘𝐴)) |
| 68 | 62, 63, 64, 65, 66, 67 | isnlm 24696 |
. 2
⊢ (𝐴 ∈ NrmMod ↔ ((𝐴 ∈ NrmGrp ∧ 𝐴 ∈ LMod ∧
(Scalar‘𝐴) ∈
NrmRing) ∧ ∀𝑥
∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ (Base‘𝐴)((norm‘𝐴)‘(𝑥( ·𝑠
‘𝐴)𝑦)) = (((norm‘(Scalar‘𝐴))‘𝑥) · ((norm‘𝐴)‘𝑦)))) |
| 69 | 23, 61, 68 | sylanbrc 583 |
1
⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝐴 ∈ NrmMod) |