Metamath Proof Explorer

Theorem cphsscph

Description: A subspace of a subcomplex pre-Hilbert space is a subcomplex pre-Hilbert space. (Contributed by NM, 1-Feb-2008) (Revised by AV, 25-Sep-2022)

Ref Expression
Hypotheses cphsscph.x 
|- X = ( W |`s U )
cphsscph.s 
|- S = ( LSubSp ` W )
Assertion cphsscph 
|- ( ( W e. CPreHil /\ U e. S ) -> X e. CPreHil )

Proof

Step Hyp Ref Expression
1 cphsscph.x 
 |-  X = ( W |`s U )
2 cphsscph.s 
 |-  S = ( LSubSp ` W )
3 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
4 1 2 phlssphl 
 |-  ( ( W e. PreHil /\ U e. S ) -> X e. PreHil )
5 3 4 sylan 
 |-  ( ( W e. CPreHil /\ U e. S ) -> X e. PreHil )
6 cphnlm 
 |-  ( W e. CPreHil -> W e. NrmMod )
7 1 2 lssnlm 
 |-  ( ( W e. NrmMod /\ U e. S ) -> X e. NrmMod )
8 6 7 sylan 
 |-  ( ( W e. CPreHil /\ U e. S ) -> X e. NrmMod )
9 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
10 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
11 9 10 cphsca 
 |-  ( W e. CPreHil -> ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) )
12 11 adantr 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) )
13 1 9 resssca 
 |-  ( U e. S -> ( Scalar ` W ) = ( Scalar ` X ) )
14 13 fveq2d 
 |-  ( U e. S -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` X ) ) )
15 14 oveq2d 
 |-  ( U e. S -> ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) = ( CCfld |`s ( Base ` ( Scalar ` X ) ) ) )
16 13 15 eqeq12d 
 |-  ( U e. S -> ( ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) <-> ( Scalar ` X ) = ( CCfld |`s ( Base ` ( Scalar ` X ) ) ) ) )
17 16 adantl 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) <-> ( Scalar ` X ) = ( CCfld |`s ( Base ` ( Scalar ` X ) ) ) ) )
18 12 17 mpbid 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( Scalar ` X ) = ( CCfld |`s ( Base ` ( Scalar ` X ) ) ) )
19 5 8 18 3jca 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( X e. PreHil /\ X e. NrmMod /\ ( Scalar ` X ) = ( CCfld |`s ( Base ` ( Scalar ` X ) ) ) ) )
20 simpl 
 |-  ( ( W e. CPreHil /\ U e. S ) -> W e. CPreHil )
21 elinel1 
 |-  ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) -> q e. ( Base ` ( Scalar ` W ) ) )
22 21 adantr 
 |-  ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) -> q e. ( Base ` ( Scalar ` W ) ) )
23 elinel2 
 |-  ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) -> q e. ( 0 [,) +oo ) )
24 elrege0 
 |-  ( q e. ( 0 [,) +oo ) <-> ( q e. RR /\ 0 <_ q ) )
25 24 simplbi 
 |-  ( q e. ( 0 [,) +oo ) -> q e. RR )
26 23 25 syl 
 |-  ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) -> q e. RR )
27 26 adantr 
 |-  ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) -> q e. RR )
28 24 simprbi 
 |-  ( q e. ( 0 [,) +oo ) -> 0 <_ q )
29 23 28 syl 
 |-  ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) -> 0 <_ q )
30 29 adantr 
 |-  ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) -> 0 <_ q )
31 22 27 30 3jca 
 |-  ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) -> ( q e. ( Base ` ( Scalar ` W ) ) /\ q e. RR /\ 0 <_ q ) )
32 9 10 cphsqrtcl 
 |-  ( ( W e. CPreHil /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ q e. RR /\ 0 <_ q ) ) -> ( sqrt ` q ) e. ( Base ` ( Scalar ` W ) ) )
33 20 31 32 syl2anr 
 |-  ( ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) /\ ( W e. CPreHil /\ U e. S ) ) -> ( sqrt ` q ) e. ( Base ` ( Scalar ` W ) ) )
34 eleq1 
 |-  ( ( sqrt ` q ) = x -> ( ( sqrt ` q ) e. ( Base ` ( Scalar ` W ) ) <-> x e. ( Base ` ( Scalar ` W ) ) ) )
35 34 adantl 
 |-  ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) -> ( ( sqrt ` q ) e. ( Base ` ( Scalar ` W ) ) <-> x e. ( Base ` ( Scalar ` W ) ) ) )
36 35 adantr 
 |-  ( ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) /\ ( W e. CPreHil /\ U e. S ) ) -> ( ( sqrt ` q ) e. ( Base ` ( Scalar ` W ) ) <-> x e. ( Base ` ( Scalar ` W ) ) ) )
37 33 36 mpbid 
 |-  ( ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) /\ ( W e. CPreHil /\ U e. S ) ) -> x e. ( Base ` ( Scalar ` W ) ) )
38 37 ex 
 |-  ( ( q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) /\ ( sqrt ` q ) = x ) -> ( ( W e. CPreHil /\ U e. S ) -> x e. ( Base ` ( Scalar ` W ) ) ) )
39 38 rexlimiva 
 |-  ( E. q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ( sqrt ` q ) = x -> ( ( W e. CPreHil /\ U e. S ) -> x e. ( Base ` ( Scalar ` W ) ) ) )
40 df-sqrt 
 |-  sqrt = ( x e. CC |-> ( iota_ c e. CC ( ( c ^ 2 ) = x /\ 0 <_ ( Re ` c ) /\ ( _i x. c ) e/ RR+ ) ) )
41 40 funmpt2 
 |-  Fun sqrt
42 fvelima 
 |-  ( ( Fun sqrt /\ x e. ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) ) -> E. q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ( sqrt ` q ) = x )
43 41 42 mpan 
 |-  ( x e. ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) -> E. q e. ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ( sqrt ` q ) = x )
44 39 43 syl11 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( x e. ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) -> x e. ( Base ` ( Scalar ` W ) ) ) )
45 44 ssrdv 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` W ) ) )
46 14 ineq1d 
 |-  ( U e. S -> ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) = ( ( Base ` ( Scalar ` X ) ) i^i ( 0 [,) +oo ) ) )
47 46 imaeq2d 
 |-  ( U e. S -> ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) = ( sqrt " ( ( Base ` ( Scalar ` X ) ) i^i ( 0 [,) +oo ) ) ) )
48 47 14 sseq12d 
 |-  ( U e. S -> ( ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` W ) ) <-> ( sqrt " ( ( Base ` ( Scalar ` X ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` X ) ) ) )
49 48 adantl 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` W ) ) <-> ( sqrt " ( ( Base ` ( Scalar ` X ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` X ) ) ) )
50 45 49 mpbid 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( sqrt " ( ( Base ` ( Scalar ` X ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` X ) ) )
51 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
52 2 lsssubg 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
53 51 52 sylan 
 |-  ( ( W e. CPreHil /\ U e. S ) -> U e. ( SubGrp ` W ) )
54 eqid 
 |-  ( norm ` W ) = ( norm ` W )
55 eqid 
 |-  ( norm ` X ) = ( norm ` X )
56 1 54 55 subgnm 
 |-  ( U e. ( SubGrp ` W ) -> ( norm ` X ) = ( ( norm ` W ) |` U ) )
57 53 56 syl 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( norm ` X ) = ( ( norm ` W ) |` U ) )
58 eqid 
 |-  ( Base ` W ) = ( Base ` W )
59 eqid 
 |-  ( .i ` W ) = ( .i ` W )
60 58 59 54 cphnmfval 
 |-  ( W e. CPreHil -> ( norm ` W ) = ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` W ) b ) ) ) )
61 60 adantr 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( norm ` W ) = ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` W ) b ) ) ) )
62 1 59 ressip 
 |-  ( U e. S -> ( .i ` W ) = ( .i ` X ) )
63 62 adantl 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( .i ` W ) = ( .i ` X ) )
64 63 oveqd 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( b ( .i ` W ) b ) = ( b ( .i ` X ) b ) )
65 64 fveq2d 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( sqrt ` ( b ( .i ` W ) b ) ) = ( sqrt ` ( b ( .i ` X ) b ) ) )
66 65 mpteq2dv 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` W ) b ) ) ) = ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) )
67 61 66 eqtrd 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( norm ` W ) = ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) )
68 58 2 lssss 
 |-  ( U e. S -> U C_ ( Base ` W ) )
69 68 adantl 
 |-  ( ( W e. CPreHil /\ U e. S ) -> U C_ ( Base ` W ) )
70 dfss 
 |-  ( U C_ ( Base ` W ) <-> U = ( U i^i ( Base ` W ) ) )
71 69 70 sylib 
 |-  ( ( W e. CPreHil /\ U e. S ) -> U = ( U i^i ( Base ` W ) ) )
72 67 71 reseq12d 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( ( norm ` W ) |` U ) = ( ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) |` ( U i^i ( Base ` W ) ) ) )
73 1 58 ressbas 
 |-  ( U e. S -> ( U i^i ( Base ` W ) ) = ( Base ` X ) )
74 73 adantl 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( U i^i ( Base ` W ) ) = ( Base ` X ) )
75 74 reseq2d 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) |` ( U i^i ( Base ` W ) ) ) = ( ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) |` ( Base ` X ) ) )
76 72 75 eqtrd 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( ( norm ` W ) |` U ) = ( ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) |` ( Base ` X ) ) )
77 1 58 ressbasss 
 |-  ( Base ` X ) C_ ( Base ` W )
78 77 a1i 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( Base ` X ) C_ ( Base ` W ) )
79 78 resmptd 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( ( b e. ( Base ` W ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) |` ( Base ` X ) ) = ( b e. ( Base ` X ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) )
80 57 76 79 3eqtrd 
 |-  ( ( W e. CPreHil /\ U e. S ) -> ( norm ` X ) = ( b e. ( Base ` X ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) )
81 eqid 
 |-  ( Base ` X ) = ( Base ` X )
82 eqid 
 |-  ( .i ` X ) = ( .i ` X )
83 eqid 
 |-  ( Scalar ` X ) = ( Scalar ` X )
84 eqid 
 |-  ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` X ) )
85 81 82 55 83 84 iscph 
 |-  ( X e. CPreHil <-> ( ( X e. PreHil /\ X e. NrmMod /\ ( Scalar ` X ) = ( CCfld |`s ( Base ` ( Scalar ` X ) ) ) ) /\ ( sqrt " ( ( Base ` ( Scalar ` X ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` X ) ) /\ ( norm ` X ) = ( b e. ( Base ` X ) |-> ( sqrt ` ( b ( .i ` X ) b ) ) ) ) )
86 19 50 80 85 syl3anbrc 
 |-  ( ( W e. CPreHil /\ U e. S ) -> X e. CPreHil )