lcvat

Description: If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. ( cvati analog.) (Contributed by NM, 11-Jan-2015)

	Ref	Expression
Hypotheses	lcvat.s	$⊢ S = LSubSp (W)$
	lcvat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lcvat.a	$⊢ A = LSAtoms (W)$
	icvat.c	$⊢ C = ⋖_{L} (W)$
	lcvat.w	$⊢ φ \to W \in LMod$
	lcvat.t	$⊢ φ \to T \in S$
	lcvat.u	$⊢ φ \to U \in S$
	lcvat.l	$⊢ φ \to T C U$
Assertion	lcvat	$⊢ φ \to \exists q \in A T \underset{˙}{\oplus} q = U$

Proof

Step	Hyp	Ref	Expression
1		lcvat.s	$⊢ S = LSubSp (W)$
2		lcvat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lcvat.a	$⊢ A = LSAtoms (W)$
4		icvat.c	$⊢ C = ⋖_{L} (W)$
5		lcvat.w	$⊢ φ \to W \in LMod$
6		lcvat.t	$⊢ φ \to T \in S$
7		lcvat.u	$⊢ φ \to U \in S$
8		lcvat.l	$⊢ φ \to T C U$
9	1 4 5 6 7 8	lcvpss	$⊢ φ \to T \subset U$
10	1 2 3 5 6 7 9	lrelat	$⊢ φ \to \exists q \in A (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)$
11	5	3ad2ant1	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to W \in LMod$
12	6	3ad2ant1	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to T \in S$
13	7	3ad2ant1	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to U \in S$
14		simp2	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to q \in A$
15	1 3 11 14	lsatlssel	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to q \in S$
16	1 2	lsmcl	$⊢ (W \in LMod \land T \in S \land q \in S) \to T \underset{˙}{\oplus} q \in S$
17	11 12 15 16	syl3anc	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to T \underset{˙}{\oplus} q \in S$
18	8	3ad2ant1	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to T C U$
19		simp3l	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to T \subset T \underset{˙}{\oplus} q$
20		simp3r	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to T \underset{˙}{\oplus} q \subseteq U$
21	1 4 11 12 13 17 18 19 20	lcvnbtwn2	$⊢ (φ \land q \in A \land (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)) \to T \underset{˙}{\oplus} q = U$
22	21	3exp	$⊢ φ \to (q \in A \to ((T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U) \to T \underset{˙}{\oplus} q = U))$
23	22	reximdvai	$⊢ φ \to (\exists q \in A (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U) \to \exists q \in A T \underset{˙}{\oplus} q = U)$
24	10 23	mpd	$⊢ φ \to \exists q \in A T \underset{˙}{\oplus} q = U$

Metamath Proof Explorer

Theorem lcvat

Proof