Metamath Proof Explorer

Theorem hlhillvec

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

Ref Expression
Hypotheses hlhillvec.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hlhillvec.u ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
hlhillvec.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion hlhillvec ( 𝜑 → 𝑈 ∈ LVec )

Proof

Step Hyp Ref Expression
1 hlhillvec.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hlhillvec.u ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
3 hlhillvec.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
4 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 1 4 3 dvhlvec ⊢ ( 𝜑 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
6 eqidd ⊢ ( 𝜑 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
7 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
8 1 2 3 4 7 hlhilbase ⊢ ( 𝜑 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ 𝑈 ) )
9 eqid ⊢ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
10 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
11 eqidd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
12 eqid ⊢ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
13 1 4 9 2 10 3 12 hlhilsbase2 ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
14 eqid ⊢ ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
15 1 2 3 4 14 hlhilplus ⊢ ( 𝜑 → ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +g ‘ 𝑈 ) )
16 15 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( 𝑥 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) )
17 eqid ⊢ ( +g ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( +g ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
18 1 4 9 2 10 3 17 hlhilsplus2 ⊢ ( 𝜑 → ( +g ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( +g ‘ ( Scalar ‘ 𝑈 ) ) )
19 18 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) → ( 𝑥 ( +g ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑦 ) )
20 eqid ⊢ ( .r ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( .r ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
21 1 4 9 2 10 3 20 hlhilsmul2 ⊢ ( 𝜑 → ( .r ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( .r ‘ ( Scalar ‘ 𝑈 ) ) )
22 21 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) → ( 𝑥 ( .r ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( Scalar ‘ 𝑈 ) ) 𝑦 ) )
23 eqid ⊢ ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
24 1 4 23 2 3 hlhilvsca ⊢ ( 𝜑 → ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ 𝑈 ) )
25 24 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑦 ) )
26 6 8 9 10 11 13 16 19 22 25 lvecprop2d ⊢ ( 𝜑 → ( ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec ↔ 𝑈 ∈ LVec ) )
27 5 26 mpbid ⊢ ( 𝜑 → 𝑈 ∈ LVec )