Theorem lsatcv1

Description: Two atoms covering the zero subspace are equal. ( atcv1 analog.) (Contributed by NM, 10-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lsatcv1.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsatcv1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
3		lsatcv1.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
4		lsatcv1.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		lsatcv1.c	$$⊢C={⋖}_L\left(W\right)$$
6		lsatcv1.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		lsatcv1.u	$$⊢\phi \to U\in S$$
8		lsatcv1.q	$$⊢\phi \to Q\in A$$
9		lsatcv1.r	$$⊢\phi \to R\in A$$
10		lsatcv1.l	$$⊢\phi \to UC\left(Q\underset{\dot{}}{\oplus }R\right)$$
11		breq1	$$⊢U=\left\{\underset{\dot{}}{0}\right\}\to \left(UC\left(Q\underset{\dot{}}{\oplus }R\right)\leftrightarrow \left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\right)$$
12	10 11	syl5ibcom	$$⊢\phi \to \left(U=\left\{\underset{\dot{}}{0}\right\}\to \left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\right)$$
13	1 2 4 5 6 8 9	lsatcv0eq	$$⊢\phi \to \left(\left\{\underset{\dot{}}{0}\right\}C\left(Q\underset{\dot{}}{\oplus }R\right)\leftrightarrow Q=R\right)$$
14	12 13	sylibd	$$⊢\phi \to \left(U=\left\{\underset{\dot{}}{0}\right\}\to Q=R\right)$$
15	10	adantr	$$⊢\left(\phi \wedge Q=R\right)\to UC\left(Q\underset{\dot{}}{\oplus }R\right)$$
16	6	adantr	$$⊢\left(\phi \wedge Q=R\right)\to W\in \mathrm{LVec}$$
17	7	adantr	$$⊢\left(\phi \wedge Q=R\right)\to U\in S$$
18		oveq1	$$⊢Q=R\to Q\underset{\dot{}}{\oplus }R=R\underset{\dot{}}{\oplus }R$$
19		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
20	6 19	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
21	3 4 20 9	lsatlssel	$$⊢\phi \to R\in S$$
22	3	lsssubg	$$⊢\left(W\in \mathrm{LMod}\wedge R\in S\right)\to R\in \mathrm{SubGrp}\left(W\right)$$
23	20 21 22	syl2anc	$$⊢\phi \to R\in \mathrm{SubGrp}\left(W\right)$$
24	2	lsmidm	$$⊢R\in \mathrm{SubGrp}\left(W\right)\to R\underset{\dot{}}{\oplus }R=R$$
25	23 24	syl	$$⊢\phi \to R\underset{\dot{}}{\oplus }R=R$$
26	18 25	sylan9eqr	$$⊢\left(\phi \wedge Q=R\right)\to Q\underset{\dot{}}{\oplus }R=R$$
27	9	adantr	$$⊢\left(\phi \wedge Q=R\right)\to R\in A$$
28	26 27	eqeltrd	$$⊢\left(\phi \wedge Q=R\right)\to Q\underset{\dot{}}{\oplus }R\in A$$
29	1 3 4 5 16 17 28	lsatcveq0	$$⊢\left(\phi \wedge Q=R\right)\to \left(UC\left(Q\underset{\dot{}}{\oplus }R\right)\leftrightarrow U=\left\{\underset{\dot{}}{0}\right\}\right)$$
30	15 29	mpbid	$$⊢\left(\phi \wedge Q=R\right)\to U=\left\{\underset{\dot{}}{0}\right\}$$
31	30	ex	$$⊢\phi \to \left(Q=R\to U=\left\{\underset{\dot{}}{0}\right\}\right)$$
32	14 31	impbid	$$⊢\phi \to \left(U=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow Q=R\right)$$