hdmaprnlem9N

Description: Part of proof of part 12 in Baer p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 and mapdcnv11N . Use better hypotheses and/or theorems? (Contributed by NM, 27-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}$
	hdmaprnlem1.t2	$⊢ φ \to t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})$
	hdmaprnlem1.p	$⊢ \underset{˙}{+} = +_{U}$
	hdmaprnlem1.pt	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) = M (N (\{u \underset{˙}{+} t\}))$
Assertion	hdmaprnlem9N	$⊢ φ \to s = S (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		hdmaprnlem1.t2	$⊢ φ \to t \in (N (\{v\}) ∖ \{\underset{˙}{0}\})$
20		hdmaprnlem1.p	$⊢ \underset{˙}{+} = +_{U}$
21		hdmaprnlem1.pt	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) = M (N (\{u \underset{˙}{+} t\}))$
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	hdmaprnlem7N	$⊢ φ \to s -_{C} S (t) \in L (\{S (u) \underset{˙}{✚} s\})$
23	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	hdmaprnlem8N	$⊢ φ \to s -_{C} S (t) \in M (N (\{t\}))$
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	hdmaprnlem4N	$⊢ φ \to M (N (\{t\})) = L (\{s\})$
25	23 24	eleqtrd	$⊢ φ \to s -_{C} S (t) \in L (\{s\})$
26	22 25	elind	$⊢ φ \to s -_{C} S (t) \in (L (\{S (u) \underset{˙}{✚} s\}) \cap L (\{s\}))$
27	1 5 9	lcdlvec	$⊢ φ \to C \in LVec$
28	1 5 9	lcdlmod	$⊢ φ \to C \in LMod$
29	1 2 3 5 15 8 9 13	hdmapcl	$⊢ φ \to S (u) \in D$
30	10	eldifad	$⊢ φ \to s \in D$
31	15 18	lmodvacl	$⊢ (C \in LMod \land S (u) \in D \land s \in D) \to S (u) \underset{˙}{✚} s \in D$
32	28 29 30 31	syl3anc	$⊢ φ \to S (u) \underset{˙}{✚} s \in D$
33		eqid	$⊢ LSubSp (C) = LSubSp (C)$
34	15 33 6	lspsncl	$⊢ (C \in LMod \land s \in D) \to L (\{s\}) \in LSubSp (C)$
35	28 30 34	syl2anc	$⊢ φ \to L (\{s\}) \in LSubSp (C)$
36	1 7 5 33 9	mapdrn2	$⊢ φ \to ran M = LSubSp (C)$
37	35 36	eleqtrrd	$⊢ φ \to L (\{s\}) \in ran M$
38	1 7 9 37	mapdcnvid2	$⊢ φ \to M (M^{-1} (L (\{s\}))) = L (\{s\})$
39	12 38	eqtr4d	$⊢ φ \to M (N (\{v\})) = M (M^{-1} (L (\{s\})))$
40		eqid	$⊢ LSubSp (U) = LSubSp (U)$
41	1 2 9	dvhlmod	$⊢ φ \to U \in LMod$
42	3 40 4	lspsncl	$⊢ (U \in LMod \land v \in V) \to N (\{v\}) \in LSubSp (U)$
43	41 11 42	syl2anc	$⊢ φ \to N (\{v\}) \in LSubSp (U)$
44	1 7 2 40 9 37	mapdcnvcl	$⊢ φ \to M^{-1} (L (\{s\})) \in LSubSp (U)$
45	1 2 40 7 9 43 44	mapd11	$⊢ φ \to (M (N (\{v\})) = M (M^{-1} (L (\{s\}))) \leftrightarrow N (\{v\}) = M^{-1} (L (\{s\})))$
46	39 45	mpbid	$⊢ φ \to N (\{v\}) = M^{-1} (L (\{s\}))$
47	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\}))$
48	46 47	eqnetrrd	$⊢ φ \to M^{-1} (L (\{s\})) \neq M^{-1} (L (\{S (u) \underset{˙}{✚} s\}))$
49	15 33 6	lspsncl	$⊢ (C \in LMod \land S (u) \underset{˙}{✚} s \in D) \to L (\{S (u) \underset{˙}{✚} s\}) \in LSubSp (C)$
50	28 32 49	syl2anc	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \in LSubSp (C)$
51	50 36	eleqtrrd	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \in ran M$
52	1 7 9 37 51	mapdcnv11N	$⊢ φ \to (M^{-1} (L (\{s\})) = M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) \leftrightarrow L (\{s\}) = L (\{S (u) \underset{˙}{✚} s\}))$
53	52	necon3bid	$⊢ φ \to (M^{-1} (L (\{s\})) \neq M^{-1} (L (\{S (u) \underset{˙}{✚} s\})) \leftrightarrow L (\{s\}) \neq L (\{S (u) \underset{˙}{✚} s\}))$
54	48 53	mpbid	$⊢ φ \to L (\{s\}) \neq L (\{S (u) \underset{˙}{✚} s\})$
55	54	necomd	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \neq L (\{s\})$
56	15 16 6 27 32 30 55	lspdisj2	$⊢ φ \to L (\{S (u) \underset{˙}{✚} s\}) \cap L (\{s\}) = \{Q\}$
57	26 56	eleqtrd	$⊢ φ \to s -_{C} S (t) \in \{Q\}$
58		elsni	$⊢ s -_{C} S (t) \in \{Q\} \to s -_{C} S (t) = Q$
59	57 58	syl	$⊢ φ \to s -_{C} S (t) = Q$
60	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	hdmaprnlem4tN	$⊢ φ \to t \in V$
61	1 2 3 5 15 8 9 60	hdmapcl	$⊢ φ \to S (t) \in D$
62		eqid	$⊢ -_{C} = -_{C}$
63	15 16 62	lmodsubeq0	$⊢ (C \in LMod \land s \in D \land S (t) \in D) \to (s -_{C} S (t) = Q \leftrightarrow s = S (t))$
64	28 30 61 63	syl3anc	$⊢ φ \to (s -_{C} S (t) = Q \leftrightarrow s = S (t))$
65	59 64	mpbid	$⊢ φ \to s = S (t)$

Metamath Proof Explorer

Theorem hdmaprnlem9N

Proof