Metamath Proof Explorer

Theorem lshpcmp

Description: If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 lshpcmp.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
2 lshpcmp.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
3 lshpcmp.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐻 )
4 lshpcmp.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
7 2 6 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 5 1 7 4 lshpne ⊢ ( 𝜑 → 𝑈 ≠ ( Base ‘ 𝑊 ) )
9 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10 9 1 7 4 lshplss ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
11 5 9 lssss ⊢ ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
12 10 11 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
13 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
14 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
15 5 13 9 14 1 7 islshpsm ⊢ ( 𝜑 → ( 𝑇 ∈ 𝐻 ↔ ( 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑇 ≠ ( Base ‘ 𝑊 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) )
16 3 15 mpbid ⊢ ( 𝜑 → ( 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑇 ≠ ( Base ‘ 𝑊 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) )
17 16 simp3d ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) )
18 id ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) )
19 18 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) → ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) )
20 2 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ LVec )
21 9 1 7 3 lshplss ⊢ ( 𝜑 → 𝑇 ∈ ( LSubSp ‘ 𝑊 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑇 ∈ ( LSubSp ‘ 𝑊 ) )
23 10 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
25 5 9 13 14 20 22 23 24 lsmcv ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) → 𝑈 = ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
26 19 25 syl3an1 ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) → 𝑈 = ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
27 26 3expia ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) ∧ 𝑇 ⊊ 𝑈 ) → ( 𝑈 ⊆ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑈 = ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) )
28 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) ∧ 𝑇 ⊊ 𝑈 ) → ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) )
29 28 sseq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) ∧ 𝑇 ⊊ 𝑈 ) → ( 𝑈 ⊆ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ↔ 𝑈 ⊆ ( Base ‘ 𝑊 ) ) )
30 28 eqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) ∧ 𝑇 ⊊ 𝑈 ) → ( 𝑈 = ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ↔ 𝑈 = ( Base ‘ 𝑊 ) ) )
31 27 29 30 3imtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) ∧ 𝑇 ⊊ 𝑈 ) → ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑊 ) ) )
32 31 exp42 ⊢ ( 𝜑 → ( 𝑣 ∈ ( Base ‘ 𝑊 ) → ( ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) → ( 𝑇 ⊊ 𝑈 → ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑊 ) ) ) ) ) )
33 32 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) → ( 𝑇 ⊊ 𝑈 → ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑊 ) ) ) ) )
34 17 33 mpd ⊢ ( 𝜑 → ( 𝑇 ⊊ 𝑈 → ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑊 ) ) ) )
35 12 34 mpid ⊢ ( 𝜑 → ( 𝑇 ⊊ 𝑈 → 𝑈 = ( Base ‘ 𝑊 ) ) )
36 35 necon3ad ⊢ ( 𝜑 → ( 𝑈 ≠ ( Base ‘ 𝑊 ) → ¬ 𝑇 ⊊ 𝑈 ) )
37 8 36 mpd ⊢ ( 𝜑 → ¬ 𝑇 ⊊ 𝑈 )
38 df-pss ⊢ ( 𝑇 ⊊ 𝑈 ↔ ( 𝑇 ⊆ 𝑈 ∧ 𝑇 ≠ 𝑈 ) )
39 38 simplbi2 ⊢ ( 𝑇 ⊆ 𝑈 → ( 𝑇 ≠ 𝑈 → 𝑇 ⊊ 𝑈 ) )
40 39 necon1bd ⊢ ( 𝑇 ⊆ 𝑈 → ( ¬ 𝑇 ⊊ 𝑈 → 𝑇 = 𝑈 ) )
41 37 40 syl5com ⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 → 𝑇 = 𝑈 ) )
42 eqimss ⊢ ( 𝑇 = 𝑈 → 𝑇 ⊆ 𝑈 )
43 41 42 impbid1 ⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) )