Step | Hyp | Ref
| Expression |
1 | | simp2 1138 |
. . . 4
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β π β CMetSp) |
2 | | eqidd 2738 |
. . . . 5
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (Baseβπ) = (Baseβπ)) |
3 | | srabn.a |
. . . . . . 7
β’ π΄ = ((subringAlg βπ)βπ) |
4 | 3 | a1i 11 |
. . . . . 6
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β π΄ = ((subringAlg βπ)βπ)) |
5 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
6 | 5 | subrgss 20226 |
. . . . . . 7
β’ (π β (SubRingβπ) β π β (Baseβπ)) |
7 | 6 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β π β (Baseβπ)) |
8 | 4, 7 | srabase 20643 |
. . . . 5
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (Baseβπ) = (Baseβπ΄)) |
9 | 4, 7 | srads 20657 |
. . . . . 6
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (distβπ) = (distβπ΄)) |
10 | 9 | reseq1d 5937 |
. . . . 5
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))) = ((distβπ΄) βΎ ((Baseβπ) Γ (Baseβπ)))) |
11 | 4, 7 | sratopn 20656 |
. . . . 5
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (TopOpenβπ) = (TopOpenβπ΄)) |
12 | 2, 8, 10, 11 | cmspropd 24716 |
. . . 4
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (π β CMetSp β π΄ β CMetSp)) |
13 | 1, 12 | mpbid 231 |
. . 3
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β π΄ β CMetSp) |
14 | | eqid 2737 |
. . . . . 6
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
15 | 14 | isbn 24705 |
. . . . 5
β’ (π΄ β Ban β (π΄ β NrmVec β§ π΄ β CMetSp β§
(Scalarβπ΄) β
CMetSp)) |
16 | | 3anrot 1101 |
. . . . 5
β’ ((π΄ β NrmVec β§ π΄ β CMetSp β§
(Scalarβπ΄) β
CMetSp) β (π΄ β
CMetSp β§ (Scalarβπ΄) β CMetSp β§ π΄ β NrmVec)) |
17 | | 3anass 1096 |
. . . . 5
β’ ((π΄ β CMetSp β§
(Scalarβπ΄) β
CMetSp β§ π΄ β
NrmVec) β (π΄ β
CMetSp β§ ((Scalarβπ΄) β CMetSp β§ π΄ β NrmVec))) |
18 | 15, 16, 17 | 3bitri 297 |
. . . 4
β’ (π΄ β Ban β (π΄ β CMetSp β§
((Scalarβπ΄) β
CMetSp β§ π΄ β
NrmVec))) |
19 | 18 | baib 537 |
. . 3
β’ (π΄ β CMetSp β (π΄ β Ban β
((Scalarβπ΄) β
CMetSp β§ π΄ β
NrmVec))) |
20 | 13, 19 | syl 17 |
. 2
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (π΄ β Ban β ((Scalarβπ΄) β CMetSp β§ π΄ β
NrmVec))) |
21 | 4, 7 | srasca 20649 |
. . . . 5
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (π βΎs π) = (Scalarβπ΄)) |
22 | 21 | eleq1d 2823 |
. . . 4
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β ((π βΎs π) β CMetSp β (Scalarβπ΄) β
CMetSp)) |
23 | | eqid 2737 |
. . . . . 6
β’ (π βΎs π) = (π βΎs π) |
24 | | srabn.j |
. . . . . 6
β’ π½ = (TopOpenβπ) |
25 | 23, 5, 24 | cmsss 24718 |
. . . . 5
β’ ((π β CMetSp β§ π β (Baseβπ)) β ((π βΎs π) β CMetSp β π β (Clsdβπ½))) |
26 | 1, 7, 25 | syl2anc 585 |
. . . 4
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β ((π βΎs π) β CMetSp β π β (Clsdβπ½))) |
27 | 22, 26 | bitr3d 281 |
. . 3
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β ((Scalarβπ΄) β CMetSp β π β (Clsdβπ½))) |
28 | 3 | sranlm 24051 |
. . . . . 6
β’ ((π β NrmRing β§ π β (SubRingβπ)) β π΄ β NrmMod) |
29 | 28 | 3adant2 1132 |
. . . . 5
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β π΄ β NrmMod) |
30 | 14 | isnvc2 24066 |
. . . . . 6
β’ (π΄ β NrmVec β (π΄ β NrmMod β§
(Scalarβπ΄) β
DivRing)) |
31 | 30 | baib 537 |
. . . . 5
β’ (π΄ β NrmMod β (π΄ β NrmVec β
(Scalarβπ΄) β
DivRing)) |
32 | 29, 31 | syl 17 |
. . . 4
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (π΄ β NrmVec β (Scalarβπ΄) β
DivRing)) |
33 | 21 | eleq1d 2823 |
. . . 4
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β ((π βΎs π) β DivRing β (Scalarβπ΄) β
DivRing)) |
34 | 32, 33 | bitr4d 282 |
. . 3
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (π΄ β NrmVec β (π βΎs π) β DivRing)) |
35 | 27, 34 | anbi12d 632 |
. 2
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (((Scalarβπ΄) β CMetSp β§ π΄ β NrmVec) β (π β (Clsdβπ½) β§ (π βΎs π) β DivRing))) |
36 | 20, 35 | bitrd 279 |
1
β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (π΄ β Ban β (π β (Clsdβπ½) β§ (π βΎs π) β DivRing))) |