dva1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in Crawley p. 120 line 21, but using a non-identity translation (nonzero vector) F whose trace is P rather than P itself; F exists by cdlemf . E is the division ring base by erngdv , and sF is the scalar product by dvavsca . F must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013)

	Ref	Expression
Hypotheses	dva1dim.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dva1dim.h	$⊢ H = LHyp (K)$
	dva1dim.t	$⊢ T = LTrn (K) (W)$
	dva1dim.r	$⊢ R = trL (K) (W)$
	dva1dim.e	$⊢ E = TEndo (K) (W)$
Assertion	dva1dim	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \{g \| \exists s \in E g = s (F)\} = \{g \in T \| R (g) \underset{˙}{\leq} R (F)\}$

Proof

Step	Hyp	Ref	Expression
1		dva1dim.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dva1dim.h	$⊢ H = LHyp (K)$
3		dva1dim.t	$⊢ T = LTrn (K) (W)$
4		dva1dim.r	$⊢ R = trL (K) (W)$
5		dva1dim.e	$⊢ E = TEndo (K) (W)$
6	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in E \land F \in T) \to s (F) \in T$
7	1 2 3 4 5	tendotp	$⊢ ((K \in HL \land W \in H) \land s \in E \land F \in T) \to R (s (F)) \underset{˙}{\leq} R (F)$
8	6 7	jca	$⊢ ((K \in HL \land W \in H) \land s \in E \land F \in T) \to (s (F) \in T \land R (s (F)) \underset{˙}{\leq} R (F))$
9	8	3expb	$⊢ ((K \in HL \land W \in H) \land (s \in E \land F \in T)) \to (s (F) \in T \land R (s (F)) \underset{˙}{\leq} R (F))$
10	9	anass1rs	$⊢ (((K \in HL \land W \in H) \land F \in T) \land s \in E) \to (s (F) \in T \land R (s (F)) \underset{˙}{\leq} R (F))$
11		eleq1	$⊢ g = s (F) \to (g \in T \leftrightarrow s (F) \in T)$
12		fveq2	$⊢ g = s (F) \to R (g) = R (s (F))$
13	12	breq1d	$⊢ g = s (F) \to (R (g) \underset{˙}{\leq} R (F) \leftrightarrow R (s (F)) \underset{˙}{\leq} R (F))$
14	11 13	anbi12d	$⊢ g = s (F) \to ((g \in T \land R (g) \underset{˙}{\leq} R (F)) \leftrightarrow (s (F) \in T \land R (s (F)) \underset{˙}{\leq} R (F)))$
15	10 14	syl5ibrcom	$⊢ (((K \in HL \land W \in H) \land F \in T) \land s \in E) \to (g = s (F) \to (g \in T \land R (g) \underset{˙}{\leq} R (F)))$
16	15	rexlimdva	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists s \in E g = s (F) \to (g \in T \land R (g) \underset{˙}{\leq} R (F)))$
17		simpll	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (g \in T \land R (g) \underset{˙}{\leq} R (F))) \to (K \in HL \land W \in H)$
18		simplr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (g \in T \land R (g) \underset{˙}{\leq} R (F))) \to F \in T$
19		simprl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (g \in T \land R (g) \underset{˙}{\leq} R (F))) \to g \in T$
20		simprr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (g \in T \land R (g) \underset{˙}{\leq} R (F))) \to R (g) \underset{˙}{\leq} R (F)$
21	1 2 3 4 5	tendoex	$⊢ ((K \in HL \land W \in H) \land (F \in T \land g \in T) \land R (g) \underset{˙}{\leq} R (F)) \to \exists s \in E s (F) = g$
22	17 18 19 20 21	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (g \in T \land R (g) \underset{˙}{\leq} R (F))) \to \exists s \in E s (F) = g$
23		eqcom	$⊢ s (F) = g \leftrightarrow g = s (F)$
24	23	rexbii	$⊢ \exists s \in E s (F) = g \leftrightarrow \exists s \in E g = s (F)$
25	22 24	sylib	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (g \in T \land R (g) \underset{˙}{\leq} R (F))) \to \exists s \in E g = s (F)$
26	25	ex	$⊢ ((K \in HL \land W \in H) \land F \in T) \to ((g \in T \land R (g) \underset{˙}{\leq} R (F)) \to \exists s \in E g = s (F))$
27	16 26	impbid	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\exists s \in E g = s (F) \leftrightarrow (g \in T \land R (g) \underset{˙}{\leq} R (F)))$
28	27	abbidv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \{g \| \exists s \in E g = s (F)\} = \{g \| (g \in T \land R (g) \underset{˙}{\leq} R (F))\}$
29		df-rab	$⊢ \{g \in T \| R (g) \underset{˙}{\leq} R (F)\} = \{g \| (g \in T \land R (g) \underset{˙}{\leq} R (F))\}$
30	28 29	eqtr4di	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \{g \| \exists s \in E g = s (F)\} = \{g \in T \| R (g) \underset{˙}{\leq} R (F)\}$

Metamath Proof Explorer

Theorem dva1dim

Proof