Metamath Proof Explorer


Theorem 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 ˙ = LSSum W
lcvat.a A = LSAtoms W
icvat.c C = L W
lcvat.w φ W LMod
lcvat.t φ T S
lcvat.u φ U S
lcvat.l φ T C U
Assertion lcvat φ q A T ˙ q = U

Proof

Step Hyp Ref Expression
1 lcvat.s S = LSubSp W
2 lcvat.p ˙ = LSSum W
3 lcvat.a A = LSAtoms W
4 icvat.c C = L W
5 lcvat.w φ W LMod
6 lcvat.t φ T S
7 lcvat.u φ U S
8 lcvat.l φ T C U
9 1 4 5 6 7 8 lcvpss φ T U
10 1 2 3 5 6 7 9 lrelat φ q A T T ˙ q T ˙ q U
11 5 3ad2ant1 φ q A T T ˙ q T ˙ q U W LMod
12 6 3ad2ant1 φ q A T T ˙ q T ˙ q U T S
13 7 3ad2ant1 φ q A T T ˙ q T ˙ q U U S
14 simp2 φ q A T T ˙ q T ˙ q U q A
15 1 3 11 14 lsatlssel φ q A T T ˙ q T ˙ q U q S
16 1 2 lsmcl W LMod T S q S T ˙ q S
17 11 12 15 16 syl3anc φ q A T T ˙ q T ˙ q U T ˙ q S
18 8 3ad2ant1 φ q A T T ˙ q T ˙ q U T C U
19 simp3l φ q A T T ˙ q T ˙ q U T T ˙ q
20 simp3r φ q A T T ˙ q T ˙ q U T ˙ q U
21 1 4 11 12 13 17 18 19 20 lcvnbtwn2 φ q A T T ˙ q T ˙ q U T ˙ q = U
22 21 3exp φ q A T T ˙ q T ˙ q U T ˙ q = U
23 22 reximdvai φ q A T T ˙ q T ˙ q U q A T ˙ q = U
24 10 23 mpd φ q A T ˙ q = U