Theorem hgmaprnlem2N

Description: Lemma for hgmaprnN . Part 15 of Baer p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero z is taken care of automatically. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hgmaprnlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hgmaprnlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hgmaprnlem1.v	$$⊢V={\mathrm{Base}}_U$$
	hgmaprnlem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hgmaprnlem1.b	$$⊢B={\mathrm{Base}}_R$$
	hgmaprnlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hgmaprnlem1.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hgmaprnlem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hgmaprnlem1.d	$$⊢D={\mathrm{Base}}_C$$
	hgmaprnlem1.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
	hgmaprnlem1.a	$$⊢A={\mathrm{Base}}_P$$
	hgmaprnlem1.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hgmaprnlem1.q	$$⊢Q=0_C$$
	hgmaprnlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hgmaprnlem1.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hgmaprnlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hgmaprnlem1.z	$$⊢\phi \to z\in A$$
	hgmaprnlem1.t2	$$⊢\phi \to t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hgmaprnlem1.s2	$$⊢\phi \to s\in V$$
	hgmaprnlem1.sz	$$⊢\phi \to S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)$$
	hgmaprnlem1.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hgmaprnlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hgmaprnlem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
Assertion	hgmaprnlem2N	$$⊢\phi \to N\left(\left\{s\right\}\right)\subseteq N\left(\left\{t\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hgmaprnlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmaprnlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmaprnlem1.v	$$⊢V={\mathrm{Base}}_U$$
4		hgmaprnlem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		hgmaprnlem1.b	$$⊢B={\mathrm{Base}}_R$$
6		hgmaprnlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		hgmaprnlem1.o	$$⊢\underset{\dot{}}{0}=0_U$$
8		hgmaprnlem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		hgmaprnlem1.d	$$⊢D={\mathrm{Base}}_C$$
10		hgmaprnlem1.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
11		hgmaprnlem1.a	$$⊢A={\mathrm{Base}}_P$$
12		hgmaprnlem1.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
13		hgmaprnlem1.q	$$⊢Q=0_C$$
14		hgmaprnlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
15		hgmaprnlem1.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
16		hgmaprnlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		hgmaprnlem1.z	$$⊢\phi \to z\in A$$
18		hgmaprnlem1.t2	$$⊢\phi \to t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19		hgmaprnlem1.s2	$$⊢\phi \to s\in V$$
20		hgmaprnlem1.sz	$$⊢\phi \to S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)$$
21		hgmaprnlem1.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
22		hgmaprnlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
23		hgmaprnlem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
24	1 8 16	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
25	18	eldifad	$$⊢\phi \to t\in V$$
26	1 2 3 8 9 14 16 25	hdmapcl	$$⊢\phi \to S\left(t\right)\in D$$
27	10 11 9 12 23	lspsnvsi	$$⊢\left(C\in \mathrm{LMod}\wedge z\in A\wedge S\left(t\right)\in D\right)\to L\left(\left\{z\underset{\dot{}}{\bullet }S\left(t\right)\right\}\right)\subseteq L\left(\left\{S\left(t\right)\right\}\right)$$
28	24 17 26 27	syl3anc	$$⊢\phi \to L\left(\left\{z\underset{\dot{}}{\bullet }S\left(t\right)\right\}\right)\subseteq L\left(\left\{S\left(t\right)\right\}\right)$$
29	1 2 3 22 8 23 21 14 16 19	hdmap10	$$⊢\phi \to M\left(N\left(\left\{s\right\}\right)\right)=L\left(\left\{S\left(s\right)\right\}\right)$$
30	20	sneqd	$$⊢\phi \to \left\{S\left(s\right)\right\}=\left\{z\underset{\dot{}}{\bullet }S\left(t\right)\right\}$$
31	30	fveq2d	$$⊢\phi \to L\left(\left\{S\left(s\right)\right\}\right)=L\left(\left\{z\underset{\dot{}}{\bullet }S\left(t\right)\right\}\right)$$
32	29 31	eqtrd	$$⊢\phi \to M\left(N\left(\left\{s\right\}\right)\right)=L\left(\left\{z\underset{\dot{}}{\bullet }S\left(t\right)\right\}\right)$$
33	1 2 3 22 8 23 21 14 16 25	hdmap10	$$⊢\phi \to M\left(N\left(\left\{t\right\}\right)\right)=L\left(\left\{S\left(t\right)\right\}\right)$$
34	28 32 33	3sstr4d	$$⊢\phi \to M\left(N\left(\left\{s\right\}\right)\right)\subseteq M\left(N\left(\left\{t\right\}\right)\right)$$
35		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
36	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
37	3 35 22	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge s\in V\right)\to N\left(\left\{s\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
38	36 19 37	syl2anc	$$⊢\phi \to N\left(\left\{s\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
39	3 35 22	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge t\in V\right)\to N\left(\left\{t\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
40	36 25 39	syl2anc	$$⊢\phi \to N\left(\left\{t\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
41	1 2 35 21 16 38 40	mapdord	$$⊢\phi \to \left(M\left(N\left(\left\{s\right\}\right)\right)\subseteq M\left(N\left(\left\{t\right\}\right)\right)\leftrightarrow N\left(\left\{s\right\}\right)\subseteq N\left(\left\{t\right\}\right)\right)$$
42	34 41	mpbid	$$⊢\phi \to N\left(\left\{s\right\}\right)\subseteq N\left(\left\{t\right\}\right)$$