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

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 
|- ( ph -> W e. LVec )
lshpnel2.u 
|- ( ph -> U e. S )
lshpnel2.t 
|- ( ph -> U =/= V )
lshpnel2.x 
|- ( ph -> X e. V )
lshpnel2.e 
|- ( ph -> -. X e. U )
Assertion lshpnel2N 
|- ( ph -> ( U e. 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 
 |-  ( ph -> W e. LVec )
7 lshpnel2.u 
 |-  ( ph -> U e. S )
8 lshpnel2.t 
 |-  ( ph -> U =/= V )
9 lshpnel2.x 
 |-  ( ph -> X e. V )
10 lshpnel2.e 
 |-  ( ph -> -. X e. U )
11 10 adantr 
 |-  ( ( ph /\ U e. H ) -> -. X e. U )
12 6 adantr 
 |-  ( ( ph /\ U e. H ) -> W e. LVec )
13 simpr 
 |-  ( ( ph /\ U e. H ) -> U e. H )
14 9 adantr 
 |-  ( ( ph /\ U e. H ) -> X e. V )
15 1 3 4 5 12 13 14 lshpnelb 
 |-  ( ( ph /\ U e. H ) -> ( -. X e. U <-> ( U .(+) ( N ` { X } ) ) = V ) )
16 11 15 mpbid 
 |-  ( ( ph /\ U e. H ) -> ( U .(+) ( N ` { X } ) ) = V )
17 7 adantr 
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> U e. S )
18 8 adantr 
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> U =/= V )
19 9 adantr 
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> X e. V )
20 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
21 6 20 syl 
 |-  ( ph -> W e. LMod )
22 2 3 lspid 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U )
23 21 7 22 syl2anc 
 |-  ( ph -> ( N ` U ) = U )
24 23 uneq1d 
 |-  ( ph -> ( ( N ` U ) u. ( N ` { X } ) ) = ( U u. ( N ` { X } ) ) )
25 24 fveq2d 
 |-  ( ph -> ( N ` ( ( N ` U ) u. ( N ` { X } ) ) ) = ( N ` ( U u. ( N ` { X } ) ) ) )
26 1 2 lssss 
 |-  ( U e. S -> U C_ V )
27 7 26 syl 
 |-  ( ph -> U C_ V )
28 9 snssd 
 |-  ( ph -> { X } C_ V )
29 1 3 lspun 
 |-  ( ( W e. LMod /\ U C_ V /\ { X } C_ V ) -> ( N ` ( U u. { X } ) ) = ( N ` ( ( N ` U ) u. ( N ` { X } ) ) ) )
30 21 27 28 29 syl3anc 
 |-  ( ph -> ( N ` ( U u. { X } ) ) = ( N ` ( ( N ` U ) u. ( N ` { X } ) ) ) )
31 1 2 3 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. S )
32 21 9 31 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. S )
33 2 3 4 lsmsp 
 |-  ( ( W e. LMod /\ U e. S /\ ( N ` { X } ) e. S ) -> ( U .(+) ( N ` { X } ) ) = ( N ` ( U u. ( N ` { X } ) ) ) )
34 21 7 32 33 syl3anc 
 |-  ( ph -> ( U .(+) ( N ` { X } ) ) = ( N ` ( U u. ( N ` { X } ) ) ) )
35 25 30 34 3eqtr4rd 
 |-  ( ph -> ( U .(+) ( N ` { X } ) ) = ( N ` ( U u. { X } ) ) )
36 35 eqeq1d 
 |-  ( ph -> ( ( U .(+) ( N ` { X } ) ) = V <-> ( N ` ( U u. { X } ) ) = V ) )
37 36 biimpa 
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> ( N ` ( U u. { X } ) ) = V )
38 sneq 
 |-  ( v = X -> { v } = { X } )
39 38 uneq2d 
 |-  ( v = X -> ( U u. { v } ) = ( U u. { X } ) )
40 39 fveqeq2d 
 |-  ( v = X -> ( ( N ` ( U u. { v } ) ) = V <-> ( N ` ( U u. { X } ) ) = V ) )
41 40 rspcev 
 |-  ( ( X e. V /\ ( N ` ( U u. { X } ) ) = V ) -> E. v e. V ( N ` ( U u. { v } ) ) = V )
42 19 37 41 syl2anc 
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> E. v e. V ( N ` ( U u. { v } ) ) = V )
43 6 adantr 
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> W e. LVec )
44 1 3 2 5 islshp 
 |-  ( W e. LVec -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
45 43 44 syl 
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
46 17 18 42 45 mpbir3and 
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> U e. H )
47 16 46 impbida 
 |-  ( ph -> ( U e. H <-> ( U .(+) ( N ` { X } ) ) = V ) )