Metamath Proof Explorer

Theorem lshpinN

Description: The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lshpin.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpin.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lshpin.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐻 )
lshpin.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
Assertion lshpinN ( 𝜑 → ( ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ↔ 𝑇 = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lshpin.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
2 lshpin.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
3 lshpin.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐻 )
4 lshpin.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
5 inss1 ⊢ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑇
6 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → 𝑊 ∈ LVec )
7 simpr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 )
8 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → 𝑇 ∈ 𝐻 )
9 1 6 7 8 lshpcmp ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑇 ↔ ( 𝑇 ∩ 𝑈 ) = 𝑇 ) )
10 5 9 mpbii ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → ( 𝑇 ∩ 𝑈 ) = 𝑇 )
11 inss2 ⊢ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈
12 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → 𝑈 ∈ 𝐻 )
13 1 6 7 12 lshpcmp ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 ↔ ( 𝑇 ∩ 𝑈 ) = 𝑈 ) )
14 11 13 mpbii ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → ( 𝑇 ∩ 𝑈 ) = 𝑈 )
15 10 14 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) → 𝑇 = 𝑈 )
16 15 ex ⊢ ( 𝜑 → ( ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 → 𝑇 = 𝑈 ) )
17 inidm ⊢ ( 𝑇 ∩ 𝑇 ) = 𝑇
18 17 3 eqeltrid ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑇 ) ∈ 𝐻 )
19 ineq2 ⊢ ( 𝑇 = 𝑈 → ( 𝑇 ∩ 𝑇 ) = ( 𝑇 ∩ 𝑈 ) )
20 19 eleq1d ⊢ ( 𝑇 = 𝑈 → ( ( 𝑇 ∩ 𝑇 ) ∈ 𝐻 ↔ ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) )
21 18 20 syl5ibcom ⊢ ( 𝜑 → ( 𝑇 = 𝑈 → ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ) )
22 16 21 impbid ⊢ ( 𝜑 → ( ( 𝑇 ∩ 𝑈 ) ∈ 𝐻 ↔ 𝑇 = 𝑈 ) )