dvhb1dimN

Description: Two expressions for the 1-dimensional subspaces of vector space H, in the isomorphism B case where the 2nd vector component is zero. (Contributed by NM, 23-Feb-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvhb1dim.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dvhb1dim.h	$⊢ H = LHyp (K)$
	dvhb1dim.t	$⊢ T = LTrn (K) (W)$
	dvhb1dim.r	$⊢ R = trL (K) (W)$
	dvhb1dim.e	$⊢ E = TEndo (K) (W)$
	dvhb1dim.o	$⊢ \underset{˙}{0} = (h \in T ⟼ {I ↾}_{B})$
Assertion	dvhb1dimN	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \{g \in (T \times E) \| \exists s \in E g = ⟨s (F), \underset{˙}{0}⟩\} = \{g \in (T \times E) \| (R (1^{st} (g)) \underset{˙}{\leq} R (F) \land 2^{nd} (g) = \underset{˙}{0})\}$

Proof

Step	Hyp	Ref	Expression
1		dvhb1dim.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dvhb1dim.h	$⊢ H = LHyp (K)$
3		dvhb1dim.t	$⊢ T = LTrn (K) (W)$
4		dvhb1dim.r	$⊢ R = trL (K) (W)$
5		dvhb1dim.e	$⊢ E = TEndo (K) (W)$
6		dvhb1dim.o	$⊢ \underset{˙}{0} = (h \in T ⟼ {I ↾}_{B})$
7		eqop	$⊢ g \in (T \times E) \to (g = ⟨s (F), \underset{˙}{0}⟩ \leftrightarrow (1^{st} (g) = s (F) \land 2^{nd} (g) = \underset{˙}{0}))$
8	7	adantl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to (g = ⟨s (F), \underset{˙}{0}⟩ \leftrightarrow (1^{st} (g) = s (F) \land 2^{nd} (g) = \underset{˙}{0}))$
9	8	rexbidv	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to (\exists s \in E g = ⟨s (F), \underset{˙}{0}⟩ \leftrightarrow \exists s \in E (1^{st} (g) = s (F) \land 2^{nd} (g) = \underset{˙}{0}))$
10		r19.41v	$⊢ \exists s \in E (1^{st} (g) = s (F) \land 2^{nd} (g) = \underset{˙}{0}) \leftrightarrow (\exists s \in E 1^{st} (g) = s (F) \land 2^{nd} (g) = \underset{˙}{0})$
11		fvex	$⊢ 1^{st} (g) \in V$
12		eqeq1	$⊢ f = 1^{st} (g) \to (f = s (F) \leftrightarrow 1^{st} (g) = s (F))$
13	12	rexbidv	$⊢ f = 1^{st} (g) \to (\exists s \in E f = s (F) \leftrightarrow \exists s \in E 1^{st} (g) = s (F))$
14	11 13	elab	$⊢ 1^{st} (g) \in \{f \| \exists s \in E f = s (F)\} \leftrightarrow \exists s \in E 1^{st} (g) = s (F)$
15	1 2 3 4 5	dva1dim	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \{f \| \exists s \in E f = s (F)\} = \{f \in T \| R (f) \underset{˙}{\leq} R (F)\}$
16	15	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to \{f \| \exists s \in E f = s (F)\} = \{f \in T \| R (f) \underset{˙}{\leq} R (F)\}$
17	16	eleq2d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to (1^{st} (g) \in \{f \| \exists s \in E f = s (F)\} \leftrightarrow 1^{st} (g) \in \{f \in T \| R (f) \underset{˙}{\leq} R (F)\})$
18	14 17	bitr3id	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to (\exists s \in E 1^{st} (g) = s (F) \leftrightarrow 1^{st} (g) \in \{f \in T \| R (f) \underset{˙}{\leq} R (F)\})$
19		xp1st	$⊢ g \in (T \times E) \to 1^{st} (g) \in T$
20	19	adantl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to 1^{st} (g) \in T$
21		fveq2	$⊢ f = 1^{st} (g) \to R (f) = R (1^{st} (g))$
22	21	breq1d	$⊢ f = 1^{st} (g) \to (R (f) \underset{˙}{\leq} R (F) \leftrightarrow R (1^{st} (g)) \underset{˙}{\leq} R (F))$
23	22	elrab3	$⊢ 1^{st} (g) \in T \to (1^{st} (g) \in \{f \in T \| R (f) \underset{˙}{\leq} R (F)\} \leftrightarrow R (1^{st} (g)) \underset{˙}{\leq} R (F))$
24	20 23	syl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to (1^{st} (g) \in \{f \in T \| R (f) \underset{˙}{\leq} R (F)\} \leftrightarrow R (1^{st} (g)) \underset{˙}{\leq} R (F))$
25	18 24	bitrd	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to (\exists s \in E 1^{st} (g) = s (F) \leftrightarrow R (1^{st} (g)) \underset{˙}{\leq} R (F))$
26	25	anbi1d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to ((\exists s \in E 1^{st} (g) = s (F) \land 2^{nd} (g) = \underset{˙}{0}) \leftrightarrow (R (1^{st} (g)) \underset{˙}{\leq} R (F) \land 2^{nd} (g) = \underset{˙}{0}))$
27	10 26	syl5bb	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to (\exists s \in E (1^{st} (g) = s (F) \land 2^{nd} (g) = \underset{˙}{0}) \leftrightarrow (R (1^{st} (g)) \underset{˙}{\leq} R (F) \land 2^{nd} (g) = \underset{˙}{0}))$
28	9 27	bitrd	$⊢ (((K \in HL \land W \in H) \land F \in T) \land g \in (T \times E)) \to (\exists s \in E g = ⟨s (F), \underset{˙}{0}⟩ \leftrightarrow (R (1^{st} (g)) \underset{˙}{\leq} R (F) \land 2^{nd} (g) = \underset{˙}{0}))$
29	28	rabbidva	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \{g \in (T \times E) \| \exists s \in E g = ⟨s (F), \underset{˙}{0}⟩\} = \{g \in (T \times E) \| (R (1^{st} (g)) \underset{˙}{\leq} R (F) \land 2^{nd} (g) = \underset{˙}{0})\}$

Metamath Proof Explorer

Theorem dvhb1dimN

Proof