Metamath Proof Explorer


Theorem lcd0v2

Description: The zero functional in the set of functionals with closed kernels. (Contributed by NM, 27-Mar-2015)

Ref Expression
Hypotheses lcd0v2.h
|- H = ( LHyp ` K )
lcd0v2.u
|- U = ( ( DVecH ` K ) ` W )
lcd0v2.d
|- D = ( LDual ` U )
lcd0v2.z
|- .0. = ( 0g ` D )
lcd0v2.c
|- C = ( ( LCDual ` K ) ` W )
lcd0v2.o
|- O = ( 0g ` C )
lcd0v2.k
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion lcd0v2
|- ( ph -> O = .0. )

Proof

Step Hyp Ref Expression
1 lcd0v2.h
 |-  H = ( LHyp ` K )
2 lcd0v2.u
 |-  U = ( ( DVecH ` K ) ` W )
3 lcd0v2.d
 |-  D = ( LDual ` U )
4 lcd0v2.z
 |-  .0. = ( 0g ` D )
5 lcd0v2.c
 |-  C = ( ( LCDual ` K ) ` W )
6 lcd0v2.o
 |-  O = ( 0g ` C )
7 lcd0v2.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 eqid
 |-  ( Base ` U ) = ( Base ` U )
9 eqid
 |-  ( Scalar ` U ) = ( Scalar ` U )
10 eqid
 |-  ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
11 1 2 8 9 10 5 6 7 lcd0v
 |-  ( ph -> O = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) )
12 1 2 7 dvhlmod
 |-  ( ph -> U e. LMod )
13 8 9 10 3 4 12 ldual0v
 |-  ( ph -> .0. = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) )
14 11 13 eqtr4d
 |-  ( ph -> O = .0. )