Metamath Proof Explorer


Theorem islshpsm

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

Ref Expression
Hypotheses islshpsm.v 𝑉 = ( Base ‘ 𝑊 )
islshpsm.n 𝑁 = ( LSpan ‘ 𝑊 )
islshpsm.s 𝑆 = ( LSubSp ‘ 𝑊 )
islshpsm.p = ( LSSum ‘ 𝑊 )
islshpsm.h 𝐻 = ( LSHyp ‘ 𝑊 )
islshpsm.w ( 𝜑𝑊 ∈ LMod )
Assertion islshpsm ( 𝜑 → ( 𝑈𝐻 ↔ ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑈 ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 islshpsm.v 𝑉 = ( Base ‘ 𝑊 )
2 islshpsm.n 𝑁 = ( LSpan ‘ 𝑊 )
3 islshpsm.s 𝑆 = ( LSubSp ‘ 𝑊 )
4 islshpsm.p = ( LSSum ‘ 𝑊 )
5 islshpsm.h 𝐻 = ( LSHyp ‘ 𝑊 )
6 islshpsm.w ( 𝜑𝑊 ∈ LMod )
7 1 2 3 5 islshp ( 𝑊 ∈ LMod → ( 𝑈𝐻 ↔ ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
8 6 7 syl ( 𝜑 → ( 𝑈𝐻 ↔ ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
9 6 ad2antrr ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → 𝑊 ∈ LMod )
10 simplrl ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → 𝑈𝑆 )
11 3 2 lspid ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑁𝑈 ) = 𝑈 )
12 9 10 11 syl2anc ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → ( 𝑁𝑈 ) = 𝑈 )
13 12 uneq1d ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → ( ( 𝑁𝑈 ) ∪ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑈 ∪ ( 𝑁 ‘ { 𝑣 } ) ) )
14 13 fveq2d ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → ( 𝑁 ‘ ( ( 𝑁𝑈 ) ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) = ( 𝑁 ‘ ( 𝑈 ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
15 1 3 lssss ( 𝑈𝑆𝑈𝑉 )
16 10 15 syl ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → 𝑈𝑉 )
17 snssi ( 𝑣𝑉 → { 𝑣 } ⊆ 𝑉 )
18 17 adantl ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → { 𝑣 } ⊆ 𝑉 )
19 1 2 lspun ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ∧ { 𝑣 } ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = ( 𝑁 ‘ ( ( 𝑁𝑈 ) ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
20 9 16 18 19 syl3anc ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = ( 𝑁 ‘ ( ( 𝑁𝑈 ) ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
21 1 3 2 lspcl ( ( 𝑊 ∈ LMod ∧ { 𝑣 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑣 } ) ∈ 𝑆 )
22 9 18 21 syl2anc ( ( ( 𝜑 ∧ ( 𝑈𝑆𝑈𝑉 ) ) ∧ 𝑣𝑉 ) → ( 𝑁 ‘ { 𝑣 } ) ∈ 𝑆 )
23 3 2 4 lsmsp ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ∧ ( 𝑁 ‘ { 𝑣 } ) ∈ 𝑆 ) → ( 𝑈 ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑁 ‘ ( 𝑈 ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
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 ( ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈𝑆𝑈𝑉 ) ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) )
31 df-3an ( ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑈 ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈𝑆𝑈𝑉 ) ∧ ∃ 𝑣𝑉 ( 𝑈 ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) )
32 29 30 31 3bitr4g ( 𝜑 → ( ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑈 ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )
33 8 32 bitrd ( 𝜑 → ( 𝑈𝐻 ↔ ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑈 ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )