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 𝑆 = ( LSubSp ‘ 𝑊 )
lcvat.p = ( LSSum ‘ 𝑊 )
lcvat.a 𝐴 = ( LSAtoms ‘ 𝑊 )
icvat.c 𝐶 = ( ⋖L𝑊 )
lcvat.w ( 𝜑𝑊 ∈ LMod )
lcvat.t ( 𝜑𝑇𝑆 )
lcvat.u ( 𝜑𝑈𝑆 )
lcvat.l ( 𝜑𝑇 𝐶 𝑈 )
Assertion lcvat ( 𝜑 → ∃ 𝑞𝐴 ( 𝑇 𝑞 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 lcvat.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvat.p = ( LSSum ‘ 𝑊 )
3 lcvat.a 𝐴 = ( LSAtoms ‘ 𝑊 )
4 icvat.c 𝐶 = ( ⋖L𝑊 )
5 lcvat.w ( 𝜑𝑊 ∈ LMod )
6 lcvat.t ( 𝜑𝑇𝑆 )
7 lcvat.u ( 𝜑𝑈𝑆 )
8 lcvat.l ( 𝜑𝑇 𝐶 𝑈 )
9 1 4 5 6 7 8 lcvpss ( 𝜑𝑇𝑈 )
10 1 2 3 5 6 7 9 lrelat ( 𝜑 → ∃ 𝑞𝐴 ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) )
11 5 3ad2ant1 ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → 𝑊 ∈ LMod )
12 6 3ad2ant1 ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → 𝑇𝑆 )
13 7 3ad2ant1 ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → 𝑈𝑆 )
14 simp2 ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → 𝑞𝐴 )
15 1 3 11 14 lsatlssel ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → 𝑞𝑆 )
16 1 2 lsmcl ( ( 𝑊 ∈ LMod ∧ 𝑇𝑆𝑞𝑆 ) → ( 𝑇 𝑞 ) ∈ 𝑆 )
17 11 12 15 16 syl3anc ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → ( 𝑇 𝑞 ) ∈ 𝑆 )
18 8 3ad2ant1 ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → 𝑇 𝐶 𝑈 )
19 simp3l ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → 𝑇 ⊊ ( 𝑇 𝑞 ) )
20 simp3r ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → ( 𝑇 𝑞 ) ⊆ 𝑈 )
21 1 4 11 12 13 17 18 19 20 lcvnbtwn2 ( ( 𝜑𝑞𝐴 ∧ ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) ) → ( 𝑇 𝑞 ) = 𝑈 )
22 21 3exp ( 𝜑 → ( 𝑞𝐴 → ( ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) → ( 𝑇 𝑞 ) = 𝑈 ) ) )
23 22 reximdvai ( 𝜑 → ( ∃ 𝑞𝐴 ( 𝑇 ⊊ ( 𝑇 𝑞 ) ∧ ( 𝑇 𝑞 ) ⊆ 𝑈 ) → ∃ 𝑞𝐴 ( 𝑇 𝑞 ) = 𝑈 ) )
24 10 23 mpd ( 𝜑 → ∃ 𝑞𝐴 ( 𝑇 𝑞 ) = 𝑈 )