Metamath Proof Explorer

Theorem dih1dimb

Description: Two expressions for a 1-dimensional subspace of vector space H (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 27-Apr-2014)

		Ref	Expression
	Hypotheses	dih1dimb.b	$⊢ B = {Base}_{K}$
		dih1dimb.h	$⊢ H = LHyp (K)$
		dih1dimb.t	$⊢ T = LTrn (K) (W)$
		dih1dimb.r	$⊢ R = trL (K) (W)$
		dih1dimb.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
		dih1dimb.u	$⊢ U = DVecH (K) (W)$
		dih1dimb.i	$⊢ I = DIsoH (K) (W)$
		dih1dimb.n	$⊢ N = LSpan (U)$
	Assertion	dih1dimb	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = N (\{⟨F, O⟩\})$

Proof

Step	Hyp	Ref	Expression
1		dih1dimb.b	$⊢ B = {Base}_{K}$
2		dih1dimb.h	$⊢ H = LHyp (K)$
3		dih1dimb.t	$⊢ T = LTrn (K) (W)$
4		dih1dimb.r	$⊢ R = trL (K) (W)$
5		dih1dimb.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
6		dih1dimb.u	$⊢ U = DVecH (K) (W)$
7		dih1dimb.i	$⊢ I = DIsoH (K) (W)$
8		dih1dimb.n	$⊢ N = LSpan (U)$
9		simpl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (K \in HL \land W \in H)$
10	1 2 3 4	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in B$
11		eqid	$⊢ \leq_{K} = \leq_{K}$
12	11 2 3 4	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \leq_{K} W$
13		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
14	1 11 2 7 13	dihvalb	$⊢ ((K \in HL \land W \in H) \land (R (F) \in B \land R (F) \leq_{K} W)) \to I (R (F)) = DIsoB (K) (W) (R (F))$
15	9 10 12 14	syl12anc	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = DIsoB (K) (W) (R (F))$
16	1 2 3 4 5 6 13 8	dib1dim2	$⊢ ((K \in HL \land W \in H) \land F \in T) \to DIsoB (K) (W) (R (F)) = N (\{⟨F, O⟩\})$
17	15 16	eqtrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = N (\{⟨F, O⟩\})$