Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. 2
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β π β NrmVec) |
2 | | simpl2 1193 |
. 2
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β (Scalarβπ) β CMetSp) |
3 | | nvcnlm 24063 |
. . . . . . . 8
β’ (π β NrmVec β π β NrmMod) |
4 | | nlmngp 24044 |
. . . . . . . 8
β’ (π β NrmMod β π β NrmGrp) |
5 | 3, 4 | syl 17 |
. . . . . . 7
β’ (π β NrmVec β π β NrmGrp) |
6 | | nvclmod 24065 |
. . . . . . . 8
β’ (π β NrmVec β π β LMod) |
7 | | cssbn.s |
. . . . . . . . 9
β’ π = (LSubSpβπ) |
8 | 7 | lsssubg 20421 |
. . . . . . . 8
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
9 | 6, 8 | sylan 581 |
. . . . . . 7
β’ ((π β NrmVec β§ π β π) β π β (SubGrpβπ)) |
10 | | cssbn.x |
. . . . . . . 8
β’ π = (π βΎs π) |
11 | 10 | subgngp 23994 |
. . . . . . 7
β’ ((π β NrmGrp β§ π β (SubGrpβπ)) β π β NrmGrp) |
12 | 5, 9, 11 | syl2an2r 684 |
. . . . . 6
β’ ((π β NrmVec β§ π β π) β π β NrmGrp) |
13 | 12 | 3adant2 1132 |
. . . . 5
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β π β NrmGrp) |
14 | 13 | adantr 482 |
. . . 4
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β π β NrmGrp) |
15 | | ngpms 23959 |
. . . 4
β’ (π β NrmGrp β π β MetSp) |
16 | 14, 15 | syl 17 |
. . 3
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β π β MetSp) |
17 | | cssbn.d |
. . . . . . 7
β’ π· = ((distβπ) βΎ (π Γ π)) |
18 | | eqid 2737 |
. . . . . . . . . 10
β’
(distβπ) =
(distβπ) |
19 | 10, 18 | ressds 17292 |
. . . . . . . . 9
β’ (π β π β (distβπ) = (distβπ)) |
20 | 19 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β (distβπ) = (distβπ)) |
21 | 9 | 3adant2 1132 |
. . . . . . . . . 10
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β π β (SubGrpβπ)) |
22 | 10 | subgbas 18933 |
. . . . . . . . . 10
β’ (π β (SubGrpβπ) β π = (Baseβπ)) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β π = (Baseβπ)) |
24 | 23 | sqxpeqd 5666 |
. . . . . . . 8
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β (π Γ π) = ((Baseβπ) Γ (Baseβπ))) |
25 | 20, 24 | reseq12d 5939 |
. . . . . . 7
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β ((distβπ) βΎ (π Γ π)) = ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) |
26 | 17, 25 | eqtrid 2789 |
. . . . . 6
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β π· = ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) |
27 | 26 | eqcomd 2743 |
. . . . 5
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))) = π·) |
28 | 27 | adantr 482 |
. . . 4
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))) = π·) |
29 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
30 | | eqid 2737 |
. . . . . . . . 9
β’
((distβπ)
βΎ ((Baseβπ)
Γ (Baseβπ))) =
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) |
31 | 29, 30 | ngpmet 23962 |
. . . . . . . 8
β’ (π β NrmGrp β
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) β
(Metβ(Baseβπ))) |
32 | 13, 31 | syl 17 |
. . . . . . 7
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))) β
(Metβ(Baseβπ))) |
33 | 26, 32 | eqeltrd 2838 |
. . . . . 6
β’ ((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β π· β (Metβ(Baseβπ))) |
34 | 33 | adantr 482 |
. . . . 5
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β π· β (Metβ(Baseβπ))) |
35 | | simpr 486 |
. . . . 5
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) |
36 | | eqid 2737 |
. . . . . 6
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
37 | 36 | iscmet2 24661 |
. . . . 5
β’ (π· β
(CMetβ(Baseβπ))
β (π· β
(Metβ(Baseβπ))
β§ (Cauβπ·) β
dom (βπ‘β(MetOpenβπ·)))) |
38 | 34, 35, 37 | sylanbrc 584 |
. . . 4
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β π· β (CMetβ(Baseβπ))) |
39 | 28, 38 | eqeltrd 2838 |
. . 3
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))) β (CMetβ(Baseβπ))) |
40 | 29, 30 | iscms 24712 |
. . 3
β’ (π β CMetSp β (π β MetSp β§
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) β
(CMetβ(Baseβπ)))) |
41 | 16, 39, 40 | sylanbrc 584 |
. 2
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β π β CMetSp) |
42 | | simpl3 1194 |
. 2
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β π β π) |
43 | 10, 7 | cmslssbn 24739 |
. 2
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp) β§ (π β
CMetSp β§ π β π)) β π β Ban) |
44 | 1, 2, 41, 42, 43 | syl22anc 838 |
1
β’ (((π β NrmVec β§
(Scalarβπ) β
CMetSp β§ π β π) β§ (Cauβπ·) β dom
(βπ‘β(MetOpenβπ·))) β π β Ban) |