mapdpglem25

Description: Lemma for mapdpg . Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-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\})$
	mapdpgem25.h1	$⊢ φ \to (h \in F \land (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})))$
	mapdpgem25.i1	$⊢ φ \to (i \in F \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))$
Assertion	mapdpglem25	$⊢ φ \to (J (\{h\}) = J (\{i\}) \land J (\{G R h\}) = J (\{G R i\}))$

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		mapdpgem25.h1	$⊢ φ \to (h \in F \land (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})))$
19		mapdpgem25.i1	$⊢ φ \to (i \in F \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))$
20	18	simprd	$⊢ φ \to (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$
21	20	simpld	$⊢ φ \to M (N (\{Y\})) = J (\{h\})$
22	19	simprd	$⊢ φ \to (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\}))$
23	22	simpld	$⊢ φ \to M (N (\{Y\})) = J (\{i\})$
24	21 23	eqtr3d	$⊢ φ \to J (\{h\}) = J (\{i\})$
25	20	simprd	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})$
26	22	simprd	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})$
27	25 26	eqtr3d	$⊢ φ \to J (\{G R h\}) = J (\{G R i\})$
28	24 27	jca	$⊢ φ \to (J (\{h\}) = J (\{i\}) \land J (\{G R h\}) = J (\{G R i\}))$

Metamath Proof Explorer

Theorem mapdpglem25

Proof