dia1dim2

Description: Two expressions for a 1-dimensional subspace of partial vector space A (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 15-Jan-2014) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dia1dim2.h	$⊢ H = LHyp (K)$
	dia1dim2.t	$⊢ T = LTrn (K) (W)$
	dia1dim2.r	$⊢ R = trL (K) (W)$
	dva1dim2.u	$⊢ U = DVecA (K) (W)$
	dia1dim2.i	$⊢ I = DIsoA (K) (W)$
	dva1dim2.n	$⊢ N = LSpan (U)$
Assertion	dia1dim2	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = N (\{F\})$

Proof

Step	Hyp	Ref	Expression
1		dia1dim2.h	$⊢ H = LHyp (K)$
2		dia1dim2.t	$⊢ T = LTrn (K) (W)$
3		dia1dim2.r	$⊢ R = trL (K) (W)$
4		dva1dim2.u	$⊢ U = DVecA (K) (W)$
5		dia1dim2.i	$⊢ I = DIsoA (K) (W)$
6		dva1dim2.n	$⊢ N = LSpan (U)$
7		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
8		eqid	$⊢ Scalar (U) = Scalar (U)$
9		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
10	1 7 4 8 9	dvabase	$⊢ (K \in HL \land W \in H) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
11	10	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
12	11	rexeqdv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists s \in {Base}_{Scalar (U)} g = s \cdot_{U} F \leftrightarrow \exists s \in TEndo (K) (W) g = s \cdot_{U} F)$
13		eqid	$⊢ \cdot_{U} = \cdot_{U}$
14	1 2 7 4 13	dvavsca	$⊢ ((K \in HL \land W \in H) \land (s \in TEndo (K) (W) \land F \in T)) \to s \cdot_{U} F = s (F)$
15	14	anass1rs	$⊢ (((K \in HL \land W \in H) \land F \in T) \land s \in TEndo (K) (W)) \to s \cdot_{U} F = s (F)$
16	15	eqeq2d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land s \in TEndo (K) (W)) \to (g = s \cdot_{U} F \leftrightarrow g = s (F))$
17	16	rexbidva	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists s \in TEndo (K) (W) g = s \cdot_{U} F \leftrightarrow \exists s \in TEndo (K) (W) g = s (F))$
18	12 17	bitrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists s \in {Base}_{Scalar (U)} g = s \cdot_{U} F \leftrightarrow \exists s \in TEndo (K) (W) g = s (F))$
19	18	abbidv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \{g \| \exists s \in {Base}_{Scalar (U)} g = s \cdot_{U} F\} = \{g \| \exists s \in TEndo (K) (W) g = s (F)\}$
20	1 4	dvalvec	$⊢ (K \in HL \land W \in H) \to U \in LVec$
21	20	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to U \in LVec$
22		lveclmod	$⊢ U \in LVec \to U \in LMod$
23	21 22	syl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to U \in LMod$
24		simpr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in T$
25		eqid	$⊢ {Base}_{U} = {Base}_{U}$
26	1 2 4 25	dvavbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = T$
27	26	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to {Base}_{U} = T$
28	24 27	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in {Base}_{U}$
29	8 9 25 13 6	lspsn	$⊢ (U \in LMod \land F \in {Base}_{U}) \to N (\{F\}) = \{g \| \exists s \in {Base}_{Scalar (U)} g = s \cdot_{U} F\}$
30	23 28 29	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T) \to N (\{F\}) = \{g \| \exists s \in {Base}_{Scalar (U)} g = s \cdot_{U} F\}$
31	1 2 3 7 5	dia1dim	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{g \| \exists s \in TEndo (K) (W) g = s (F)\}$
32	19 30 31	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = N (\{F\})$

Metamath Proof Explorer

Theorem dia1dim2

Proof