hdmaprnlem8N

Description: Part of proof of part 12 in Baer p. 49 line 19, s-St e. (Ft)* = T*. (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	hdmaprnlem8N	$⊢ φ \to s -_{C} S (t) \in M (N (\{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 5 9	lcdlmod	$⊢ φ \to C \in LMod$
23		eqid	$⊢ LSubSp (U) = LSubSp (U)$
24		eqid	$⊢ LSubSp (C) = LSubSp (C)$
25	1 2 9	dvhlmod	$⊢ φ \to U \in LMod$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	hdmaprnlem4tN	$⊢ φ \to t \in V$
27	3 23 4	lspsncl	$⊢ (U \in LMod \land t \in V) \to N (\{t\}) \in LSubSp (U)$
28	25 26 27	syl2anc	$⊢ φ \to N (\{t\}) \in LSubSp (U)$
29	1 7 2 23 5 24 9 28	mapdcl2	$⊢ φ \to M (N (\{t\})) \in LSubSp (C)$
30	10	eldifad	$⊢ φ \to s \in D$
31	15 6	lspsnid	$⊢ (C \in LMod \land s \in D) \to s \in L (\{s\})$
32	22 30 31	syl2anc	$⊢ φ \to s \in L (\{s\})$
33	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\})$
34	32 33	eleqtrrd	$⊢ φ \to s \in M (N (\{t\}))$
35	1 2 3 5 15 8 9 26	hdmapcl	$⊢ φ \to S (t) \in D$
36	15 6	lspsnid	$⊢ (C \in LMod \land S (t) \in D) \to S (t) \in L (\{S (t)\})$
37	22 35 36	syl2anc	$⊢ φ \to S (t) \in L (\{S (t)\})$
38	1 2 3 4 5 6 7 8 9 26	hdmap10	$⊢ φ \to M (N (\{t\})) = L (\{S (t)\})$
39	37 38	eleqtrrd	$⊢ φ \to S (t) \in M (N (\{t\}))$
40		eqid	$⊢ -_{C} = -_{C}$
41	40 24	lssvsubcl	$⊢ ((C \in LMod \land M (N (\{t\})) \in LSubSp (C)) \land (s \in M (N (\{t\})) \land S (t) \in M (N (\{t\})))) \to s -_{C} S (t) \in M (N (\{t\}))$
42	22 29 34 39 41	syl22anc	$⊢ φ \to s -_{C} S (t) \in M (N (\{t\}))$

Metamath Proof Explorer

Theorem hdmaprnlem8N

Proof