Theorem dvh3dimatN

Description: There is an atom that is outside the subspace sum of 2 others. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvh4dimat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvh4dimat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dvh3dimat.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dvh3dimat.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	dvh3dimat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dvh3dimat.p	$$⊢\phi \to P\in A$$
	dvh3dimat.q	$$⊢\phi \to Q\in A$$
Assertion	dvh3dimatN	$$⊢\phi \to \exists s\in A\neg s\subseteq P\underset{\dot{}}{\oplus }Q$$

Proof

Step	Hyp	Ref	Expression
1		dvh4dimat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvh4dimat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		dvh3dimat.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
4		dvh3dimat.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
5		dvh3dimat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		dvh3dimat.p	$$⊢\phi \to P\in A$$
7		dvh3dimat.q	$$⊢\phi \to Q\in A$$
8	1 2 3 4 5 6 6 7	dvh4dimat	$$⊢\phi \to \exists s\in A\neg s\subseteq \left(P\underset{\dot{}}{\oplus }P\right)\underset{\dot{}}{\oplus }Q$$
9	1 2 5	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
10		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
11	10 4 9 6	lsatlssel	$$⊢\phi \to P\in \mathrm{LSubSp}\left(U\right)$$
12	10	lsssubg	$$⊢\left(U\in \mathrm{LMod}\wedge P\in \mathrm{LSubSp}\left(U\right)\right)\to P\in \mathrm{SubGrp}\left(U\right)$$
13	9 11 12	syl2anc	$$⊢\phi \to P\in \mathrm{SubGrp}\left(U\right)$$
14	3	lsmidm	$$⊢P\in \mathrm{SubGrp}\left(U\right)\to P\underset{\dot{}}{\oplus }P=P$$
15	13 14	syl	$$⊢\phi \to P\underset{\dot{}}{\oplus }P=P$$
16	15	oveq1d	$$⊢\phi \to \left(P\underset{\dot{}}{\oplus }P\right)\underset{\dot{}}{\oplus }Q=P\underset{\dot{}}{\oplus }Q$$
17	16	sseq2d	$$⊢\phi \to \left(s\subseteq \left(P\underset{\dot{}}{\oplus }P\right)\underset{\dot{}}{\oplus }Q\leftrightarrow s\subseteq P\underset{\dot{}}{\oplus }Q\right)$$
18	17	notbid	$$⊢\phi \to \left(\neg s\subseteq \left(P\underset{\dot{}}{\oplus }P\right)\underset{\dot{}}{\oplus }Q\leftrightarrow \neg s\subseteq P\underset{\dot{}}{\oplus }Q\right)$$
19	18	rexbidv	$$⊢\phi \to \left(\exists s\in A\neg s\subseteq \left(P\underset{\dot{}}{\oplus }P\right)\underset{\dot{}}{\oplus }Q\leftrightarrow \exists s\in A\neg s\subseteq P\underset{\dot{}}{\oplus }Q\right)$$
20	8 19	mpbid	$$⊢\phi \to \exists s\in A\neg s\subseteq P\underset{\dot{}}{\oplus }Q$$