mapdpglem29

Description: Lemma for mapdpg . Baer p. 45 line 16: "But Gx' and Gy'' are distinct points and so x' and y'' are independent elements in B. (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\})$
	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\})))$
	mapdpglem26.a	$⊢ A = Scalar (U)$
	mapdpglem26.b	$⊢ B = {Base}_{A}$
	mapdpglem26.t	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
	mapdpglem26.o	$⊢ O = 0_{A}$
	mapdpglem28.ve	$⊢ φ \to v \in B$
	mapdpglem28.u1	$⊢ φ \to h = u \underset{˙}{\cdot} i$
	mapdpglem28.u2	$⊢ φ \to G R h = v \underset{˙}{\cdot} (G R i)$
Assertion	mapdpglem29	$⊢ φ \to J (\{G\}) \neq J (\{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		mapdpglem26.a	$⊢ A = Scalar (U)$
21		mapdpglem26.b	$⊢ B = {Base}_{A}$
22		mapdpglem26.t	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
23		mapdpglem26.o	$⊢ O = 0_{A}$
24		mapdpglem28.ve	$⊢ φ \to v \in B$
25		mapdpglem28.u1	$⊢ φ \to h = u \underset{˙}{\cdot} i$
26		mapdpglem28.u2	$⊢ φ \to G R h = v \underset{˙}{\cdot} (G R i)$
27		eqid	$⊢ LSubSp (U) = LSubSp (U)$
28	1 3 12	dvhlmod	$⊢ φ \to U \in LMod$
29	13	eldifad	$⊢ φ \to X \in V$
30	4 27 7	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
31	28 29 30	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
32	14	eldifad	$⊢ φ \to Y \in V$
33	4 27 7	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
34	28 32 33	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
35	1 3 27 2 12 31 34	mapd11	$⊢ φ \to (M (N (\{X\})) = M (N (\{Y\})) \leftrightarrow N (\{X\}) = N (\{Y\}))$
36	35	necon3bid	$⊢ φ \to (M (N (\{X\})) \neq M (N (\{Y\})) \leftrightarrow N (\{X\}) \neq N (\{Y\}))$
37	16 36	mpbird	$⊢ φ \to M (N (\{X\})) \neq M (N (\{Y\}))$
38	19	simprd	$⊢ φ \to (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\}))$
39	38	simpld	$⊢ φ \to M (N (\{Y\})) = J (\{i\})$
40	37 17 39	3netr3d	$⊢ φ \to J (\{G\}) \neq J (\{i\})$

Metamath Proof Explorer

Theorem mapdpglem29

Proof