hdmap11lem2

	Ref	Expression
Hypotheses	hdmap11.h	$⊢ H = LHyp (K)$
	hdmap11.u	$⊢ U = DVecH (K) (W)$
	hdmap11.v	$⊢ V = {Base}_{U}$
	hdmap11.p	$⊢ \underset{˙}{+} = +_{U}$
	hdmap11.c	$⊢ C = LCDual (K) (W)$
	hdmap11.a	$⊢ \underset{˙}{✚} = +_{C}$
	hdmap11.s	$⊢ S = HDMap (K) (W)$
	hdmap11.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap11.x	$⊢ φ \to X \in V$
	hdmap11.y	$⊢ φ \to Y \in V$
	hdmap11.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
	hdmap11.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap11.n	$⊢ N = LSpan (U)$
	hdmap11.d	$⊢ D = {Base}_{C}$
	hdmap11.l	$⊢ L = LSpan (C)$
	hdmap11.m	$⊢ M = mapd (K) (W)$
	hdmap11.j	$⊢ J = HVMap (K) (W)$
	hdmap11.i	$⊢ I = HDMap1 (K) (W)$
Assertion	hdmap11lem2	$⊢ φ \to S (X \underset{˙}{+} Y) = S (X) \underset{˙}{✚} S (Y)$

Proof

Step	Hyp	Ref	Expression
1		hdmap11.h	$⊢ H = LHyp (K)$
2		hdmap11.u	$⊢ U = DVecH (K) (W)$
3		hdmap11.v	$⊢ V = {Base}_{U}$
4		hdmap11.p	$⊢ \underset{˙}{+} = +_{U}$
5		hdmap11.c	$⊢ C = LCDual (K) (W)$
6		hdmap11.a	$⊢ \underset{˙}{✚} = +_{C}$
7		hdmap11.s	$⊢ S = HDMap (K) (W)$
8		hdmap11.k	$⊢ φ \to (K \in HL \land W \in H)$
9		hdmap11.x	$⊢ φ \to X \in V$
10		hdmap11.y	$⊢ φ \to Y \in V$
11		hdmap11.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
12		hdmap11.o	$⊢ \underset{˙}{0} = 0_{U}$
13		hdmap11.n	$⊢ N = LSpan (U)$
14		hdmap11.d	$⊢ D = {Base}_{C}$
15		hdmap11.l	$⊢ L = LSpan (C)$
16		hdmap11.m	$⊢ M = mapd (K) (W)$
17		hdmap11.j	$⊢ J = HVMap (K) (W)$
18		hdmap11.i	$⊢ I = HDMap1 (K) (W)$
19	1 2 3 13 8 9 10	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y\})$
20	19	adantr	$⊢ (φ \land E \in N (\{X, Y\})) \to \exists z \in V \neg z \in N (\{X, Y\})$
21		eqid	$⊢ LSubSp (U) = LSubSp (U)$
22	1 2 8	dvhlmod	$⊢ φ \to U \in LMod$
23	22	adantr	$⊢ (φ \land E \in N (\{X, Y\})) \to U \in LMod$
24	3 21 13 22 9 10	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
25	24	adantr	$⊢ (φ \land E \in N (\{X, Y\})) \to N (\{X, Y\}) \in LSubSp (U)$
26		simpr	$⊢ (φ \land E \in N (\{X, Y\})) \to E \in N (\{X, Y\})$
27	21 13 23 25 26	ellspsn5	$⊢ (φ \land E \in N (\{X, Y\})) \to N (\{E\}) \subseteq N (\{X, Y\})$
28	27	ssneld	$⊢ (φ \land E \in N (\{X, Y\})) \to (\neg z \in N (\{X, Y\}) \to \neg z \in N (\{E\}))$
29	28	ancld	$⊢ (φ \land E \in N (\{X, Y\})) \to (\neg z \in N (\{X, Y\}) \to (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\})))$
30	29	reximdv	$⊢ (φ \land E \in N (\{X, Y\})) \to (\exists z \in V \neg z \in N (\{X, Y\}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\})))$
31	20 30	mpd	$⊢ (φ \land E \in N (\{X, Y\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))$
32		eqid	$⊢ {Base}_{K} = {Base}_{K}$
33		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
34	1 32 33 2 3 12 11 8	dvheveccl	$⊢ φ \to E \in (V ∖ \{\underset{˙}{0}\})$
35	34	eldifad	$⊢ φ \to E \in V$
36	1 2 3 13 8 35 10	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{E, Y\})$
37	36	adantr	$⊢ (φ \land X = \underset{˙}{0}) \to \exists z \in V \neg z \in N (\{E, Y\})$
38		preq1	$⊢ X = \underset{˙}{0} \to \{X, Y\} = \{\underset{˙}{0}, Y\}$
39		prcom	$⊢ \{\underset{˙}{0}, Y\} = \{Y, \underset{˙}{0}\}$
40	38 39	eqtrdi	$⊢ X = \underset{˙}{0} \to \{X, Y\} = \{Y, \underset{˙}{0}\}$
41	40	fveq2d	$⊢ X = \underset{˙}{0} \to N (\{X, Y\}) = N (\{Y, \underset{˙}{0}\})$
42	3 12 13 22 10	lsppr0	$⊢ φ \to N (\{Y, \underset{˙}{0}\}) = N (\{Y\})$
43	41 42	sylan9eqr	$⊢ (φ \land X = \underset{˙}{0}) \to N (\{X, Y\}) = N (\{Y\})$
44	3 21 13 22 35 10	lspprcl	$⊢ φ \to N (\{E, Y\}) \in LSubSp (U)$
45	3 13 22 35 10	lspprid2	$⊢ φ \to Y \in N (\{E, Y\})$
46	21 13 22 44 45	ellspsn5	$⊢ φ \to N (\{Y\}) \subseteq N (\{E, Y\})$
47	46	adantr	$⊢ (φ \land X = \underset{˙}{0}) \to N (\{Y\}) \subseteq N (\{E, Y\})$
48	43 47	eqsstrd	$⊢ (φ \land X = \underset{˙}{0}) \to N (\{X, Y\}) \subseteq N (\{E, Y\})$
49	48	ssneld	$⊢ (φ \land X = \underset{˙}{0}) \to (\neg z \in N (\{E, Y\}) \to \neg z \in N (\{X, Y\}))$
50	3 13 22 35 10	lspprid1	$⊢ φ \to E \in N (\{E, Y\})$
51	21 13 22 44 50	ellspsn5	$⊢ φ \to N (\{E\}) \subseteq N (\{E, Y\})$
52	51	adantr	$⊢ (φ \land X = \underset{˙}{0}) \to N (\{E\}) \subseteq N (\{E, Y\})$
53	52	ssneld	$⊢ (φ \land X = \underset{˙}{0}) \to (\neg z \in N (\{E, Y\}) \to \neg z \in N (\{E\}))$
54	49 53	jcad	$⊢ (φ \land X = \underset{˙}{0}) \to (\neg z \in N (\{E, Y\}) \to (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\})))$
55	54	reximdv	$⊢ (φ \land X = \underset{˙}{0}) \to (\exists z \in V \neg z \in N (\{E, Y\}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\})))$
56	37 55	mpd	$⊢ (φ \land X = \underset{˙}{0}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))$
57	56	adantlr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X = \underset{˙}{0}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))$
58	3 4	lmodvacl	$⊢ (U \in LMod \land E \in V \land X \in V) \to E \underset{˙}{+} X \in V$
59	22 35 9 58	syl3anc	$⊢ φ \to E \underset{˙}{+} X \in V$
60	59	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to E \underset{˙}{+} X \in V$
61	22	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to U \in LMod$
62	24	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to N (\{X, Y\}) \in LSubSp (U)$
63	3 13 22 9 10	lspprid1	$⊢ φ \to X \in N (\{X, Y\})$
64	63	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to X \in N (\{X, Y\})$
65	35	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to E \in V$
66		simplr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to \neg E \in N (\{X, Y\})$
67	3 4 21 61 62 64 65 66	lssvancl2	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to \neg E \underset{˙}{+} X \in N (\{X, Y\})$
68	3 21 13	lspsncl	$⊢ (U \in LMod \land E \in V) \to N (\{E\}) \in LSubSp (U)$
69	22 35 68	syl2anc	$⊢ φ \to N (\{E\}) \in LSubSp (U)$
70	69	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to N (\{E\}) \in LSubSp (U)$
71	3 13	lspsnid	$⊢ (U \in LMod \land E \in V) \to E \in N (\{E\})$
72	22 35 71	syl2anc	$⊢ φ \to E \in N (\{E\})$
73	72	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to E \in N (\{E\})$
74	9	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to X \in V$
75	1 2 8	dvhlvec	$⊢ φ \to U \in LVec$
76	75	ad2antrr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to U \in LVec$
77		simpr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to X \neq \underset{˙}{0}$
78		eldifsn	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in V \land X \neq \underset{˙}{0})$
79	74 77 78	sylanbrc	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
80	21 13 22 24 63	ellspsn5	$⊢ φ \to N (\{X\}) \subseteq N (\{X, Y\})$
81	80	sseld	$⊢ φ \to (E \in N (\{X\}) \to E \in N (\{X, Y\}))$
82	81	con3dimp	$⊢ (φ \land \neg E \in N (\{X, Y\})) \to \neg E \in N (\{X\})$
83	82	adantr	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to \neg E \in N (\{X\})$
84	3 12 13 76 65 79 83	lspsnnecom	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to \neg X \in N (\{E\})$
85	3 4 21 61 70 73 74 84	lssvancl1	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to \neg E \underset{˙}{+} X \in N (\{E\})$
86		eleq1	$⊢ z = E \underset{˙}{+} X \to (z \in N (\{X, Y\}) \leftrightarrow E \underset{˙}{+} X \in N (\{X, Y\}))$
87	86	notbid	$⊢ z = E \underset{˙}{+} X \to (\neg z \in N (\{X, Y\}) \leftrightarrow \neg E \underset{˙}{+} X \in N (\{X, Y\}))$
88		eleq1	$⊢ z = E \underset{˙}{+} X \to (z \in N (\{E\}) \leftrightarrow E \underset{˙}{+} X \in N (\{E\}))$
89	88	notbid	$⊢ z = E \underset{˙}{+} X \to (\neg z \in N (\{E\}) \leftrightarrow \neg E \underset{˙}{+} X \in N (\{E\}))$
90	87 89	anbi12d	$⊢ z = E \underset{˙}{+} X \to ((\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\})) \leftrightarrow (\neg E \underset{˙}{+} X \in N (\{X, Y\}) \land \neg E \underset{˙}{+} X \in N (\{E\})))$
91	90	rspcev	$⊢ (E \underset{˙}{+} X \in V \land (\neg E \underset{˙}{+} X \in N (\{X, Y\}) \land \neg E \underset{˙}{+} X \in N (\{E\}))) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))$
92	60 67 85 91	syl12anc	$⊢ ((φ \land \neg E \in N (\{X, Y\})) \land X \neq \underset{˙}{0}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))$
93	57 92	pm2.61dane	$⊢ (φ \land \neg E \in N (\{X, Y\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))$
94	31 93	pm2.61dan	$⊢ φ \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))$
95	8	3ad2ant1	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to (K \in HL \land W \in H)$
96	9	3ad2ant1	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to X \in V$
97	10	3ad2ant1	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to Y \in V$
98		simp2	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to z \in V$
99		simp3l	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to \neg z \in N (\{X, Y\})$
100	22	3ad2ant1	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to U \in LMod$
101	35	3ad2ant1	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to E \in V$
102		simp3r	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to \neg z \in N (\{E\})$
103	3 13 100 98 101 102	lspsnne2	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to N (\{z\}) \neq N (\{E\})$
104	1 2 3 4 5 6 7 95 96 97 11 12 13 14 15 16 17 18 98 99 103	hdmap11lem1	$⊢ (φ \land z \in V \land (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\}))) \to S (X \underset{˙}{+} Y) = S (X) \underset{˙}{✚} S (Y)$
105	104	rexlimdv3a	$⊢ φ \to (\exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{E\})) \to S (X \underset{˙}{+} Y) = S (X) \underset{˙}{✚} S (Y))$
106	94 105	mpd	$⊢ φ \to S (X \underset{˙}{+} Y) = S (X) \underset{˙}{✚} S (Y)$

Metamath Proof Explorer

Theorem hdmap11lem2

Proof