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 · ˙ = D
ldualssvscl.s S = LSubSp D
ldualssvscl.w φ W LMod
ldualssvscl.u φ U S
ldualssvscl.x φ X K
ldualssvscl.y φ Y U
Assertion ldualssvscl φ X · ˙ Y 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 · ˙ = D
5 ldualssvscl.s S = LSubSp D
6 ldualssvscl.w φ W LMod
7 ldualssvscl.u φ U S
8 ldualssvscl.x φ X K
9 ldualssvscl.y φ Y U
10 3 6 lduallmod φ D LMod
11 eqid Scalar D = Scalar D
12 eqid Base Scalar D = Base Scalar D
13 1 2 3 11 12 6 ldualsbase φ Base Scalar D = K
14 8 13 eleqtrrd φ X Base Scalar D
15 11 4 12 5 lssvscl D LMod U S X Base Scalar D Y U X · ˙ Y U
16 10 7 14 9 15 syl22anc φ X · ˙ Y U