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 𝐻 = ( LHyp ‘ 𝐾 )
hlhil0.l 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hlhil0.u 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
hlhil0.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hlhil0.z 0 = ( 0g𝐿 )
Assertion hlhil0 ( 𝜑0 = ( 0g𝑈 ) )

Proof

Step Hyp Ref Expression
1 hlhil0.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hlhil0.l 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hlhil0.u 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
4 hlhil0.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
5 hlhil0.z 0 = ( 0g𝐿 )
6 eqidd ( 𝜑 → ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 ) )
7 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
8 1 3 4 2 7 hlhilbase ( 𝜑 → ( Base ‘ 𝐿 ) = ( Base ‘ 𝑈 ) )
9 eqid ( +g𝐿 ) = ( +g𝐿 )
10 1 3 4 2 9 hlhilplus ( 𝜑 → ( +g𝐿 ) = ( +g𝑈 ) )
11 10 oveqdr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐿 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) ) → ( 𝑥 ( +g𝐿 ) 𝑦 ) = ( 𝑥 ( +g𝑈 ) 𝑦 ) )
12 6 8 11 grpidpropd ( 𝜑 → ( 0g𝐿 ) = ( 0g𝑈 ) )
13 5 12 syl5eq ( 𝜑0 = ( 0g𝑈 ) )