dvhelvbasei

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

	Ref	Expression
Hypotheses	dvhvbase.h	$⊢ H = LHyp (K)$
	dvhvbase.t	$⊢ T = LTrn (K) (W)$
	dvhvbase.e	$⊢ E = TEndo (K) (W)$
	dvhvbase.u	$⊢ U = DVecH (K) (W)$
	dvhvbase.v	$⊢ V = {Base}_{U}$
Assertion	dvhelvbasei	$⊢ ((K \in X \land W \in H) \land (F \in T \land S \in E)) \to ⟨F, S⟩ \in V$

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

Metamath Proof Explorer