Theorem mapdpglem5N

Description: Lemma for mapdpg . (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdpglem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdpglem.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdpglem.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdpglem.v	$$⊢V={\mathrm{Base}}_U$$
	mapdpglem.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdpglem.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdpglem.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdpglem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdpglem.x	$$⊢\phi \to X\in V$$
	mapdpglem.y	$$⊢\phi \to Y\in V$$
	mapdpglem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(C\right)$$
	mapdpglem2.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdpglem3.f	$$⊢F={\mathrm{Base}}_C$$
	mapdpglem3.te	$$⊢\phi \to t\in \left(M\left(N\left(\left\{X\right\}\right)\right)\underset{\dot{}}{\oplus }M\left(N\left(\left\{Y\right\}\right)\right)\right)$$
	mapdpglem3.a	$$⊢A=\mathrm{Scalar}\left(U\right)$$
	mapdpglem3.b	$$⊢B={\mathrm{Base}}_A$$
	mapdpglem3.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
	mapdpglem3.r	$$⊢R={-}_C$$
	mapdpglem3.g	$$⊢\phi \to G\in F$$
	mapdpglem3.e	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{G\right\}\right)$$
	mapdpglem4.q	$$⊢Q=0_U$$
	mapdpglem.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	mapdpglem4.jt	$$⊢\phi \to M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{t\right\}\right)$$
Assertion	mapdpglem5N	$$⊢\phi \to t\ne 0_C$$

Proof

Step	Hyp	Ref	Expression
1		mapdpglem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdpglem.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
3		mapdpglem.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		mapdpglem.v	$$⊢V={\mathrm{Base}}_U$$
5		mapdpglem.s	$$⊢\underset{\dot{}}{-}={-}_U$$
6		mapdpglem.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		mapdpglem.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		mapdpglem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		mapdpglem.x	$$⊢\phi \to X\in V$$
10		mapdpglem.y	$$⊢\phi \to Y\in V$$
11		mapdpglem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(C\right)$$
12		mapdpglem2.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
13		mapdpglem3.f	$$⊢F={\mathrm{Base}}_C$$
14		mapdpglem3.te	$$⊢\phi \to t\in \left(M\left(N\left(\left\{X\right\}\right)\right)\underset{\dot{}}{\oplus }M\left(N\left(\left\{Y\right\}\right)\right)\right)$$
15		mapdpglem3.a	$$⊢A=\mathrm{Scalar}\left(U\right)$$
16		mapdpglem3.b	$$⊢B={\mathrm{Base}}_A$$
17		mapdpglem3.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
18		mapdpglem3.r	$$⊢R={-}_C$$
19		mapdpglem3.g	$$⊢\phi \to G\in F$$
20		mapdpglem3.e	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{G\right\}\right)$$
21		mapdpglem4.q	$$⊢Q=0_U$$
22		mapdpglem.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
23		mapdpglem4.jt	$$⊢\phi \to M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{t\right\}\right)$$
24		eqid	$$⊢\mathrm{LSAtoms}\left(U\right)=\mathrm{LSAtoms}\left(U\right)$$
25		eqid	$$⊢\mathrm{LSAtoms}\left(C\right)=\mathrm{LSAtoms}\left(C\right)$$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22	mapdpglem4N	$$⊢\phi \to X\underset{\dot{}}{-}Y\ne Q$$
27	1 3 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
28	4 5	lmodvsubcl	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{-}Y\in V$$
29	27 9 10 28	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Y\in V$$
30	4 6 21 24 27 29	lsatspn0	$$⊢\phi \to \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\in \mathrm{LSAtoms}\left(U\right)\leftrightarrow X\underset{\dot{}}{-}Y\ne Q\right)$$
31	26 30	mpbird	$$⊢\phi \to N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\in \mathrm{LSAtoms}\left(U\right)$$
32	1 2 3 24 7 25 8 31	mapdat	$$⊢\phi \to M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)\in \mathrm{LSAtoms}\left(C\right)$$
33	23 32	eqeltrrd	$$⊢\phi \to J\left(\left\{t\right\}\right)\in \mathrm{LSAtoms}\left(C\right)$$
34		eqid	$$⊢0_C=0_C$$
35	1 7 8	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14	mapdpglem2a	$$⊢\phi \to t\in F$$
37	13 12 34 25 35 36	lsatspn0	$$⊢\phi \to \left(J\left(\left\{t\right\}\right)\in \mathrm{LSAtoms}\left(C\right)\leftrightarrow t\ne 0_C\right)$$
38	33 37	mpbid	$$⊢\phi \to t\ne 0_C$$