mapdpg

Description: Part 1 of proof of the first fundamental theorem of projective geometry. Part (1) in Baer p. 44. Our notation corresponds to Baer's as follows: M for *, N{ } for F(), J{ } for G(), X for x, G for x', Y for y, h for y'. TODO: Rename variables per mapdhval . (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	mapdpg.h	$⊢ H = LHyp (K)$
	mapdpg.m	$⊢ M = mapd (K) (W)$
	mapdpg.u	$⊢ U = DVecH (K) (W)$
	mapdpg.v	$⊢ V = {Base}_{U}$
	mapdpg.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdpg.z	$⊢ \underset{˙}{0} = 0_{U}$
	mapdpg.n	$⊢ N = LSpan (U)$
	mapdpg.c	$⊢ C = LCDual (K) (W)$
	mapdpg.f	$⊢ F = {Base}_{C}$
	mapdpg.r	$⊢ R = -_{C}$
	mapdpg.j	$⊢ J = LSpan (C)$
	mapdpg.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdpg.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdpg.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdpg.g	$⊢ φ \to G \in F$
	mapdpg.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdpg.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
Assertion	mapdpg	$⊢ φ \to \exists! h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$

Proof

Step	Hyp	Ref	Expression
1		mapdpg.h	$⊢ H = LHyp (K)$
2		mapdpg.m	$⊢ M = mapd (K) (W)$
3		mapdpg.u	$⊢ U = DVecH (K) (W)$
4		mapdpg.v	$⊢ V = {Base}_{U}$
5		mapdpg.s	$⊢ \underset{˙}{-} = -_{U}$
6		mapdpg.z	$⊢ \underset{˙}{0} = 0_{U}$
7		mapdpg.n	$⊢ N = LSpan (U)$
8		mapdpg.c	$⊢ C = LCDual (K) (W)$
9		mapdpg.f	$⊢ F = {Base}_{C}$
10		mapdpg.r	$⊢ R = -_{C}$
11		mapdpg.j	$⊢ J = LSpan (C)$
12		mapdpg.k	$⊢ φ \to (K \in HL \land W \in H)$
13		mapdpg.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
14		mapdpg.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
15		mapdpg.g	$⊢ φ \to G \in F$
16		mapdpg.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
17		mapdpg.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	mapdpglem24	$⊢ φ \to \exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$
19	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	mapdpglem32	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to h = i$
20	19	3exp	$⊢ φ \to ((h \in F \land i \in F) \to (((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\}))) \to h = i))$
21	20	ralrimivv	$⊢ φ \to \forall h \in F \forall i \in F (((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\}))) \to h = i)$
22		sneq	$⊢ h = i \to \{h\} = \{i\}$
23	22	fveq2d	$⊢ h = i \to J (\{h\}) = J (\{i\})$
24	23	eqeq2d	$⊢ h = i \to (M (N (\{Y\})) = J (\{h\}) \leftrightarrow M (N (\{Y\})) = J (\{i\}))$
25		oveq2	$⊢ h = i \to G R h = G R i$
26	25	sneqd	$⊢ h = i \to \{G R h\} = \{G R i\}$
27	26	fveq2d	$⊢ h = i \to J (\{G R h\}) = J (\{G R i\})$
28	27	eqeq2d	$⊢ h = i \to (M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}) \leftrightarrow M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\}))$
29	24 28	anbi12d	$⊢ h = i \to ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \leftrightarrow (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))$
30	29	reu4	$⊢ \exists! h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \leftrightarrow (\exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land \forall h \in F \forall i \in F (((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\}))) \to h = i))$
31	18 21 30	sylanbrc	$⊢ φ \to \exists! h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$

Metamath Proof Explorer

Theorem mapdpg

Proof