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

Metamath Proof Explorer

Theorem ldualssvscl

Description: Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015)

Ref Expression
Hypotheses ldualssvscl.r 
|- R = ( Scalar ` W )
ldualssvscl.k 
|- K = ( Base ` R )
ldualssvscl.d 
|- D = ( LDual ` W )
ldualssvscl.t 
|- .x. = ( .s ` D )
ldualssvscl.s 
|- S = ( LSubSp ` D )
ldualssvscl.w 
|- ( ph -> W e. LMod )
ldualssvscl.u 
|- ( ph -> U e. S )
ldualssvscl.x 
|- ( ph -> X e. K )
ldualssvscl.y 
|- ( ph -> Y e. U )
Assertion ldualssvscl 
|- ( ph -> ( X .x. Y ) e. U )

Proof

Step Hyp Ref Expression
1 ldualssvscl.r 
 |-  R = ( Scalar ` W )
2 ldualssvscl.k 
 |-  K = ( Base ` R )
3 ldualssvscl.d 
 |-  D = ( LDual ` W )
4 ldualssvscl.t 
 |-  .x. = ( .s ` D )
5 ldualssvscl.s 
 |-  S = ( LSubSp ` D )
6 ldualssvscl.w 
 |-  ( ph -> W e. LMod )
7 ldualssvscl.u 
 |-  ( ph -> U e. S )
8 ldualssvscl.x 
 |-  ( ph -> X e. K )
9 ldualssvscl.y 
 |-  ( ph -> Y e. U )
10 3 6 lduallmod 
 |-  ( ph -> D e. LMod )
11 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
12 eqid 
 |-  ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
13 1 2 3 11 12 6 ldualsbase 
 |-  ( ph -> ( Base ` ( Scalar ` D ) ) = K )
14 8 13 eleqtrrd 
 |-  ( ph -> X e. ( Base ` ( Scalar ` D ) ) )
15 11 4 12 5 lssvscl 
 |-  ( ( ( D e. LMod /\ U e. S ) /\ ( X e. ( Base ` ( Scalar ` D ) ) /\ Y e. U ) ) -> ( X .x. Y ) e. U )
16 10 7 14 9 15 syl22anc 
 |-  ( ph -> ( X .x. Y ) e. U )