Theorem lsatcv0eq

Description: If the sum of two atoms cover the zero subspace, they are equal. ( atcv0eq analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsatcv0eq.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatcv0eq.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lsatcv0eq.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatcv0eq.c	$$⊢C={⋖}_L\left(W\right)$$
	lsatcv0eq.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatcv0eq.q	$$⊢\phi \to Q\in A$$
	lsatcv0eq.r	$$⊢\phi \to R\in A$$
Assertion	lsatcv0eq	$$⊢\phi \to \left(\left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\leftrightarrow Q=R\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsatcv0eq.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsatcv0eq.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
3		lsatcv0eq.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
4		lsatcv0eq.c	$$⊢C={⋖}_L\left(W\right)$$
5		lsatcv0eq.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lsatcv0eq.q	$$⊢\phi \to Q\in A$$
7		lsatcv0eq.r	$$⊢\phi \to R\in A$$
8	1 3 5 6 7	lsatnem0	$$⊢\phi \to \left(Q\ne R\leftrightarrow Q\cap R=\left\{\underset{\dot{}}{0}\right\}\right)$$
9		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
10		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
11	5 10	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
12	9 3 11 6	lsatlssel	$$⊢\phi \to Q\in \mathrm{LSubSp}\left(W\right)$$
13	9 2 1 3 4 5 12 7	lcvp	$$⊢\phi \to \left(Q\cap R=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)$$
14	1 3 4 5 6	lsatcv0	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}CQ$$
15	14	biantrurd	$$⊢\phi \to \left(QC\left(Q\underset{\dot{}}{\oplus }R\right)\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)$$
16	8 13 15	3bitrd	$$⊢\phi \to \left(Q\ne R\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)$$
17	5	adantr	$$⊢\left(\phi \wedge \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)\to W\in \mathrm{LVec}$$
18	1 9	lsssn0	$$⊢W\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(W\right)$$
19	11 18	syl	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(W\right)$$
20	19	adantr	$$⊢\left(\phi \wedge \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(W\right)$$
21	12	adantr	$$⊢\left(\phi \wedge \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)\to Q\in \mathrm{LSubSp}\left(W\right)$$
22	9 3 11 7	lsatlssel	$$⊢\phi \to R\in \mathrm{LSubSp}\left(W\right)$$
23	9 2	lsmcl	$$⊢\left(W\in \mathrm{LMod}\wedge Q\in \mathrm{LSubSp}\left(W\right)\wedge R\in \mathrm{LSubSp}\left(W\right)\right)\to Q\underset{\dot{}}{\oplus }R\in \mathrm{LSubSp}\left(W\right)$$
24	11 12 22 23	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\oplus }R\in \mathrm{LSubSp}\left(W\right)$$
25	24	adantr	$$⊢\left(\phi \wedge \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)\to Q\underset{\dot{}}{\oplus }R\in \mathrm{LSubSp}\left(W\right)$$
26		simprl	$$⊢\left(\phi \wedge \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)\to \left\{\underset{\dot{}}{0}\right\}CQ$$
27		simprr	$$⊢\left(\phi \wedge \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)\to QC\left(Q\underset{\dot{}}{\oplus }R\right)$$
28	9 4 17 20 21 25 26 27	lcvntr	$$⊢\left(\phi \wedge \left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\right)\to \neg \left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)$$
29	28	ex	$$⊢\phi \to \left(\left(\left\{\underset{\dot{}}{0}\right\}CQ\wedge QC\left(Q\underset{\dot{}}{\oplus }R\right)\right)\to \neg \left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\right)$$
30	16 29	sylbid	$$⊢\phi \to \left(Q\ne R\to \neg \left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\right)$$
31	30	necon4ad	$$⊢\phi \to \left(\left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\to Q=R\right)$$
32	9	lsssssubg	$$⊢W\in \mathrm{LMod}\to \mathrm{LSubSp}\left(W\right)\subseteq \mathrm{SubGrp}\left(W\right)$$
33	11 32	syl	$$⊢\phi \to \mathrm{LSubSp}\left(W\right)\subseteq \mathrm{SubGrp}\left(W\right)$$
34	33 12	sseldd	$$⊢\phi \to Q\in \mathrm{SubGrp}\left(W\right)$$
35	2	lsmidm	$$⊢Q\in \mathrm{SubGrp}\left(W\right)\to Q\underset{\dot{}}{\oplus }Q=Q$$
36	34 35	syl	$$⊢\phi \to Q\underset{\dot{}}{\oplus }Q=Q$$
37	14 36	breqtrrd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }Q\right)$$
38		oveq2	$$⊢Q=R\to Q\underset{\dot{}}{\oplus }Q=Q\underset{\dot{}}{\oplus }R$$
39	38	breq2d	$$⊢Q=R\to \left(\left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }Q\right)\leftrightarrow \left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\right)$$
40	37 39	syl5ibcom	$$⊢\phi \to \left(Q=R\to \left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\right)$$
41	31 40	impbid	$$⊢\phi \to \left(\left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\leftrightarrow Q=R\right)$$