hdmap1l6i

Description: Lemmma for hdmap1l6 . Eliminate auxiliary vector w . (Contributed by NM, 1-May-2015)

	Ref	Expression
Hypotheses	hdmap1l6.h	$⊢ H = LHyp (K)$
	hdmap1l6.u	$⊢ U = DVecH (K) (W)$
	hdmap1l6.v	$⊢ V = {Base}_{U}$
	hdmap1l6.p	$⊢ \underset{˙}{+} = +_{U}$
	hdmap1l6.s	$⊢ \underset{˙}{-} = -_{U}$
	hdmap1l6c.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap1l6.n	$⊢ N = LSpan (U)$
	hdmap1l6.c	$⊢ C = LCDual (K) (W)$
	hdmap1l6.d	$⊢ D = {Base}_{C}$
	hdmap1l6.a	$⊢ \underset{˙}{✚} = +_{C}$
	hdmap1l6.r	$⊢ R = -_{C}$
	hdmap1l6.q	$⊢ Q = 0_{C}$
	hdmap1l6.l	$⊢ L = LSpan (C)$
	hdmap1l6.m	$⊢ M = mapd (K) (W)$
	hdmap1l6.i	$⊢ I = HDMap1 (K) (W)$
	hdmap1l6.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap1l6.f	$⊢ φ \to F \in D$
	hdmap1l6cl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6.mn	$⊢ φ \to M (N (\{X\})) = L (\{F\})$
	hdmap1l6i.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	hdmap1l6i.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6i.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6i.yz	$⊢ φ \to N (\{Y\}) = N (\{Z\})$
Assertion	hdmap1l6i	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$

Proof

Step	Hyp	Ref	Expression
1		hdmap1l6.h	$⊢ H = LHyp (K)$
2		hdmap1l6.u	$⊢ U = DVecH (K) (W)$
3		hdmap1l6.v	$⊢ V = {Base}_{U}$
4		hdmap1l6.p	$⊢ \underset{˙}{+} = +_{U}$
5		hdmap1l6.s	$⊢ \underset{˙}{-} = -_{U}$
6		hdmap1l6c.o	$⊢ \underset{˙}{0} = 0_{U}$
7		hdmap1l6.n	$⊢ N = LSpan (U)$
8		hdmap1l6.c	$⊢ C = LCDual (K) (W)$
9		hdmap1l6.d	$⊢ D = {Base}_{C}$
10		hdmap1l6.a	$⊢ \underset{˙}{✚} = +_{C}$
11		hdmap1l6.r	$⊢ R = -_{C}$
12		hdmap1l6.q	$⊢ Q = 0_{C}$
13		hdmap1l6.l	$⊢ L = LSpan (C)$
14		hdmap1l6.m	$⊢ M = mapd (K) (W)$
15		hdmap1l6.i	$⊢ I = HDMap1 (K) (W)$
16		hdmap1l6.k	$⊢ φ \to (K \in HL \land W \in H)$
17		hdmap1l6.f	$⊢ φ \to F \in D$
18		hdmap1l6cl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
19		hdmap1l6.mn	$⊢ φ \to M (N (\{X\})) = L (\{F\})$
20		hdmap1l6i.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
21		hdmap1l6i.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
22		hdmap1l6i.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
23		hdmap1l6i.yz	$⊢ φ \to N (\{Y\}) = N (\{Z\})$
24	18	eldifad	$⊢ φ \to X \in V$
25	21	eldifad	$⊢ φ \to Y \in V$
26	1 2 3 7 16 24 25	dvh3dim	$⊢ φ \to \exists w \in V \neg w \in N (\{X, Y\})$
27	16	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to (K \in HL \land W \in H)$
28	17	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to F \in D$
29	18	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
30	19	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to M (N (\{X\})) = L (\{F\})$
31	20	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to \neg X \in N (\{Y, Z\})$
32	23	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{Y\}) = N (\{Z\})$
33	21	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
34	22	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to Z \in (V ∖ \{\underset{˙}{0}\})$
35		eqid	$⊢ LSubSp (U) = LSubSp (U)$
36	1 2 16	dvhlmod	$⊢ φ \to U \in LMod$
37	36	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to U \in LMod$
38	3 35 7 36 24 25	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
39	38	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{X, Y\}) \in LSubSp (U)$
40		simp2	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to w \in V$
41		simp3	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to \neg w \in N (\{X, Y\})$
42	6 35 37 39 40 41	lssneln0	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to w \in (V ∖ \{\underset{˙}{0}\})$
43	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 27 28 29 30 31 32 33 34 42 41	hdmap1l6h	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$
44	43	rexlimdv3a	$⊢ φ \to (\exists w \in V \neg w \in N (\{X, Y\}) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))$
45	26 44	mpd	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$

Metamath Proof Explorer

Theorem hdmap1l6i

Proof