# 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 ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dvhvbase.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dvhvbase.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dvhvbase.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvhvbase.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
Assertion dvhelvbasei ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {S}\in {E}\right)\right)\to ⟨{F},{S}⟩\in {V}$

### Proof

Step Hyp Ref Expression
1 dvhvbase.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dvhvbase.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
3 dvhvbase.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
4 dvhvbase.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dvhvbase.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
6 opelxpi ${⊢}\left({F}\in {T}\wedge {S}\in {E}\right)\to ⟨{F},{S}⟩\in \left({T}×{E}\right)$
7 6 adantl ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {S}\in {E}\right)\right)\to ⟨{F},{S}⟩\in \left({T}×{E}\right)$
8 1 2 3 4 5 dvhvbase ${⊢}\left({K}\in {X}\wedge {W}\in {H}\right)\to {V}={T}×{E}$
9 8 adantr ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {S}\in {E}\right)\right)\to {V}={T}×{E}$
10 7 9 eleqtrrd ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {S}\in {E}\right)\right)\to ⟨{F},{S}⟩\in {V}$