| 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 ) ) ) ) |