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

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 ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )