Metamath Proof Explorer


Theorem hlhil0

Description: The zero vector for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015)

Ref Expression
Hypotheses hlhil0.h
|- H = ( LHyp ` K )
hlhil0.l
|- L = ( ( DVecH ` K ) ` W )
hlhil0.u
|- U = ( ( HLHil ` K ) ` W )
hlhil0.k
|- ( ph -> ( K e. HL /\ W e. H ) )
hlhil0.z
|- .0. = ( 0g ` L )
Assertion hlhil0
|- ( ph -> .0. = ( 0g ` U ) )

Proof

Step Hyp Ref Expression
1 hlhil0.h
 |-  H = ( LHyp ` K )
2 hlhil0.l
 |-  L = ( ( DVecH ` K ) ` W )
3 hlhil0.u
 |-  U = ( ( HLHil ` K ) ` W )
4 hlhil0.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
5 hlhil0.z
 |-  .0. = ( 0g ` L )
6 eqidd
 |-  ( ph -> ( Base ` L ) = ( Base ` L ) )
7 eqid
 |-  ( Base ` L ) = ( Base ` L )
8 1 3 4 2 7 hlhilbase
 |-  ( ph -> ( Base ` L ) = ( Base ` U ) )
9 eqid
 |-  ( +g ` L ) = ( +g ` L )
10 1 3 4 2 9 hlhilplus
 |-  ( ph -> ( +g ` L ) = ( +g ` U ) )
11 10 oveqdr
 |-  ( ( ph /\ ( x e. ( Base ` L ) /\ y e. ( Base ` L ) ) ) -> ( x ( +g ` L ) y ) = ( x ( +g ` U ) y ) )
12 6 8 11 grpidpropd
 |-  ( ph -> ( 0g ` L ) = ( 0g ` U ) )
13 5 12 syl5eq
 |-  ( ph -> .0. = ( 0g ` U ) )