This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐴 ( 𝑇 ⊕ 𝑞 ) = 𝑈 )