Theorem dochexmidlem7

Description: Lemma for dochexmid . Contradict dochexmidlem6 . (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	dochexmidlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochexmidlem1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochexmidlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochexmidlem1.v	$$⊢V={\mathrm{Base}}_U$$
	dochexmidlem1.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	dochexmidlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dochexmidlem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dochexmidlem1.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	dochexmidlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochexmidlem1.x	$$⊢\phi \to X\in S$$
	dochexmidlem6.pp	$$⊢\phi \to p\in A$$
	dochexmidlem6.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochexmidlem6.m	$$⊢M=X\underset{\dot{}}{\oplus }p$$
	dochexmidlem6.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
	dochexmidlem6.c	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X$$
	dochexmidlem6.pl	$$⊢\phi \to \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
Assertion	dochexmidlem7	$$⊢\phi \to M\ne X$$

Proof

Step	Hyp	Ref	Expression
1		dochexmidlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochexmidlem1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochexmidlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochexmidlem1.v	$$⊢V={\mathrm{Base}}_U$$
5		dochexmidlem1.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
6		dochexmidlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		dochexmidlem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
8		dochexmidlem1.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
9		dochexmidlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		dochexmidlem1.x	$$⊢\phi \to X\in S$$
11		dochexmidlem6.pp	$$⊢\phi \to p\in A$$
12		dochexmidlem6.z	$$⊢\underset{\dot{}}{0}=0_U$$
13		dochexmidlem6.m	$$⊢M=X\underset{\dot{}}{\oplus }p$$
14		dochexmidlem6.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
15		dochexmidlem6.c	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X$$
16		dochexmidlem6.pl	$$⊢\phi \to \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
17	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18	5	lsssssubg	$$⊢U\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(U\right)$$
19	17 18	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(U\right)$$
20	19 10	sseldd	$$⊢\phi \to X\in \mathrm{SubGrp}\left(U\right)$$
21	5 8 17 11	lsatlssel	$$⊢\phi \to p\in S$$
22	19 21	sseldd	$$⊢\phi \to p\in \mathrm{SubGrp}\left(U\right)$$
23	7	lsmub2	$$⊢\left(X\in \mathrm{SubGrp}\left(U\right)\wedge p\in \mathrm{SubGrp}\left(U\right)\right)\to p\subseteq X\underset{\dot{}}{\oplus }p$$
24	20 22 23	syl2anc	$$⊢\phi \to p\subseteq X\underset{\dot{}}{\oplus }p$$
25	24 13	sseqtrrdi	$$⊢\phi \to p\subseteq M$$
26	4 5	lssss	$$⊢X\in S\to X\subseteq V$$
27	10 26	syl	$$⊢\phi \to X\subseteq V$$
28	1 3 4 5 2	dochlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq V\right)\to \underset{\dot{}}{\perp }\left(X\right)\in S$$
29	9 27 28	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\in S$$
30	19 29	sseldd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\in \mathrm{SubGrp}\left(U\right)$$
31	7	lsmub1	$$⊢\left(X\in \mathrm{SubGrp}\left(U\right)\wedge \underset{\dot{}}{\perp }\left(X\right)\in \mathrm{SubGrp}\left(U\right)\right)\to X\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
32	20 30 31	syl2anc	$$⊢\phi \to X\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
33		sstr2	$$⊢p\subseteq X\to \left(X\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)$$
34	32 33	syl5com	$$⊢\phi \to \left(p\subseteq X\to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)$$
35	16 34	mtod	$$⊢\phi \to \neg p\subseteq X$$
36		sseq2	$$⊢M=X\to \left(p\subseteq M\leftrightarrow p\subseteq X\right)$$
37	36	biimpcd	$$⊢p\subseteq M\to \left(M=X\to p\subseteq X\right)$$
38	37	necon3bd	$$⊢p\subseteq M\to \left(\neg p\subseteq X\to M\ne X\right)$$
39	25 35 38	sylc	$$⊢\phi \to M\ne X$$