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	⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) → ⟨ 𝐹 , 𝑆 ⟩ ∈ 𝑉 )