Metamath Proof Explorer

Theorem islshpsm

Description: Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014)

Ref Expression
Hypotheses islshpsm.v 
|- V = ( Base ` W )
islshpsm.n 
|- N = ( LSpan ` W )
islshpsm.s 
|- S = ( LSubSp ` W )
islshpsm.p 
|- .(+) = ( LSSum ` W )
islshpsm.h 
|- H = ( LSHyp ` W )
islshpsm.w 
|- ( ph -> W e. LMod )
Assertion islshpsm 
|- ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) ) )

Proof

Step Hyp Ref Expression
1 islshpsm.v 
 |-  V = ( Base ` W )
2 islshpsm.n 
 |-  N = ( LSpan ` W )
3 islshpsm.s 
 |-  S = ( LSubSp ` W )
4 islshpsm.p 
 |-  .(+) = ( LSSum ` W )
5 islshpsm.h 
 |-  H = ( LSHyp ` W )
6 islshpsm.w 
 |-  ( ph -> W e. LMod )
7 1 2 3 5 islshp 
 |-  ( W e. LMod -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
8 6 7 syl 
 |-  ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
9 6 ad2antrr 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> W e. LMod )
10 simplrl 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> U e. S )
11 3 2 lspid 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U )
12 9 10 11 syl2anc 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> ( N ` U ) = U )
13 12 uneq1d 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> ( ( N ` U ) u. ( N ` { v } ) ) = ( U u. ( N ` { v } ) ) )
14 13 fveq2d 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> ( N ` ( ( N ` U ) u. ( N ` { v } ) ) ) = ( N ` ( U u. ( N ` { v } ) ) ) )
15 1 3 lssss 
 |-  ( U e. S -> U C_ V )
16 10 15 syl 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> U C_ V )
17 snssi 
 |-  ( v e. V -> { v } C_ V )
18 17 adantl 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> { v } C_ V )
19 1 2 lspun 
 |-  ( ( W e. LMod /\ U C_ V /\ { v } C_ V ) -> ( N ` ( U u. { v } ) ) = ( N ` ( ( N ` U ) u. ( N ` { v } ) ) ) )
20 9 16 18 19 syl3anc 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> ( N ` ( U u. { v } ) ) = ( N ` ( ( N ` U ) u. ( N ` { v } ) ) ) )
21 1 3 2 lspcl 
 |-  ( ( W e. LMod /\ { v } C_ V ) -> ( N ` { v } ) e. S )
22 9 18 21 syl2anc 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> ( N ` { v } ) e. S )
23 3 2 4 lsmsp 
 |-  ( ( W e. LMod /\ U e. S /\ ( N ` { v } ) e. S ) -> ( U .(+) ( N ` { v } ) ) = ( N ` ( U u. ( N ` { v } ) ) ) )
24 9 10 22 23 syl3anc 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> ( U .(+) ( N ` { v } ) ) = ( N ` ( U u. ( N ` { v } ) ) ) )
25 14 20 24 3eqtr4rd 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> ( U .(+) ( N ` { v } ) ) = ( N ` ( U u. { v } ) ) )
26 25 eqeq1d 
 |-  ( ( ( ph /\ ( U e. S /\ U =/= V ) ) /\ v e. V ) -> ( ( U .(+) ( N ` { v } ) ) = V <-> ( N ` ( U u. { v } ) ) = V ) )
27 26 rexbidva 
 |-  ( ( ph /\ ( U e. S /\ U =/= V ) ) -> ( E. v e. V ( U .(+) ( N ` { v } ) ) = V <-> E. v e. V ( N ` ( U u. { v } ) ) = V ) )
28 27 pm5.32da 
 |-  ( ph -> ( ( ( U e. S /\ U =/= V ) /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
29 28 bicomd 
 |-  ( ph -> ( ( ( U e. S /\ U =/= V ) /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) ) )
30 df-3an 
 |-  ( ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) )
31 df-3an 
 |-  ( ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) )
32 29 30 31 3bitr4g 
 |-  ( ph -> ( ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) <-> ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) ) )
33 8 32 bitrd 
 |-  ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) ) )