lsatcvat

Description: A nonzero subspace less than the sum of two atoms is an atom. ( atcvati analog.) (Contributed by NM, 10-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lsatcvat.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lsatcvat.s	$⊢ S = LSubSp (W)$
3		lsatcvat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		lsatcvat.a	$⊢ A = LSAtoms (W)$
5		lsatcvat.w	$⊢ φ \to W \in LVec$
6		lsatcvat.u	$⊢ φ \to U \in S$
7		lsatcvat.q	$⊢ φ \to Q \in A$
8		lsatcvat.r	$⊢ φ \to R \in A$
9		lsatcvat.n	$⊢ φ \to U \neq \{\underset{˙}{0}\}$
10		lsatcvat.l	$⊢ φ \to U \subset Q \underset{˙}{\oplus} R$
11	5	adantr	$⊢ (φ \land \neg Q \subseteq U) \to W \in LVec$
12	6	adantr	$⊢ (φ \land \neg Q \subseteq U) \to U \in S$
13	7	adantr	$⊢ (φ \land \neg Q \subseteq U) \to Q \in A$
14	8	adantr	$⊢ (φ \land \neg Q \subseteq U) \to R \in A$
15	9	adantr	$⊢ (φ \land \neg Q \subseteq U) \to U \neq \{\underset{˙}{0}\}$
16	10	adantr	$⊢ (φ \land \neg Q \subseteq U) \to U \subset Q \underset{˙}{\oplus} R$
17		simpr	$⊢ (φ \land \neg Q \subseteq U) \to \neg Q \subseteq U$
18	1 2 3 4 11 12 13 14 15 16 17	lsatcvatlem	$⊢ (φ \land \neg Q \subseteq U) \to U \in A$
19	5	adantr	$⊢ (φ \land \neg R \subseteq U) \to W \in LVec$
20	6	adantr	$⊢ (φ \land \neg R \subseteq U) \to U \in S$
21	8	adantr	$⊢ (φ \land \neg R \subseteq U) \to R \in A$
22	7	adantr	$⊢ (φ \land \neg R \subseteq U) \to Q \in A$
23	9	adantr	$⊢ (φ \land \neg R \subseteq U) \to U \neq \{\underset{˙}{0}\}$
24		lveclmod	$⊢ W \in LVec \to W \in LMod$
25	5 24	syl	$⊢ φ \to W \in LMod$
26		lmodabl	$⊢ W \in LMod \to W \in Abel$
27	25 26	syl	$⊢ φ \to W \in Abel$
28	2	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
29	25 28	syl	$⊢ φ \to S \subseteq SubGrp (W)$
30	2 4 25 7	lsatlssel	$⊢ φ \to Q \in S$
31	29 30	sseldd	$⊢ φ \to Q \in SubGrp (W)$
32	2 4 25 8	lsatlssel	$⊢ φ \to R \in S$
33	29 32	sseldd	$⊢ φ \to R \in SubGrp (W)$
34	3	lsmcom	$⊢ (W \in Abel \land Q \in SubGrp (W) \land R \in SubGrp (W)) \to Q \underset{˙}{\oplus} R = R \underset{˙}{\oplus} Q$
35	27 31 33 34	syl3anc	$⊢ φ \to Q \underset{˙}{\oplus} R = R \underset{˙}{\oplus} Q$
36	35	psseq2d	$⊢ φ \to (U \subset Q \underset{˙}{\oplus} R \leftrightarrow U \subset R \underset{˙}{\oplus} Q)$
37	10 36	mpbid	$⊢ φ \to U \subset R \underset{˙}{\oplus} Q$
38	37	adantr	$⊢ (φ \land \neg R \subseteq U) \to U \subset R \underset{˙}{\oplus} Q$
39		simpr	$⊢ (φ \land \neg R \subseteq U) \to \neg R \subseteq U$
40	1 2 3 4 19 20 21 22 23 38 39	lsatcvatlem	$⊢ (φ \land \neg R \subseteq U) \to U \in A$
41	29 6	sseldd	$⊢ φ \to U \in SubGrp (W)$
42	3	lsmlub	$⊢ (Q \in SubGrp (W) \land R \in SubGrp (W) \land U \in SubGrp (W)) \to ((Q \subseteq U \land R \subseteq U) \leftrightarrow Q \underset{˙}{\oplus} R \subseteq U)$
43	31 33 41 42	syl3anc	$⊢ φ \to ((Q \subseteq U \land R \subseteq U) \leftrightarrow Q \underset{˙}{\oplus} R \subseteq U)$
44		ssnpss	$⊢ Q \underset{˙}{\oplus} R \subseteq U \to \neg U \subset Q \underset{˙}{\oplus} R$
45	43 44	syl6bi	$⊢ φ \to ((Q \subseteq U \land R \subseteq U) \to \neg U \subset Q \underset{˙}{\oplus} R)$
46	45	con2d	$⊢ φ \to (U \subset Q \underset{˙}{\oplus} R \to \neg (Q \subseteq U \land R \subseteq U))$
47		ianor	$⊢ \neg (Q \subseteq U \land R \subseteq U) \leftrightarrow (\neg Q \subseteq U \lor \neg R \subseteq U)$
48	46 47	imbitrdi	$⊢ φ \to (U \subset Q \underset{˙}{\oplus} R \to (\neg Q \subseteq U \lor \neg R \subseteq U))$
49	10 48	mpd	$⊢ φ \to (\neg Q \subseteq U \lor \neg R \subseteq U)$
50	18 40 49	mpjaodan	$⊢ φ \to U \in A$

Metamath Proof Explorer

Theorem lsatcvat

Proof