Theorem hdmaprnlem3N

Description: Part of proof of part 12 in Baer p. 49 line 15, T =/= P. Our (`' M `( L{ ( ( Su ) .+b s ) } ) ) is Baer's P, where P* = G(u'+s). (Contributed by NM, 27-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmaprnlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmaprnlem1.v	$$⊢V={\mathrm{Base}}_U$$
	hdmaprnlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmaprnlem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmaprnlem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmaprnlem1.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmaprnlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmaprnlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmaprnlem1.se	$$⊢\phi \to s\in \left(D\setminus \left\{Q\right\}\right)$$
	hdmaprnlem1.ve	$$⊢\phi \to v\in V$$
	hdmaprnlem1.e	$$⊢\phi \to M\left(N\left(\left\{v\right\}\right)\right)=L\left(\left\{s\right\}\right)$$
	hdmaprnlem1.ue	$$⊢\phi \to u\in V$$
	hdmaprnlem1.un	$$⊢\phi \to \neg u\in N\left(\left\{v\right\}\right)$$
	hdmaprnlem1.d	$$⊢D={\mathrm{Base}}_C$$
	hdmaprnlem1.q	$$⊢Q=0_C$$
	hdmaprnlem1.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmaprnlem1.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
Assertion	hdmaprnlem3N	$$⊢\phi \to N\left(\left\{v\right\}\right)\ne M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmaprnlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmaprnlem1.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmaprnlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
5		hdmaprnlem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmaprnlem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
7		hdmaprnlem1.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
8		hdmaprnlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
9		hdmaprnlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		hdmaprnlem1.se	$$⊢\phi \to s\in \left(D\setminus \left\{Q\right\}\right)$$
11		hdmaprnlem1.ve	$$⊢\phi \to v\in V$$
12		hdmaprnlem1.e	$$⊢\phi \to M\left(N\left(\left\{v\right\}\right)\right)=L\left(\left\{s\right\}\right)$$
13		hdmaprnlem1.ue	$$⊢\phi \to u\in V$$
14		hdmaprnlem1.un	$$⊢\phi \to \neg u\in N\left(\left\{v\right\}\right)$$
15		hdmaprnlem1.d	$$⊢D={\mathrm{Base}}_C$$
16		hdmaprnlem1.q	$$⊢Q=0_C$$
17		hdmaprnlem1.o	$$⊢\underset{\dot{}}{0}=0_U$$
18		hdmaprnlem1.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
19	1 5 9	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
20	1 2 3 5 15 8 9 13	hdmapcl	$$⊢\phi \to S\left(u\right)\in D$$
21	10	eldifad	$$⊢\phi \to s\in D$$
22	15 18	lmodvacl	$$⊢\left(C\in \mathrm{LMod}\wedge S\left(u\right)\in D\wedge s\in D\right)\to S\left(u\right)\underset{\dot{}}{✚}s\in D$$
23	19 20 21 22	syl3anc	$$⊢\phi \to S\left(u\right)\underset{\dot{}}{✚}s\in D$$
24		eqid	$$⊢\mathrm{LSubSp}\left(C\right)=\mathrm{LSubSp}\left(C\right)$$
25	15 24 6	lspsncl	$$⊢\left(C\in \mathrm{LMod}\wedge s\in D\right)\to L\left(\left\{s\right\}\right)\in \mathrm{LSubSp}\left(C\right)$$
26	19 21 25	syl2anc	$$⊢\phi \to L\left(\left\{s\right\}\right)\in \mathrm{LSubSp}\left(C\right)$$
27	15 6	lspsnid	$$⊢\left(C\in \mathrm{LMod}\wedge s\in D\right)\to s\in L\left(\left\{s\right\}\right)$$
28	19 21 27	syl2anc	$$⊢\phi \to s\in L\left(\left\{s\right\}\right)$$
29	1 5 9	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
30		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
31	1 2 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
32	3 30 4	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge v\in V\right)\to N\left(\left\{v\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
33	31 11 32	syl2anc	$$⊢\phi \to N\left(\left\{v\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
34	17 30 31 33 13 14	lssneln0	$$⊢\phi \to u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
35	1 2 3 17 5 16 15 8 9 34	hdmapnzcl	$$⊢\phi \to S\left(u\right)\in \left(D\setminus \left\{Q\right\}\right)$$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14	hdmaprnlem1N	$$⊢\phi \to L\left(\left\{S\left(u\right)\right\}\right)\ne L\left(\left\{s\right\}\right)$$
37	15 16 6 29 35 21 36	lspsnne1	$$⊢\phi \to \neg S\left(u\right)\in L\left(\left\{s\right\}\right)$$
38	15 18 24 19 26 28 20 37	lssvancl2	$$⊢\phi \to \neg S\left(u\right)\underset{\dot{}}{✚}s\in L\left(\left\{s\right\}\right)$$
39	15 6 19 23 21 38	lspsnne2	$$⊢\phi \to L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\ne L\left(\left\{s\right\}\right)$$
40	39	necomd	$$⊢\phi \to L\left(\left\{s\right\}\right)\ne L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)$$
41	15 24 6	lspsncl	$$⊢\left(C\in \mathrm{LMod}\wedge S\left(u\right)\underset{\dot{}}{✚}s\in D\right)\to L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\in \mathrm{LSubSp}\left(C\right)$$
42	19 23 41	syl2anc	$$⊢\phi \to L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\in \mathrm{LSubSp}\left(C\right)$$
43	1 7 5 24 9	mapdrn2	$$⊢\phi \to \mathrm{ran}M=\mathrm{LSubSp}\left(C\right)$$
44	42 43	eleqtrrd	$$⊢\phi \to L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\in \mathrm{ran}M$$
45	1 7 9 44	mapdcnvid2	$$⊢\phi \to M\left(M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)\right)=L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)$$
46	40 12 45	3netr4d	$$⊢\phi \to M\left(N\left(\left\{v\right\}\right)\right)\ne M\left(M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)\right)$$
47	1 7 2 30 9 44	mapdcnvcl	$$⊢\phi \to M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)\in \mathrm{LSubSp}\left(U\right)$$
48	1 2 30 7 9 33 47	mapd11	$$⊢\phi \to \left(M\left(N\left(\left\{v\right\}\right)\right)=M\left(M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)\right)\leftrightarrow N\left(\left\{v\right\}\right)=M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)\right)$$
49	48	necon3bid	$$⊢\phi \to \left(M\left(N\left(\left\{v\right\}\right)\right)\ne M\left(M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)\right)\leftrightarrow N\left(\left\{v\right\}\right)\ne M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)\right)$$
50	46 49	mpbid	$$⊢\phi \to N\left(\left\{v\right\}\right)\ne M^{-1}\left(L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)\right)$$