dib1dim2

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, 24-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dib1dim2.b	$⊢ B = {Base}_{K}$
2		dib1dim2.h	$⊢ H = LHyp (K)$
3		dib1dim2.t	$⊢ T = LTrn (K) (W)$
4		dib1dim2.r	$⊢ R = trL (K) (W)$
5		dib1dim2.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
6		dib1dim2.u	$⊢ U = DVecH (K) (W)$
7		dib1dim2.i	$⊢ I = DIsoB (K) (W)$
8		dib1dim2.n	$⊢ N = LSpan (U)$
9		df-rab	$⊢ \{u \in (T \times TEndo (K) (W)) \| \exists v \in TEndo (K) (W) u = ⟨v (F), O⟩\} = \{u \| (u \in (T \times TEndo (K) (W)) \land \exists v \in TEndo (K) (W) u = ⟨v (F), O⟩)\}$
10		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
11	1 2 3 4 10 5 7	dib1dim	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{u \in (T \times TEndo (K) (W)) \| \exists v \in TEndo (K) (W) u = ⟨v (F), O⟩\}$
12		eqid	$⊢ Scalar (U) = Scalar (U)$
13		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
14	2 10 6 12 13	dvhbase	$⊢ (K \in HL \land W \in H) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
15	14	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
16	15	rexeqdv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists v \in {Base}_{Scalar (U)} u = v \cdot_{U} ⟨F, O⟩ \leftrightarrow \exists v \in TEndo (K) (W) u = v \cdot_{U} ⟨F, O⟩)$
17		simpll	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to (K \in HL \land W \in H)$
18		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to v \in TEndo (K) (W)$
19		simplr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to F \in T$
20	1 2 3 10 5	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in TEndo (K) (W)$
21	20	ad2antrr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to O \in TEndo (K) (W)$
22		eqid	$⊢ \cdot_{U} = \cdot_{U}$
23	2 3 10 6 22	dvhopvsca	$⊢ ((K \in HL \land W \in H) \land (v \in TEndo (K) (W) \land F \in T \land O \in TEndo (K) (W))) \to v \cdot_{U} ⟨F, O⟩ = ⟨v (F), v \circ O⟩$
24	17 18 19 21 23	syl13anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to v \cdot_{U} ⟨F, O⟩ = ⟨v (F), v \circ O⟩$
25	1 2 3 10 5	tendo0mulr	$⊢ ((K \in HL \land W \in H) \land v \in TEndo (K) (W)) \to v \circ O = O$
26	25	adantlr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to v \circ O = O$
27	26	opeq2d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to ⟨v (F), v \circ O⟩ = ⟨v (F), O⟩$
28	24 27	eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to v \cdot_{U} ⟨F, O⟩ = ⟨v (F), O⟩$
29	28	eqeq2d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to (u = v \cdot_{U} ⟨F, O⟩ \leftrightarrow u = ⟨v (F), O⟩)$
30	29	rexbidva	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists v \in TEndo (K) (W) u = v \cdot_{U} ⟨F, O⟩ \leftrightarrow \exists v \in TEndo (K) (W) u = ⟨v (F), O⟩)$
31	2 3 10	tendocl	$⊢ ((K \in HL \land W \in H) \land v \in TEndo (K) (W) \land F \in T) \to v (F) \in T$
32	31	3expa	$⊢ (((K \in HL \land W \in H) \land v \in TEndo (K) (W)) \land F \in T) \to v (F) \in T$
33	32	an32s	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to v (F) \in T$
34		opelxpi	$⊢ (v (F) \in T \land O \in TEndo (K) (W)) \to ⟨v (F), O⟩ \in (T \times TEndo (K) (W))$
35	33 21 34	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to ⟨v (F), O⟩ \in (T \times TEndo (K) (W))$
36		eleq1a	$⊢ ⟨v (F), O⟩ \in (T \times TEndo (K) (W)) \to (u = ⟨v (F), O⟩ \to u \in (T \times TEndo (K) (W)))$
37	35 36	syl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land v \in TEndo (K) (W)) \to (u = ⟨v (F), O⟩ \to u \in (T \times TEndo (K) (W)))$
38	37	rexlimdva	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists v \in TEndo (K) (W) u = ⟨v (F), O⟩ \to u \in (T \times TEndo (K) (W)))$
39	38	pm4.71rd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists v \in TEndo (K) (W) u = ⟨v (F), O⟩ \leftrightarrow (u \in (T \times TEndo (K) (W)) \land \exists v \in TEndo (K) (W) u = ⟨v (F), O⟩))$
40	16 30 39	3bitrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists v \in {Base}_{Scalar (U)} u = v \cdot_{U} ⟨F, O⟩ \leftrightarrow (u \in (T \times TEndo (K) (W)) \land \exists v \in TEndo (K) (W) u = ⟨v (F), O⟩))$
41	40	abbidv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \{u \| \exists v \in {Base}_{Scalar (U)} u = v \cdot_{U} ⟨F, O⟩\} = \{u \| (u \in (T \times TEndo (K) (W)) \land \exists v \in TEndo (K) (W) u = ⟨v (F), O⟩)\}$
42	9 11 41	3eqtr4a	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{u \| \exists v \in {Base}_{Scalar (U)} u = v \cdot_{U} ⟨F, O⟩\}$
43		simpl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (K \in HL \land W \in H)$
44	2 6 43	dvhlmod	$⊢ ((K \in HL \land W \in H) \land F \in T) \to U \in LMod$
45		simpr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in T$
46	20	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to O \in TEndo (K) (W)$
47		eqid	$⊢ {Base}_{U} = {Base}_{U}$
48	2 3 10 6 47	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land (F \in T \land O \in TEndo (K) (W))) \to ⟨F, O⟩ \in {Base}_{U}$
49	43 45 46 48	syl12anc	$⊢ ((K \in HL \land W \in H) \land F \in T) \to ⟨F, O⟩ \in {Base}_{U}$
50	12 13 47 22 8	lspsn	$⊢ (U \in LMod \land ⟨F, O⟩ \in {Base}_{U}) \to N (\{⟨F, O⟩\}) = \{u \| \exists v \in {Base}_{Scalar (U)} u = v \cdot_{U} ⟨F, O⟩\}$
51	44 49 50	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T) \to N (\{⟨F, O⟩\}) = \{u \| \exists v \in {Base}_{Scalar (U)} u = v \cdot_{U} ⟨F, O⟩\}$
52	42 51	eqtr4d	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = N (\{⟨F, O⟩\})$

Metamath Proof Explorer

Theorem dib1dim2

Proof