Metamath Proof Explorer


Theorem lshpnel2N

Description: Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lshpnel2.v V = Base W
lshpnel2.s S = LSubSp W
lshpnel2.n N = LSpan W
lshpnel2.p ˙ = LSSum W
lshpnel2.h H = LSHyp W
lshpnel2.w φ W LVec
lshpnel2.u φ U S
lshpnel2.t φ U V
lshpnel2.x φ X V
lshpnel2.e φ ¬ X U
Assertion lshpnel2N φ U H U ˙ N X = V

Proof

Step Hyp Ref Expression
1 lshpnel2.v V = Base W
2 lshpnel2.s S = LSubSp W
3 lshpnel2.n N = LSpan W
4 lshpnel2.p ˙ = LSSum W
5 lshpnel2.h H = LSHyp W
6 lshpnel2.w φ W LVec
7 lshpnel2.u φ U S
8 lshpnel2.t φ U V
9 lshpnel2.x φ X V
10 lshpnel2.e φ ¬ X U
11 10 adantr φ U H ¬ X U
12 6 adantr φ U H W LVec
13 simpr φ U H U H
14 9 adantr φ U H X V
15 1 3 4 5 12 13 14 lshpnelb φ U H ¬ X U U ˙ N X = V
16 11 15 mpbid φ U H U ˙ N X = V
17 7 adantr φ U ˙ N X = V U S
18 8 adantr φ U ˙ N X = V U V
19 9 adantr φ U ˙ N X = V X V
20 lveclmod W LVec W LMod
21 6 20 syl φ W LMod
22 2 3 lspid W LMod U S N U = U
23 21 7 22 syl2anc φ N U = U
24 23 uneq1d φ N U N X = U N X
25 24 fveq2d φ N N U N X = N U N X
26 1 2 lssss U S U V
27 7 26 syl φ U V
28 9 snssd φ X V
29 1 3 lspun W LMod U V X V N U X = N N U N X
30 21 27 28 29 syl3anc φ N U X = N N U N X
31 1 2 3 lspsncl W LMod X V N X S
32 21 9 31 syl2anc φ N X S
33 2 3 4 lsmsp W LMod U S N X S U ˙ N X = N U N X
34 21 7 32 33 syl3anc φ U ˙ N X = N U N X
35 25 30 34 3eqtr4rd φ U ˙ N X = N U X
36 35 eqeq1d φ U ˙ N X = V N U X = V
37 36 biimpa φ U ˙ N X = V N U X = V
38 sneq v = X v = X
39 38 uneq2d v = X U v = U X
40 39 fveqeq2d v = X N U v = V N U X = V
41 40 rspcev X V N U X = V v V N U v = V
42 19 37 41 syl2anc φ U ˙ N X = V v V N U v = V
43 6 adantr φ U ˙ N X = V W LVec
44 1 3 2 5 islshp W LVec U H U S U V v V N U v = V
45 43 44 syl φ U ˙ N X = V U H U S U V v V N U v = V
46 17 18 42 45 mpbir3and φ U ˙ N X = V U H
47 16 46 impbida φ U H U ˙ N X = V