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

Metamath Proof Explorer

Theorem lsppratlem2

Description: Lemma for lspprat . Show that if X and Y are both in ( N{ x , y } ) (which will be our goal for each of the two cases above), then ( N{ X , Y } ) C_ U , contradicting the hypothesis for U . (Contributed by NM, 29-Aug-2014) (Revised by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses lspprat.v ⊢ V = Base W
lspprat.s ⊢ S = LSubSp ⁡ W
lspprat.n ⊢ N = LSpan ⁡ W
lspprat.w ⊢ φ → W ∈ LVec
lspprat.u ⊢ φ → U ∈ S
lspprat.x ⊢ φ → X ∈ V
lspprat.y ⊢ φ → Y ∈ V
lspprat.p ⊢ φ → U ⊂ N ⁡ X Y
lsppratlem1.o ⊢ 0 ˙ = 0 W
lsppratlem1.x2 ⊢ φ → x ∈ U ∖ 0 ˙
lsppratlem1.y2 ⊢ φ → y ∈ U ∖ N ⁡ x
lsppratlem2.x1 ⊢ φ → X ∈ N ⁡ x y
lsppratlem2.y1 ⊢ φ → Y ∈ N ⁡ x y
Assertion lsppratlem2 ⊢ φ → N ⁡ X Y ⊆ U

Proof

Step Hyp Ref Expression
1 lspprat.v ⊢ V = Base W
2 lspprat.s ⊢ S = LSubSp ⁡ W
3 lspprat.n ⊢ N = LSpan ⁡ W
4 lspprat.w ⊢ φ → W ∈ LVec
5 lspprat.u ⊢ φ → U ∈ S
6 lspprat.x ⊢ φ → X ∈ V
7 lspprat.y ⊢ φ → Y ∈ V
8 lspprat.p ⊢ φ → U ⊂ N ⁡ X Y
9 lsppratlem1.o ⊢ 0 ˙ = 0 W
10 lsppratlem1.x2 ⊢ φ → x ∈ U ∖ 0 ˙
11 lsppratlem1.y2 ⊢ φ → y ∈ U ∖ N ⁡ x
12 lsppratlem2.x1 ⊢ φ → X ∈ N ⁡ x y
13 lsppratlem2.y1 ⊢ φ → Y ∈ N ⁡ x y
14 lveclmod ⊢ W ∈ LVec → W ∈ LMod
15 4 14 syl ⊢ φ → W ∈ LMod
16 10 eldifad ⊢ φ → x ∈ U
17 11 eldifad ⊢ φ → y ∈ U
18 16 17 prssd ⊢ φ → x y ⊆ U
19 1 2 lssss ⊢ U ∈ S → U ⊆ V
20 5 19 syl ⊢ φ → U ⊆ V
21 18 20 sstrd ⊢ φ → x y ⊆ V
22 1 2 3 lspcl ⊢ W ∈ LMod ∧ x y ⊆ V → N ⁡ x y ∈ S
23 15 21 22 syl2anc ⊢ φ → N ⁡ x y ∈ S
24 2 3 15 23 12 13 lspprss ⊢ φ → N ⁡ X Y ⊆ N ⁡ x y
25 2 3 15 5 16 17 lspprss ⊢ φ → N ⁡ x y ⊆ U
26 24 25 sstrd ⊢ φ → N ⁡ X Y ⊆ U