hdmap10lem

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

Proof

Step	Hyp	Ref	Expression
1		hdmap10.h	$⊢ H = LHyp (K)$
2		hdmap10.u	$⊢ U = DVecH (K) (W)$
3		hdmap10.v	$⊢ V = {Base}_{U}$
4		hdmap10.n	$⊢ N = LSpan (U)$
5		hdmap10.c	$⊢ C = LCDual (K) (W)$
6		hdmap10.l	$⊢ L = LSpan (C)$
7		hdmap10.m	$⊢ M = mapd (K) (W)$
8		hdmap10.s	$⊢ S = HDMap (K) (W)$
9		hdmap10.k	$⊢ φ \to (K \in HL \land W \in H)$
10		hdmap10.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
11		hdmap10.o	$⊢ \underset{˙}{0} = 0_{U}$
12		hdmap10.d	$⊢ D = {Base}_{C}$
13		hdmap10.j	$⊢ J = HVMap (K) (W)$
14		hdmap10.i	$⊢ I = HDMap1 (K) (W)$
15		hdmap10lem.t	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
18	1 16 17 2 3 11 10 9	dvheveccl	$⊢ φ \to E \in (V ∖ \{\underset{˙}{0}\})$
19	18	eldifad	$⊢ φ \to E \in V$
20	15	eldifad	$⊢ φ \to T \in V$
21	1 2 3 4 9 19 20	dvh3dim	$⊢ φ \to \exists x \in V \neg x \in N (\{E, T\})$
22	9	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to (K \in HL \land W \in H)$
23	20	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to T \in V$
24		simp2	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to x \in V$
25		eqid	$⊢ LSubSp (U) = LSubSp (U)$
26	1 2 9	dvhlmod	$⊢ φ \to U \in LMod$
27	3 25 4 26 19 20	lspprcl	$⊢ φ \to N (\{E, T\}) \in LSubSp (U)$
28	3 4 26 19 20	lspprid1	$⊢ φ \to E \in N (\{E, T\})$
29	25 4 26 27 28	lspsnel5a	$⊢ φ \to N (\{E\}) \subseteq N (\{E, T\})$
30	3 4 26 19 20	lspprid2	$⊢ φ \to T \in N (\{E, T\})$
31	25 4 26 27 30	lspsnel5a	$⊢ φ \to N (\{T\}) \subseteq N (\{E, T\})$
32	29 31	unssd	$⊢ φ \to N (\{E\}) \cup N (\{T\}) \subseteq N (\{E, T\})$
33	32	sseld	$⊢ φ \to (x \in (N (\{E\}) \cup N (\{T\})) \to x \in N (\{E, T\}))$
34	33	con3dimp	$⊢ (φ \land \neg x \in N (\{E, T\})) \to \neg x \in (N (\{E\}) \cup N (\{T\}))$
35	34	3adant2	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to \neg x \in (N (\{E\}) \cup N (\{T\}))$
36	1 10 2 3 4 5 12 13 14 8 22 23 24 35	hdmapval2	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to S (T) = I (⟨x, I (⟨E, J (E), x⟩), T⟩)$
37	36	eqcomd	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to I (⟨x, I (⟨E, J (E), x⟩), T⟩) = S (T)$
38		eqid	$⊢ -_{U} = -_{U}$
39		eqid	$⊢ -_{C} = -_{C}$
40	26	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to U \in LMod$
41	27	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to N (\{E, T\}) \in LSubSp (U)$
42		simp3	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to \neg x \in N (\{E, T\})$
43	11 25 40 41 24 42	lssneln0	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to x \in (V ∖ \{\underset{˙}{0}\})$
44		eqid	$⊢ 0_{C} = 0_{C}$
45	1 2 3 11 5 12 44 13 9 18	hvmapcl2	$⊢ φ \to J (E) \in (D ∖ \{0_{C}\})$
46	45	eldifad	$⊢ φ \to J (E) \in D$
47	46	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to J (E) \in D$
48	1 2 3 11 4 5 6 7 13 9 18	mapdhvmap	$⊢ φ \to M (N (\{E\})) = L (\{J (E)\})$
49	48	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to M (N (\{E\})) = L (\{J (E)\})$
50	1 2 9	dvhlvec	$⊢ φ \to U \in LVec$
51	50	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to U \in LVec$
52	19	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to E \in V$
53	3 4 51 24 52 23 42	lspindpi	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to (N (\{x\}) \neq N (\{E\}) \land N (\{x\}) \neq N (\{T\}))$
54	53	simpld	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to N (\{x\}) \neq N (\{E\})$
55	54	necomd	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to N (\{E\}) \neq N (\{x\})$
56	18	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to E \in (V ∖ \{\underset{˙}{0}\})$
57	1 2 3 11 4 5 12 6 7 14 22 47 49 55 56 24	hdmap1cl	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to I (⟨E, J (E), x⟩) \in D$
58	15	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to T \in (V ∖ \{\underset{˙}{0}\})$
59	1 2 3 5 12 8 9 20	hdmapcl	$⊢ φ \to S (T) \in D$
60	59	3ad2ant1	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to S (T) \in D$
61	53	simprd	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to N (\{x\}) \neq N (\{T\})$
62		eqid	$⊢ I (⟨E, J (E), x⟩) = I (⟨E, J (E), x⟩)$
63	1 2 3 38 11 4 5 12 39 6 7 14 22 56 47 43 57 55 49	hdmap1eq	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to (I (⟨E, J (E), x⟩) = I (⟨E, J (E), x⟩) \leftrightarrow (M (N (\{x\})) = L (\{I (⟨E, J (E), x⟩)\}) \land M (N (\{E -_{U} x\})) = L (\{J (E) -_{C} I (⟨E, J (E), x⟩)\})))$
64	62 63	mpbii	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to (M (N (\{x\})) = L (\{I (⟨E, J (E), x⟩)\}) \land M (N (\{E -_{U} x\})) = L (\{J (E) -_{C} I (⟨E, J (E), x⟩)\}))$
65	64	simpld	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to M (N (\{x\})) = L (\{I (⟨E, J (E), x⟩)\})$
66	1 2 3 38 11 4 5 12 39 6 7 14 22 43 57 58 60 61 65	hdmap1eq	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to (I (⟨x, I (⟨E, J (E), x⟩), T⟩) = S (T) \leftrightarrow (M (N (\{T\})) = L (\{S (T)\}) \land M (N (\{x -_{U} T\})) = L (\{I (⟨E, J (E), x⟩) -_{C} S (T)\})))$
67	37 66	mpbid	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to (M (N (\{T\})) = L (\{S (T)\}) \land M (N (\{x -_{U} T\})) = L (\{I (⟨E, J (E), x⟩) -_{C} S (T)\}))$
68	67	simpld	$⊢ (φ \land x \in V \land \neg x \in N (\{E, T\})) \to M (N (\{T\})) = L (\{S (T)\})$
69	68	rexlimdv3a	$⊢ φ \to (\exists x \in V \neg x \in N (\{E, T\}) \to M (N (\{T\})) = L (\{S (T)\}))$
70	21 69	mpd	$⊢ φ \to M (N (\{T\})) = L (\{S (T)\})$

Metamath Proof Explorer

Theorem hdmap10lem

Proof