# 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 ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) ) )`