dib1dim

Description: Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	dib1dim.b	$⊢ B = {Base}_{K}$
	dib1dim.h	$⊢ H = LHyp (K)$
	dib1dim.t	$⊢ T = LTrn (K) (W)$
	dib1dim.r	$⊢ R = trL (K) (W)$
	dib1dim.e	$⊢ E = TEndo (K) (W)$
	dib1dim.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dib1dim.i	$⊢ I = DIsoB (K) (W)$
Assertion	dib1dim	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{g \in (T \times E) \| \exists s \in E g = ⟨s (F), O⟩\}$

Proof

Step	Hyp	Ref	Expression
1		dib1dim.b	$⊢ B = {Base}_{K}$
2		dib1dim.h	$⊢ H = LHyp (K)$
3		dib1dim.t	$⊢ T = LTrn (K) (W)$
4		dib1dim.r	$⊢ R = trL (K) (W)$
5		dib1dim.e	$⊢ E = TEndo (K) (W)$
6		dib1dim.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
7		dib1dim.i	$⊢ I = DIsoB (K) (W)$
8		simpl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (K \in HL \land W \in H)$
9	1 2 3 4	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in B$
10		eqid	$⊢ \leq_{K} = \leq_{K}$
11	10 2 3 4	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \leq_{K} W$
12		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
13	1 10 2 3 6 12 7	dibval2	$⊢ ((K \in HL \land W \in H) \land (R (F) \in B \land R (F) \leq_{K} W)) \to I (R (F)) = DIsoA (K) (W) (R (F)) \times \{O\}$
14	8 9 11 13	syl12anc	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = DIsoA (K) (W) (R (F)) \times \{O\}$
15		relxp	$⊢ Rel (DIsoA (K) (W) (R (F)) \times \{O\})$
16		opelxp	$⊢ ⟨f, t⟩ \in (DIsoA (K) (W) (R (F)) \times \{O\}) \leftrightarrow (f \in DIsoA (K) (W) (R (F)) \land t \in \{O\})$
17	2 3 4 5 12	dia1dim	$⊢ ((K \in HL \land W \in H) \land F \in T) \to DIsoA (K) (W) (R (F)) = \{f \| \exists s \in E f = s (F)\}$
18	17	abeq2d	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (f \in DIsoA (K) (W) (R (F)) \leftrightarrow \exists s \in E f = s (F))$
19	18	anbi1d	$⊢ ((K \in HL \land W \in H) \land F \in T) \to ((f \in DIsoA (K) (W) (R (F)) \land t \in \{O\}) \leftrightarrow (\exists s \in E f = s (F) \land t \in \{O\}))$
20	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in E \land F \in T) \to s (F) \in T$
21	20	3expa	$⊢ (((K \in HL \land W \in H) \land s \in E) \land F \in T) \to s (F) \in T$
22	21	an32s	$⊢ (((K \in HL \land W \in H) \land F \in T) \land s \in E) \to s (F) \in T$
23	1 2 3 5 6	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
24	23	ad2antrr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land s \in E) \to O \in E$
25	22 24	jca	$⊢ (((K \in HL \land W \in H) \land F \in T) \land s \in E) \to (s (F) \in T \land O \in E)$
26		eleq1	$⊢ f = s (F) \to (f \in T \leftrightarrow s (F) \in T)$
27		eleq1	$⊢ t = O \to (t \in E \leftrightarrow O \in E)$
28	26 27	bi2anan9	$⊢ (f = s (F) \land t = O) \to ((f \in T \land t \in E) \leftrightarrow (s (F) \in T \land O \in E))$
29	25 28	syl5ibrcom	$⊢ (((K \in HL \land W \in H) \land F \in T) \land s \in E) \to ((f = s (F) \land t = O) \to (f \in T \land t \in E))$
30	29	rexlimdva	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists s \in E (f = s (F) \land t = O) \to (f \in T \land t \in E))$
31	30	pm4.71rd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists s \in E (f = s (F) \land t = O) \leftrightarrow ((f \in T \land t \in E) \land \exists s \in E (f = s (F) \land t = O)))$
32		velsn	$⊢ t \in \{O\} \leftrightarrow t = O$
33	32	anbi2i	$⊢ (\exists s \in E f = s (F) \land t \in \{O\}) \leftrightarrow (\exists s \in E f = s (F) \land t = O)$
34		r19.41v	$⊢ \exists s \in E (f = s (F) \land t = O) \leftrightarrow (\exists s \in E f = s (F) \land t = O)$
35	33 34	bitr4i	$⊢ (\exists s \in E f = s (F) \land t \in \{O\}) \leftrightarrow \exists s \in E (f = s (F) \land t = O)$
36		df-3an	$⊢ (f \in T \land t \in E \land \exists s \in E (f = s (F) \land t = O)) \leftrightarrow ((f \in T \land t \in E) \land \exists s \in E (f = s (F) \land t = O))$
37	31 35 36	3bitr4g	$⊢ ((K \in HL \land W \in H) \land F \in T) \to ((\exists s \in E f = s (F) \land t \in \{O\}) \leftrightarrow (f \in T \land t \in E \land \exists s \in E (f = s (F) \land t = O)))$
38	19 37	bitrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to ((f \in DIsoA (K) (W) (R (F)) \land t \in \{O\}) \leftrightarrow (f \in T \land t \in E \land \exists s \in E (f = s (F) \land t = O)))$
39	16 38	syl5bb	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (⟨f, t⟩ \in (DIsoA (K) (W) (R (F)) \times \{O\}) \leftrightarrow (f \in T \land t \in E \land \exists s \in E (f = s (F) \land t = O)))$
40	15 39	opabbi2dv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to DIsoA (K) (W) (R (F)) \times \{O\} = \{⟨f, t⟩ \| (f \in T \land t \in E \land \exists s \in E (f = s (F) \land t = O))\}$
41	14 40	eqtrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{⟨f, t⟩ \| (f \in T \land t \in E \land \exists s \in E (f = s (F) \land t = O))\}$
42		eqeq1	$⊢ g = ⟨f, t⟩ \to (g = ⟨s (F), O⟩ \leftrightarrow ⟨f, t⟩ = ⟨s (F), O⟩)$
43		vex	$⊢ f \in V$
44		vex	$⊢ t \in V$
45	43 44	opth	$⊢ ⟨f, t⟩ = ⟨s (F), O⟩ \leftrightarrow (f = s (F) \land t = O)$
46	42 45	syl6bb	$⊢ g = ⟨f, t⟩ \to (g = ⟨s (F), O⟩ \leftrightarrow (f = s (F) \land t = O))$
47	46	rexbidv	$⊢ g = ⟨f, t⟩ \to (\exists s \in E g = ⟨s (F), O⟩ \leftrightarrow \exists s \in E (f = s (F) \land t = O))$
48	47	rabxp	$⊢ \{g \in (T \times E) \| \exists s \in E g = ⟨s (F), O⟩\} = \{⟨f, t⟩ \| (f \in T \land t \in E \land \exists s \in E (f = s (F) \land t = O))\}$
49	41 48	eqtr4di	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{g \in (T \times E) \| \exists s \in E g = ⟨s (F), O⟩\}$

Metamath Proof Explorer

Theorem dib1dim

Proof