dia1dimid

Description: A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia1dimid.h	$⊢ H = LHyp (K)$
	dia1dimid.t	$⊢ T = LTrn (K) (W)$
	dia1dimid.r	$⊢ R = trL (K) (W)$
	dia1dimid.i	$⊢ I = DIsoA (K) (W)$
Assertion	dia1dimid	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in I (R (F))$

Step	Hyp	Ref	Expression
1		dia1dimid.h	$⊢ H = LHyp (K)$
2		dia1dimid.t	$⊢ T = LTrn (K) (W)$
3		dia1dimid.r	$⊢ R = trL (K) (W)$
4		dia1dimid.i	$⊢ I = DIsoA (K) (W)$
5		eqid	$⊢ DVecA (K) (W) = DVecA (K) (W)$
6	1 5	dvalvec	$⊢ (K \in HL \land W \in H) \to DVecA (K) (W) \in LVec$
7		lveclmod	$⊢ DVecA (K) (W) \in LVec \to DVecA (K) (W) \in LMod$
8	6 7	syl	$⊢ (K \in HL \land W \in H) \to DVecA (K) (W) \in LMod$
9	8	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to DVecA (K) (W) \in LMod$
10		eqid	$⊢ {Base}_{DVecA (K) (W)} = {Base}_{DVecA (K) (W)}$
11	1 2 5 10	dvavbase	$⊢ (K \in HL \land W \in H) \to {Base}_{DVecA (K) (W)} = T$
12	11	eleq2d	$⊢ (K \in HL \land W \in H) \to (F \in {Base}_{DVecA (K) (W)} \leftrightarrow F \in T)$
13	12	biimpar	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in {Base}_{DVecA (K) (W)}$
14		eqid	$⊢ LSpan (DVecA (K) (W)) = LSpan (DVecA (K) (W))$
15	10 14	lspsnid	$⊢ (DVecA (K) (W) \in LMod \land F \in {Base}_{DVecA (K) (W)}) \to F \in LSpan (DVecA (K) (W)) (\{F\})$
16	9 13 15	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in LSpan (DVecA (K) (W)) (\{F\})$
17	1 2 3 5 4 14	dia1dim2	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = LSpan (DVecA (K) (W)) (\{F\})$
18	16 17	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in I (R (F))$

Metamath Proof Explorer