hdmap1l6j

Description: Lemmma for hdmap1l6 . Eliminate ( N { Y } ) = ( N { Z } ) hypothesis. (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}\})$
Assertion	hdmap1l6j	$⊢ φ \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	16	adantr	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to (K \in HL \land W \in H)$
24	17	adantr	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to F \in D$
25	18	adantr	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
26	19	adantr	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to M (N (\{X\})) = L (\{F\})$
27	20	adantr	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to \neg X \in N (\{Y, Z\})$
28	21	adantr	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
29	22	adantr	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to Z \in (V ∖ \{\underset{˙}{0}\})$
30		simpr	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to N (\{Y\}) = N (\{Z\})$
31	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 23 24 25 26 27 28 29 30	hdmap1l6i	$⊢ (φ \land N (\{Y\}) = N (\{Z\})) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$
32	16	adantr	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to (K \in HL \land W \in H)$
33	17	adantr	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to F \in D$
34	18	adantr	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
35	19	adantr	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to M (N (\{X\})) = L (\{F\})$
36	21	adantr	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
37	22	adantr	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to Z \in (V ∖ \{\underset{˙}{0}\})$
38	20	adantr	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to \neg X \in N (\{Y, Z\})$
39		simpr	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to N (\{Y\}) \neq N (\{Z\})$
40		eqidd	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to I (⟨X, F, Y⟩) = I (⟨X, F, Y⟩)$
41		eqidd	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to I (⟨X, F, Z⟩) = I (⟨X, F, Z⟩)$
42	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 32 33 34 35 36 37 38 39 40 41	hdmap1l6a	$⊢ (φ \land N (\{Y\}) \neq N (\{Z\})) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$
43	31 42	pm2.61dane	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$

Metamath Proof Explorer

Theorem hdmap1l6j

Proof