hdmaprnlem3eN

Description: Lemma for hdmaprnN . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem1.h	$⊢ H = LHyp (K)$
	hdmaprnlem1.u	$⊢ U = DVecH (K) (W)$
	hdmaprnlem1.v	$⊢ V = {Base}_{U}$
	hdmaprnlem1.n	$⊢ N = LSpan (U)$
	hdmaprnlem1.c	$⊢ C = LCDual (K) (W)$
	hdmaprnlem1.l	$⊢ L = LSpan (C)$
	hdmaprnlem1.m	$⊢ M = mapd (K) (W)$
	hdmaprnlem1.s	$⊢ S = HDMap (K) (W)$
	hdmaprnlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmaprnlem1.se	$⊢ φ \to s \in (D ∖ \{Q\})$
	hdmaprnlem1.ve	$⊢ φ \to v \in V$
	hdmaprnlem1.e	$⊢ φ \to M (N (\{v\})) = L (\{s\})$
	hdmaprnlem1.ue	$⊢ φ \to u \in V$
	hdmaprnlem1.un	$⊢ φ \to \neg u \in N (\{v\})$
	hdmaprnlem1.d	$⊢ D = {Base}_{C}$
	hdmaprnlem1.q	$⊢ Q = 0_{C}$
	hdmaprnlem1.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmaprnlem1.a	$⊢ \underset{˙}{✚} = +_{C}$
	hdmaprnlem3e.p	$⊢ \underset{˙}{+} = +_{U}$
Assertion	hdmaprnlem3eN	$⊢ φ \to \exists t \in (N (\{v\}) ∖ \{\underset{˙}{0}\}) L (\{S (u) \underset{˙}{✚} s\}) = M (N (\{u \underset{˙}{+} t\}))$

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem1.h	$⊢ H = LHyp (K)$
2		hdmaprnlem1.u	$⊢ U = DVecH (K) (W)$
3		hdmaprnlem1.v	$⊢ V = {Base}_{U}$
4		hdmaprnlem1.n	$⊢ N = LSpan (U)$
5		hdmaprnlem1.c	$⊢ C = LCDual (K) (W)$
6		hdmaprnlem1.l	$⊢ L = LSpan (C)$
7		hdmaprnlem1.m	$⊢ M = mapd (K) (W)$
8		hdmaprnlem1.s	$⊢ S = HDMap (K) (W)$
9		hdmaprnlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
10		hdmaprnlem1.se	$⊢ φ \to s \in (D ∖ \{Q\})$
11		hdmaprnlem1.ve	$⊢ φ \to v \in V$
12		hdmaprnlem1.e	$⊢ φ \to M (N (\{v\})) = L (\{s\})$
13		hdmaprnlem1.ue	$⊢ φ \to u \in V$
14		hdmaprnlem1.un	$⊢ φ \to \neg u \in N (\{v\})$
15		hdmaprnlem1.d	$⊢ D = {Base}_{C}$
16		hdmaprnlem1.q	$⊢ Q = 0_{C}$
17		hdmaprnlem1.o	$⊢ \underset{˙}{0} = 0_{U}$
18		hdmaprnlem1.a	$⊢ \underset{˙}{✚} = +_{C}$
19		hdmaprnlem3e.p	$⊢ \underset{˙}{+} = +_{U}$
20		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
21	1 2 9	dvhlvec	$⊢ φ \to U \in LVec$
22		eqid	$⊢ LSAtoms (C) = LSAtoms (C)$
23	1 5 9	lcdlmod	$⊢ φ \to C \in LMod$
24	1 2 3 5 15 8 9 13	hdmapcl	$⊢ φ \to S (u) \in D$
25	10	eldifad	$⊢ φ \to s \in D$
26	15 18	lmodvacl	$⊢ (C \in LMod \land S (u) \in D \land s \in D) \to S (u) \underset{˙}{✚} s \in D$
27	23 24 25 26	syl3anc	$⊢ φ \to S (u) \underset{˙}{✚} s \in D$
28	1 2 3 4 5 6 7 8 9 10 11 12 13 14	hdmaprnlem1N	$⊢ φ \to L (\{S (u)\}) \neq L (\{s\})$
29	15 18 16 6 23 24 25 28	lmodindp1	$⊢ φ \to S (u) \underset{˙}{✚} s \neq Q$
30		eldifsn	$⊢ S (u) \underset{˙}{✚} s \in (D ∖ \{Q\}) \leftrightarrow (S (u) \underset{˙}{✚} s \in D \land S (u) \underset{˙}{✚} s \neq Q)$
31	27 29 30	sylanbrc	$⊢ φ \to S (u) \underset{˙}{✚} s \in (D ∖ \{Q\})$
32	15 6 16 22 23 31	lsatlspsn	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \in LSAtoms (C)$
33	1 7 2 20 5 22 9 32	mapdcnvatN	$⊢ φ \to M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) \in LSAtoms (U)$
34	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hdmaprnlem3uN	$⊢ φ \to N (\{u\}) \neq M^{-1} (L (\{S (u) \underset{˙}{✚} s\}))$
35	34	necomd	$⊢ φ \to M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) \neq N (\{u\})$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hdmaprnlem3N	$⊢ φ \to N (\{v\}) \neq M^{-1} (L (\{S (u) \underset{˙}{✚} s\}))$
37	36	necomd	$⊢ φ \to M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) \neq N (\{v\})$
38		eqid	$⊢ LSubSp (C) = LSubSp (C)$
39		eqid	$⊢ LSubSp (U) = LSubSp (U)$
40	1 2 9	dvhlmod	$⊢ φ \to U \in LMod$
41	3 39 4	lspsncl	$⊢ (U \in LMod \land u \in V) \to N (\{u\}) \in LSubSp (U)$
42	40 13 41	syl2anc	$⊢ φ \to N (\{u\}) \in LSubSp (U)$
43	1 7 2 39 5 38 9 42	mapdcl2	$⊢ φ \to M (N (\{u\})) \in LSubSp (C)$
44	3 39 4	lspsncl	$⊢ (U \in LMod \land v \in V) \to N (\{v\}) \in LSubSp (U)$
45	40 11 44	syl2anc	$⊢ φ \to N (\{v\}) \in LSubSp (U)$
46	1 7 2 39 5 38 9 45	mapdcl2	$⊢ φ \to M (N (\{v\})) \in LSubSp (C)$
47		eqid	$⊢ LSSum (C) = LSSum (C)$
48	38 47	lsmcl	$⊢ (C \in LMod \land M (N (\{u\})) \in LSubSp (C) \land M (N (\{v\})) \in LSubSp (C)) \to M (N (\{u\})) LSSum (C) M (N (\{v\})) \in LSubSp (C)$
49	23 43 46 48	syl3anc	$⊢ φ \to M (N (\{u\})) LSSum (C) M (N (\{v\})) \in LSubSp (C)$
50	38	lsssssubg	$⊢ C \in LMod \to LSubSp (C) \subseteq SubGrp (C)$
51	23 50	syl	$⊢ φ \to LSubSp (C) \subseteq SubGrp (C)$
52	51 43	sseldd	$⊢ φ \to M (N (\{u\})) \in SubGrp (C)$
53	51 46	sseldd	$⊢ φ \to M (N (\{v\})) \in SubGrp (C)$
54	15 6	lspsnid	$⊢ (C \in LMod \land S (u) \in D) \to S (u) \in L (\{S (u)\})$
55	23 24 54	syl2anc	$⊢ φ \to S (u) \in L (\{S (u)\})$
56	1 2 3 4 5 6 7 8 9 13	hdmap10	$⊢ φ \to M (N (\{u\})) = L (\{S (u)\})$
57	55 56	eleqtrrd	$⊢ φ \to S (u) \in M (N (\{u\}))$
58		eqimss2	$⊢ M (N (\{v\})) = L (\{s\}) \to L (\{s\}) \subseteq M (N (\{v\}))$
59	12 58	syl	$⊢ φ \to L (\{s\}) \subseteq M (N (\{v\}))$
60	15 38 6 23 46 25	lspsnel5	$⊢ φ \to (s \in M (N (\{v\})) \leftrightarrow L (\{s\}) \subseteq M (N (\{v\})))$
61	59 60	mpbird	$⊢ φ \to s \in M (N (\{v\}))$
62	18 47	lsmelvali	$⊢ ((M (N (\{u\})) \in SubGrp (C) \land M (N (\{v\})) \in SubGrp (C)) \land (S (u) \in M (N (\{u\})) \land s \in M (N (\{v\})))) \to S (u) \underset{˙}{✚} s \in (M (N (\{u\})) LSSum (C) M (N (\{v\})))$
63	52 53 57 61 62	syl22anc	$⊢ φ \to S (u) \underset{˙}{✚} s \in (M (N (\{u\})) LSSum (C) M (N (\{v\})))$
64	38 6 23 49 63	lspsnel5a	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \subseteq M (N (\{u\})) LSSum (C) M (N (\{v\}))$
65		eqid	$⊢ LSSum (U) = LSSum (U)$
66	1 7 2 39 65 5 47 9 42 45	mapdlsm	$⊢ φ \to M (N (\{u\}) LSSum (U) N (\{v\})) = M (N (\{u\})) LSSum (C) M (N (\{v\}))$
67	64 66	sseqtrrd	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \subseteq M (N (\{u\}) LSSum (U) N (\{v\}))$
68	15 38 6	lspsncl	$⊢ (C \in LMod \land S (u) \underset{˙}{✚} s \in D) \to L (\{S (u) \underset{˙}{✚} s\}) \in LSubSp (C)$
69	23 27 68	syl2anc	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \in LSubSp (C)$
70	1 7 5 38 9	mapdrn2	$⊢ φ \to ran M = LSubSp (C)$
71	69 70	eleqtrrd	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \in ran M$
72	39 65	lsmcl	$⊢ (U \in LMod \land N (\{u\}) \in LSubSp (U) \land N (\{v\}) \in LSubSp (U)) \to N (\{u\}) LSSum (U) N (\{v\}) \in LSubSp (U)$
73	40 42 45 72	syl3anc	$⊢ φ \to N (\{u\}) LSSum (U) N (\{v\}) \in LSubSp (U)$
74	1 7 2 39 9 73	mapdcl	$⊢ φ \to M (N (\{u\}) LSSum (U) N (\{v\})) \in ran M$
75	1 7 9 71 74	mapdcnvordN	$⊢ φ \to (M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) \subseteq M^{-1} (M (N (\{u\}) LSSum (U) N (\{v\}))) \leftrightarrow L (\{S (u) \underset{˙}{✚} s\}) \subseteq M (N (\{u\}) LSSum (U) N (\{v\})))$
76	67 75	mpbird	$⊢ φ \to M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) \subseteq M^{-1} (M (N (\{u\}) LSSum (U) N (\{v\})))$
77	3 4 65 40 13 11	lsmpr	$⊢ φ \to N (\{u, v\}) = N (\{u\}) LSSum (U) N (\{v\})$
78	1 7 2 39 9 73	mapdcnvid1N	$⊢ φ \to M^{-1} (M (N (\{u\}) LSSum (U) N (\{v\}))) = N (\{u\}) LSSum (U) N (\{v\})$
79	77 78	eqtr4d	$⊢ φ \to N (\{u, v\}) = M^{-1} (M (N (\{u\}) LSSum (U) N (\{v\})))$
80	76 79	sseqtrrd	$⊢ φ \to M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) \subseteq N (\{u, v\})$
81	3 19 17 4 20 21 33 13 11 35 37 80	lsatfixedN	$⊢ φ \to \exists t \in (N (\{v\}) ∖ \{\underset{˙}{0}\}) M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})$
82		simpr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})$
83	9	ad2antrr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to (K \in HL \land W \in H)$
84	40	ad2antrr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to U \in LMod$
85	13	ad2antrr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to u \in V$
86	10	ad2antrr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to s \in (D ∖ \{Q\})$
87	11	ad2antrr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to v \in V$
88	12	ad2antrr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to M (N (\{v\})) = L (\{s\})$
89	14	ad2antrr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to \neg u \in N (\{v\})$
90		simplr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})$
91	1 2 3 4 5 6 7 8 83 86 87 88 85 89 15 16 17 18 90	hdmaprnlem4tN	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to t \in V$
92	3 19	lmodvacl	$⊢ (U \in LMod \land u \in V \land t \in V) \to u \underset{˙}{+} t \in V$
93	84 85 91 92	syl3anc	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to u \underset{˙}{+} t \in V$
94	3 39 4	lspsncl	$⊢ (U \in LMod \land u \underset{˙}{+} t \in V) \to N (\{u \underset{˙}{+} t\}) \in LSubSp (U)$
95	84 93 94	syl2anc	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to N (\{u \underset{˙}{+} t\}) \in LSubSp (U)$
96	1 7 2 39 83 95	mapdcnvid1N	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to M^{-1} (M (N (\{u \underset{˙}{+} t\}))) = N (\{u \underset{˙}{+} t\})$
97	82 96	eqtr4d	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = M^{-1} (M (N (\{u \underset{˙}{+} t\})))$
98	71	ad2antrr	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to L (\{S (u) \underset{˙}{✚} s\}) \in ran M$
99	1 7 2 39 83 95	mapdcl	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to M (N (\{u \underset{˙}{+} t\})) \in ran M$
100	1 7 83 98 99	mapdcnv11N	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to (M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = M^{-1} (M (N (\{u \underset{˙}{+} t\}))) \leftrightarrow L (\{S (u) \underset{˙}{✚} s\}) = M (N (\{u \underset{˙}{+} t\})))$
101	97 100	mpbid	$⊢ ((φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \land M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\})) \to L (\{S (u) \underset{˙}{✚} s\}) = M (N (\{u \underset{˙}{+} t\}))$
102	101	ex	$⊢ (φ \land t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})) \to (M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\}) \to L (\{S (u) \underset{˙}{✚} s\}) = M (N (\{u \underset{˙}{+} t\})))$
103	102	reximdva	$⊢ φ \to (\exists t \in (N (\{v\}) ∖ \{\underset{˙}{0}\}) M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) = N (\{u \underset{˙}{+} t\}) \to \exists t \in (N (\{v\}) ∖ \{\underset{˙}{0}\}) L (\{S (u) \underset{˙}{✚} s\}) = M (N (\{u \underset{˙}{+} t\})))$
104	81 103	mpd	$⊢ φ \to \exists t \in (N (\{v\}) ∖ \{\underset{˙}{0}\}) L (\{S (u) \underset{˙}{✚} s\}) = M (N (\{u \underset{˙}{+} t\}))$

Metamath Proof Explorer

Theorem hdmaprnlem3eN

Proof