lsatcv1

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

	Ref	Expression
Hypotheses	lsatcv1.o	$⊢ \underset{˙}{0} = 0_{W}$
	lsatcv1.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsatcv1.s	$⊢ S = LSubSp (W)$
	lsatcv1.a	$⊢ A = LSAtoms (W)$
	lsatcv1.c	$⊢ C = ⋖_{L} (W)$
	lsatcv1.w	$⊢ φ \to W \in LVec$
	lsatcv1.u	$⊢ φ \to U \in S$
	lsatcv1.q	$⊢ φ \to Q \in A$
	lsatcv1.r	$⊢ φ \to R \in A$
	lsatcv1.l	$⊢ φ \to U C (Q \underset{˙}{\oplus} R)$
Assertion	lsatcv1	$⊢ φ \to (U = \{\underset{˙}{0}\} \leftrightarrow Q = R)$

Proof

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

Metamath Proof Explorer

Theorem lsatcv1

Proof