This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tcphcphlem3

Description: Lemma for tcphcph : real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015)

Ref Expression
Hypotheses tcphval.n 
|- G = ( toCPreHil ` W )
tcphcph.v 
|- V = ( Base ` W )
tcphcph.f 
|- F = ( Scalar ` W )
tcphcph.1 
|- ( ph -> W e. PreHil )
tcphcph.2 
|- ( ph -> F = ( CCfld |`s K ) )
tcphcph.h 
|- ., = ( .i ` W )
Assertion tcphcphlem3 
|- ( ( ph /\ X e. V ) -> ( X ., X ) e. RR )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 tcphcph.v 
 |-  V = ( Base ` W )
3 tcphcph.f 
 |-  F = ( Scalar ` W )
4 tcphcph.1 
 |-  ( ph -> W e. PreHil )
5 tcphcph.2 
 |-  ( ph -> F = ( CCfld |`s K ) )
6 tcphcph.h 
 |-  ., = ( .i ` W )
7 1 2 3 4 5 phclm 
 |-  ( ph -> W e. CMod )
8 7 adantr 
 |-  ( ( ph /\ X e. V ) -> W e. CMod )
9 eqid 
 |-  ( Base ` F ) = ( Base ` F )
10 3 9 clmsscn 
 |-  ( W e. CMod -> ( Base ` F ) C_ CC )
11 8 10 syl 
 |-  ( ( ph /\ X e. V ) -> ( Base ` F ) C_ CC )
12 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ X e. V /\ X e. V ) -> ( X ., X ) e. ( Base ` F ) )
13 12 3anidm23 
 |-  ( ( W e. PreHil /\ X e. V ) -> ( X ., X ) e. ( Base ` F ) )
14 4 13 sylan 
 |-  ( ( ph /\ X e. V ) -> ( X ., X ) e. ( Base ` F ) )
15 11 14 sseldd 
 |-  ( ( ph /\ X e. V ) -> ( X ., X ) e. CC )
16 3 clmcj 
 |-  ( W e. CMod -> * = ( *r ` F ) )
17 8 16 syl 
 |-  ( ( ph /\ X e. V ) -> * = ( *r ` F ) )
18 17 fveq1d 
 |-  ( ( ph /\ X e. V ) -> ( * ` ( X ., X ) ) = ( ( *r ` F ) ` ( X ., X ) ) )
19 4 adantr 
 |-  ( ( ph /\ X e. V ) -> W e. PreHil )
20 simpr 
 |-  ( ( ph /\ X e. V ) -> X e. V )
21 eqid 
 |-  ( *r ` F ) = ( *r ` F )
22 3 6 2 21 ipcj 
 |-  ( ( W e. PreHil /\ X e. V /\ X e. V ) -> ( ( *r ` F ) ` ( X ., X ) ) = ( X ., X ) )
23 19 20 20 22 syl3anc 
 |-  ( ( ph /\ X e. V ) -> ( ( *r ` F ) ` ( X ., X ) ) = ( X ., X ) )
24 18 23 eqtrd 
 |-  ( ( ph /\ X e. V ) -> ( * ` ( X ., X ) ) = ( X ., X ) )
25 15 24 cjrebd 
 |-  ( ( ph /\ X e. V ) -> ( X ., X ) e. RR )