# Metamath Proof Explorer

## Theorem islshpsm

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

Ref Expression
Hypotheses islshpsm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
islshpsm.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
islshpsm.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
islshpsm.p
islshpsm.h ${⊢}{H}=\mathrm{LSHyp}\left({W}\right)$
islshpsm.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
Assertion islshpsm

### Proof

Step Hyp Ref Expression
1 islshpsm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 islshpsm.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 islshpsm.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
4 islshpsm.p
5 islshpsm.h ${⊢}{H}=\mathrm{LSHyp}\left({W}\right)$
6 islshpsm.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
7 1 2 3 5 islshp ${⊢}{W}\in \mathrm{LMod}\to \left({U}\in {H}↔\left({U}\in {S}\wedge {U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)\right)$
8 6 7 syl ${⊢}{\phi }\to \left({U}\in {H}↔\left({U}\in {S}\wedge {U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)\right)$
9 6 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to {W}\in \mathrm{LMod}$
10 simplrl ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to {U}\in {S}$
11 3 2 lspid ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {N}\left({U}\right)={U}$
12 9 10 11 syl2anc ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to {N}\left({U}\right)={U}$
13 12 uneq1d ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to {N}\left({U}\right)\cup {N}\left(\left\{{v}\right\}\right)={U}\cup {N}\left(\left\{{v}\right\}\right)$
14 13 fveq2d ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to {N}\left({N}\left({U}\right)\cup {N}\left(\left\{{v}\right\}\right)\right)={N}\left({U}\cup {N}\left(\left\{{v}\right\}\right)\right)$
15 1 3 lssss ${⊢}{U}\in {S}\to {U}\subseteq {V}$
16 10 15 syl ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to {U}\subseteq {V}$
17 snssi ${⊢}{v}\in {V}\to \left\{{v}\right\}\subseteq {V}$
18 17 adantl ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to \left\{{v}\right\}\subseteq {V}$
19 1 2 lspun ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\subseteq {V}\wedge \left\{{v}\right\}\subseteq {V}\right)\to {N}\left({U}\cup \left\{{v}\right\}\right)={N}\left({N}\left({U}\right)\cup {N}\left(\left\{{v}\right\}\right)\right)$
20 9 16 18 19 syl3anc ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to {N}\left({U}\cup \left\{{v}\right\}\right)={N}\left({N}\left({U}\right)\cup {N}\left(\left\{{v}\right\}\right)\right)$
21 1 3 2 lspcl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left\{{v}\right\}\subseteq {V}\right)\to {N}\left(\left\{{v}\right\}\right)\in {S}$
22 9 18 21 syl2anc ${⊢}\left(\left({\phi }\wedge \left({U}\in {S}\wedge {U}\ne {V}\right)\right)\wedge {v}\in {V}\right)\to {N}\left(\left\{{v}\right\}\right)\in {S}$
23 3 2 4 lsmsp
24 9 10 22 23 syl3anc
25 14 20 24 3eqtr4rd
26 25 eqeq1d
27 26 rexbidva
28 27 pm5.32da
29 28 bicomd
30 df-3an ${⊢}\left({U}\in {S}\wedge {U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)↔\left(\left({U}\in {S}\wedge {U}\ne {V}\right)\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)$
31 df-3an
32 29 30 31 3bitr4g
33 8 32 bitrd