dia1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A (when F is a nonzero vector i.e. non-identity translation). Remark after Lemma L in Crawley p. 120 line 21. (Contributed by NM, 15-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dia1dim.h	$⊢ H = LHyp (K)$
	dia1dim.t	$⊢ T = LTrn (K) (W)$
	dia1dim.r	$⊢ R = trL (K) (W)$
	dia1dim.e	$⊢ E = TEndo (K) (W)$
	dia1dim.i	$⊢ I = DIsoA (K) (W)$
Assertion	dia1dim	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{g \| \exists s \in E g = s (F)\}$

Proof

Step	Hyp	Ref	Expression
1		dia1dim.h	$⊢ H = LHyp (K)$
2		dia1dim.t	$⊢ T = LTrn (K) (W)$
3		dia1dim.r	$⊢ R = trL (K) (W)$
4		dia1dim.e	$⊢ E = TEndo (K) (W)$
5		dia1dim.i	$⊢ I = DIsoA (K) (W)$
6		simpl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (K \in HL \land W \in H)$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 1 2 3	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
9		eqid	$⊢ \leq_{K} = \leq_{K}$
10	9 1 2 3	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \leq_{K} W$
11	7 9 1 2 3 5	diaval	$⊢ ((K \in HL \land W \in H) \land (R (F) \in {Base}_{K} \land R (F) \leq_{K} W)) \to I (R (F)) = \{g \in T \| R (g) \leq_{K} R (F)\}$
12	6 8 10 11	syl12anc	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{g \in T \| R (g) \leq_{K} R (F)\}$
13	9 1 2 3 4	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) \leq_{K} R (F)\}$
14	12 13	eqtr4d	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = \{g \| \exists s \in E g = s (F)\}$

Metamath Proof Explorer

Theorem dia1dim

Proof