Metamath Proof Explorer

Theorem tcphcphlem2

Description: Lemma for tcphcph : homogeneity. (Contributed by Mario Carneiro, 8-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 )
tcphcph.3 
|- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
tcphcph.4 
|- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
tcphcph.k 
|- K = ( Base ` F )
tcphcph.s 
|- .x. = ( .s ` W )
tcphcphlem2.3 
|- ( ph -> X e. K )
tcphcphlem2.4 
|- ( ph -> Y e. V )
Assertion tcphcphlem2 
|- ( ph -> ( sqrt ` ( ( X .x. Y ) ., ( X .x. Y ) ) ) = ( ( abs ` X ) x. ( sqrt ` ( Y ., Y ) ) ) )

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 tcphcph.3 
 |-  ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
8 tcphcph.4 
 |-  ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
9 tcphcph.k 
 |-  K = ( Base ` F )
10 tcphcph.s 
 |-  .x. = ( .s ` W )
11 tcphcphlem2.3 
 |-  ( ph -> X e. K )
12 tcphcphlem2.4 
 |-  ( ph -> Y e. V )
13 1 2 3 4 5 phclm 
 |-  ( ph -> W e. CMod )
14 3 9 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
15 13 14 syl 
 |-  ( ph -> K C_ CC )
16 15 11 sseldd 
 |-  ( ph -> X e. CC )
17 16 cjmulrcld 
 |-  ( ph -> ( X x. ( * ` X ) ) e. RR )
18 16 cjmulge0d 
 |-  ( ph -> 0 <_ ( X x. ( * ` X ) ) )
19 1 2 3 4 5 6 tcphcphlem3 
 |-  ( ( ph /\ Y e. V ) -> ( Y ., Y ) e. RR )
20 12 19 mpdan 
 |-  ( ph -> ( Y ., Y ) e. RR )
21 oveq12 
 |-  ( ( x = Y /\ x = Y ) -> ( x ., x ) = ( Y ., Y ) )
22 21 anidms 
 |-  ( x = Y -> ( x ., x ) = ( Y ., Y ) )
23 22 breq2d 
 |-  ( x = Y -> ( 0 <_ ( x ., x ) <-> 0 <_ ( Y ., Y ) ) )
24 8 ralrimiva 
 |-  ( ph -> A. x e. V 0 <_ ( x ., x ) )
25 23 24 12 rspcdva 
 |-  ( ph -> 0 <_ ( Y ., Y ) )
26 17 18 20 25 sqrtmuld 
 |-  ( ph -> ( sqrt ` ( ( X x. ( * ` X ) ) x. ( Y ., Y ) ) ) = ( ( sqrt ` ( X x. ( * ` X ) ) ) x. ( sqrt ` ( Y ., Y ) ) ) )
27 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
28 4 27 syl 
 |-  ( ph -> W e. LMod )
29 2 3 10 9 lmodvscl 
 |-  ( ( W e. LMod /\ X e. K /\ Y e. V ) -> ( X .x. Y ) e. V )
30 28 11 12 29 syl3anc 
 |-  ( ph -> ( X .x. Y ) e. V )
31 eqid 
 |-  ( .r ` F ) = ( .r ` F )
32 eqid 
 |-  ( *r ` F ) = ( *r ` F )
33 3 6 2 9 10 31 32 ipassr 
 |-  ( ( W e. PreHil /\ ( ( X .x. Y ) e. V /\ Y e. V /\ X e. K ) ) -> ( ( X .x. Y ) ., ( X .x. Y ) ) = ( ( ( X .x. Y ) ., Y ) ( .r ` F ) ( ( *r ` F ) ` X ) ) )
34 4 30 12 11 33 syl13anc 
 |-  ( ph -> ( ( X .x. Y ) ., ( X .x. Y ) ) = ( ( ( X .x. Y ) ., Y ) ( .r ` F ) ( ( *r ` F ) ` X ) ) )
35 3 clmmul 
 |-  ( W e. CMod -> x. = ( .r ` F ) )
36 13 35 syl 
 |-  ( ph -> x. = ( .r ` F ) )
37 36 oveqd 
 |-  ( ph -> ( X x. ( Y ., Y ) ) = ( X ( .r ` F ) ( Y ., Y ) ) )
38 3 6 2 9 10 31 ipass 
 |-  ( ( W e. PreHil /\ ( X e. K /\ Y e. V /\ Y e. V ) ) -> ( ( X .x. Y ) ., Y ) = ( X ( .r ` F ) ( Y ., Y ) ) )
39 4 11 12 12 38 syl13anc 
 |-  ( ph -> ( ( X .x. Y ) ., Y ) = ( X ( .r ` F ) ( Y ., Y ) ) )
40 37 39 eqtr4d 
 |-  ( ph -> ( X x. ( Y ., Y ) ) = ( ( X .x. Y ) ., Y ) )
41 3 clmcj 
 |-  ( W e. CMod -> * = ( *r ` F ) )
42 13 41 syl 
 |-  ( ph -> * = ( *r ` F ) )
43 42 fveq1d 
 |-  ( ph -> ( * ` X ) = ( ( *r ` F ) ` X ) )
44 36 40 43 oveq123d 
 |-  ( ph -> ( ( X x. ( Y ., Y ) ) x. ( * ` X ) ) = ( ( ( X .x. Y ) ., Y ) ( .r ` F ) ( ( *r ` F ) ` X ) ) )
45 20 recnd 
 |-  ( ph -> ( Y ., Y ) e. CC )
46 16 cjcld 
 |-  ( ph -> ( * ` X ) e. CC )
47 16 45 46 mul32d 
 |-  ( ph -> ( ( X x. ( Y ., Y ) ) x. ( * ` X ) ) = ( ( X x. ( * ` X ) ) x. ( Y ., Y ) ) )
48 34 44 47 3eqtr2d 
 |-  ( ph -> ( ( X .x. Y ) ., ( X .x. Y ) ) = ( ( X x. ( * ` X ) ) x. ( Y ., Y ) ) )
49 48 fveq2d 
 |-  ( ph -> ( sqrt ` ( ( X .x. Y ) ., ( X .x. Y ) ) ) = ( sqrt ` ( ( X x. ( * ` X ) ) x. ( Y ., Y ) ) ) )
50 absval 
 |-  ( X e. CC -> ( abs ` X ) = ( sqrt ` ( X x. ( * ` X ) ) ) )
51 16 50 syl 
 |-  ( ph -> ( abs ` X ) = ( sqrt ` ( X x. ( * ` X ) ) ) )
52 51 oveq1d 
 |-  ( ph -> ( ( abs ` X ) x. ( sqrt ` ( Y ., Y ) ) ) = ( ( sqrt ` ( X x. ( * ` X ) ) ) x. ( sqrt ` ( Y ., Y ) ) ) )
53 26 49 52 3eqtr4d 
 |-  ( ph -> ( sqrt ` ( ( X .x. Y ) ., ( X .x. Y ) ) ) = ( ( abs ` X ) x. ( sqrt ` ( Y ., Y ) ) ) )