Metamath Proof Explorer


Theorem lsppratlem5

Description: Lemma for lspprat . Combine the two cases and show a contradiction to U C. ( N{ X , Y } ) under the assumptions on x and y . (Contributed by NM, 29-Aug-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
Assertion lsppratlem5 φ 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 4 adantr φ x N Y W LVec
13 5 adantr φ x N Y U S
14 6 adantr φ x N Y X V
15 7 adantr φ x N Y Y V
16 8 adantr φ x N Y U N X Y
17 10 adantr φ x N Y x U 0 ˙
18 11 adantr φ x N Y y U N x
19 simpr φ x N Y x N Y
20 1 2 3 12 13 14 15 16 9 17 18 19 lsppratlem3 φ x N Y X N x y Y N x y
21 4 adantr φ X N x Y W LVec
22 5 adantr φ X N x Y U S
23 6 adantr φ X N x Y X V
24 7 adantr φ X N x Y Y V
25 8 adantr φ X N x Y U N X Y
26 10 adantr φ X N x Y x U 0 ˙
27 11 adantr φ X N x Y y U N x
28 simpr φ X N x Y X N x Y
29 1 2 3 21 22 23 24 25 9 26 27 28 lsppratlem4 φ X N x Y X N x y Y N x y
30 1 2 3 4 5 6 7 8 9 10 11 lsppratlem1 φ x N Y X N x Y
31 20 29 30 mpjaodan φ X N x y Y N x y
32 4 adantr φ X N x y Y N x y W LVec
33 5 adantr φ X N x y Y N x y U S
34 6 adantr φ X N x y Y N x y X V
35 7 adantr φ X N x y Y N x y Y V
36 8 adantr φ X N x y Y N x y U N X Y
37 10 adantr φ X N x y Y N x y x U 0 ˙
38 11 adantr φ X N x y Y N x y y U N x
39 simprl φ X N x y Y N x y X N x y
40 simprr φ X N x y Y N x y Y N x y
41 1 2 3 32 33 34 35 36 9 37 38 39 40 lsppratlem2 φ X N x y Y N x y N X Y U
42 31 41 mpdan φ N X Y U