This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvhelvbasei

Description: Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014)

Ref Expression
Hypotheses dvhvbase.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvhvbase.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvhvbase.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dvhvbase.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvhvbase.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
Assertion dvhelvbasei ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) → ⟨ 𝐹 , 𝑆 ⟩ ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 dvhvbase.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvhvbase.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dvhvbase.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 dvhvbase.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dvhvbase.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 opelxpi ⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) → ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝑇 × 𝐸 ) )
7 6 adantl ⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) → ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝑇 × 𝐸 ) )
8 1 2 3 4 5 dvhvbase ⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝑉 = ( 𝑇 × 𝐸 ) )
9 8 adantr ⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) → 𝑉 = ( 𝑇 × 𝐸 ) )
10 7 9 eleqtrrd ⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) → ⟨ 𝐹 , 𝑆 ⟩ ∈ 𝑉 )