lsatcvatlem

	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$
	lsatcvat.m	$⊢ φ \to \neg Q \subseteq U$
Assertion	lsatcvatlem	$⊢ φ \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		lsatcvat.m	$⊢ φ \to \neg Q \subseteq U$
12		lveclmod	$⊢ W \in LVec \to W \in LMod$
13	5 12	syl	$⊢ φ \to W \in LMod$
14	2 1 4 13 6 9	lssatomic	$⊢ φ \to \exists x \in A x \subseteq U$
15		eqid	$⊢ ⋖_{L} (W) = ⋖_{L} (W)$
16	5	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to W \in LVec$
17	13	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to W \in LMod$
18		simp2	$⊢ (φ \land x \in A \land x \subseteq U) \to x \in A$
19	2 4 17 18	lsatlssel	$⊢ (φ \land x \in A \land x \subseteq U) \to x \in S$
20	2 4 13 7	lsatlssel	$⊢ φ \to Q \in S$
21	20	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to Q \in S$
22	2 3	lsmcl	$⊢ (W \in LMod \land Q \in S \land x \in S) \to Q \underset{˙}{\oplus} x \in S$
23	17 21 19 22	syl3anc	$⊢ (φ \land x \in A \land x \subseteq U) \to Q \underset{˙}{\oplus} x \in S$
24	6	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to U \in S$
25	11	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to \neg Q \subseteq U$
26		sseq1	$⊢ x = Q \to (x \subseteq U \leftrightarrow Q \subseteq U)$
27	26	biimpcd	$⊢ x \subseteq U \to (x = Q \to Q \subseteq U)$
28	27	necon3bd	$⊢ x \subseteq U \to (\neg Q \subseteq U \to x \neq Q)$
29	28	3ad2ant3	$⊢ (φ \land x \in A \land x \subseteq U) \to (\neg Q \subseteq U \to x \neq Q)$
30	25 29	mpd	$⊢ (φ \land x \in A \land x \subseteq U) \to x \neq Q$
31	7	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to Q \in A$
32	1 4 16 18 31	lsatnem0	$⊢ (φ \land x \in A \land x \subseteq U) \to (x \neq Q \leftrightarrow x \cap Q = \{\underset{˙}{0}\})$
33	30 32	mpbid	$⊢ (φ \land x \in A \land x \subseteq U) \to x \cap Q = \{\underset{˙}{0}\}$
34	2 3 1 4 15 16 19 31	lcvp	$⊢ (φ \land x \in A \land x \subseteq U) \to (x \cap Q = \{\underset{˙}{0}\} \leftrightarrow x ⋖_{L} (W) (x \underset{˙}{\oplus} Q))$
35	33 34	mpbid	$⊢ (φ \land x \in A \land x \subseteq U) \to x ⋖_{L} (W) (x \underset{˙}{\oplus} Q)$
36		lmodabl	$⊢ W \in LMod \to W \in Abel$
37	17 36	syl	$⊢ (φ \land x \in A \land x \subseteq U) \to W \in Abel$
38	2	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
39	17 38	syl	$⊢ (φ \land x \in A \land x \subseteq U) \to S \subseteq SubGrp (W)$
40	39 19	sseldd	$⊢ (φ \land x \in A \land x \subseteq U) \to x \in SubGrp (W)$
41	39 21	sseldd	$⊢ (φ \land x \in A \land x \subseteq U) \to Q \in SubGrp (W)$
42	3	lsmcom	$⊢ (W \in Abel \land x \in SubGrp (W) \land Q \in SubGrp (W)) \to x \underset{˙}{\oplus} Q = Q \underset{˙}{\oplus} x$
43	37 40 41 42	syl3anc	$⊢ (φ \land x \in A \land x \subseteq U) \to x \underset{˙}{\oplus} Q = Q \underset{˙}{\oplus} x$
44	35 43	breqtrd	$⊢ (φ \land x \in A \land x \subseteq U) \to x ⋖_{L} (W) (Q \underset{˙}{\oplus} x)$
45		simp3	$⊢ (φ \land x \in A \land x \subseteq U) \to x \subseteq U$
46	10	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to U \subset Q \underset{˙}{\oplus} R$
47	3	lsmub1	$⊢ (Q \in SubGrp (W) \land x \in SubGrp (W)) \to Q \subseteq Q \underset{˙}{\oplus} x$
48	41 40 47	syl2anc	$⊢ (φ \land x \in A \land x \subseteq U) \to Q \subseteq Q \underset{˙}{\oplus} x$
49	8	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to R \in A$
50	10	pssssd	$⊢ φ \to U \subseteq Q \underset{˙}{\oplus} R$
51	50	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to U \subseteq Q \underset{˙}{\oplus} R$
52	45 51	sstrd	$⊢ (φ \land x \in A \land x \subseteq U) \to x \subseteq Q \underset{˙}{\oplus} R$
53	3 4 16 18 49 31 52 30	lsatexch1	$⊢ (φ \land x \in A \land x \subseteq U) \to R \subseteq Q \underset{˙}{\oplus} x$
54	2 4 13 8	lsatlssel	$⊢ φ \to R \in S$
55	54	3ad2ant1	$⊢ (φ \land x \in A \land x \subseteq U) \to R \in S$
56	39 55	sseldd	$⊢ (φ \land x \in A \land x \subseteq U) \to R \in SubGrp (W)$
57	39 23	sseldd	$⊢ (φ \land x \in A \land x \subseteq U) \to Q \underset{˙}{\oplus} x \in SubGrp (W)$
58	3	lsmlub	$⊢ (Q \in SubGrp (W) \land R \in SubGrp (W) \land Q \underset{˙}{\oplus} x \in SubGrp (W)) \to ((Q \subseteq Q \underset{˙}{\oplus} x \land R \subseteq Q \underset{˙}{\oplus} x) \leftrightarrow Q \underset{˙}{\oplus} R \subseteq Q \underset{˙}{\oplus} x)$
59	41 56 57 58	syl3anc	$⊢ (φ \land x \in A \land x \subseteq U) \to ((Q \subseteq Q \underset{˙}{\oplus} x \land R \subseteq Q \underset{˙}{\oplus} x) \leftrightarrow Q \underset{˙}{\oplus} R \subseteq Q \underset{˙}{\oplus} x)$
60	48 53 59	mpbi2and	$⊢ (φ \land x \in A \land x \subseteq U) \to Q \underset{˙}{\oplus} R \subseteq Q \underset{˙}{\oplus} x$
61	46 60	psssstrd	$⊢ (φ \land x \in A \land x \subseteq U) \to U \subset Q \underset{˙}{\oplus} x$
62	2 15 16 19 23 24 44 45 61	lcvnbtwn3	$⊢ (φ \land x \in A \land x \subseteq U) \to U = x$
63	62 18	eqeltrd	$⊢ (φ \land x \in A \land x \subseteq U) \to U \in A$
64	63	rexlimdv3a	$⊢ φ \to (\exists x \in A x \subseteq U \to U \in A)$
65	14 64	mpd	$⊢ φ \to U \in A$

Metamath Proof Explorer

Theorem lsatcvatlem

Proof