Metamath Proof Explorer

Theorem dochshpncl

Description: If a hyperplane is not closed, its closure equals the vector space. (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses dochshpncl.h 𝐻 = ( LHyp ‘ 𝐾 )
dochshpncl.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochshpncl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochshpncl.v 𝑉 = ( Base ‘ 𝑈 )
dochshpncl.y 𝑌 = ( LSHyp ‘ 𝑈 )
dochshpncl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dochshpncl.x ( 𝜑𝑋𝑌 )
Assertion dochshpncl ( 𝜑 → ( ( ‘ ( 𝑋 ) ) ≠ 𝑋 ↔ ( ‘ ( 𝑋 ) ) = 𝑉 ) )

Proof

Step Hyp Ref Expression
1 dochshpncl.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochshpncl.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochshpncl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochshpncl.v 𝑉 = ( Base ‘ 𝑈 )
5 dochshpncl.y 𝑌 = ( LSHyp ‘ 𝑈 )
6 dochshpncl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
7 dochshpncl.x ( 𝜑𝑋𝑌 )
8 eqid ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
9 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
10 eqid ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
11 1 3 6 dvhlmod ( 𝜑𝑈 ∈ LMod )
12 4 8 9 10 5 11 islshpsm ( 𝜑 → ( 𝑋𝑌 ↔ ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) ∧ 𝑋𝑉 ∧ ∃ 𝑣𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
13 7 12 mpbid ( 𝜑 → ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) ∧ 𝑋𝑉 ∧ ∃ 𝑣𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
14 13 simp3d ( 𝜑 → ∃ 𝑣𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 )
15 14 adantr ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) → ∃ 𝑣𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 )
16 id ( ( 𝜑𝑣𝑉 ) → ( 𝜑𝑣𝑉 ) )
17 16 adantlr ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ) → ( 𝜑𝑣𝑉 ) )
18 17 3adant3 ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝜑𝑣𝑉 ) )
19 9 5 11 7 lshplss ( 𝜑𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
20 4 9 lssss ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) → 𝑋𝑉 )
21 19 20 syl ( 𝜑𝑋𝑉 )
22 1 3 4 2 dochocss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝑋 ⊆ ( ‘ ( 𝑋 ) ) )
23 6 21 22 syl2anc ( 𝜑𝑋 ⊆ ( ‘ ( 𝑋 ) ) )
24 23 adantr ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) → 𝑋 ⊆ ( ‘ ( 𝑋 ) ) )
25 24 3ad2ant1 ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → 𝑋 ⊆ ( ‘ ( 𝑋 ) ) )
26 simp1r ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ‘ ( 𝑋 ) ) ≠ 𝑋 )
27 26 necomd ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → 𝑋 ≠ ( ‘ ( 𝑋 ) ) )
28 df-pss ( 𝑋 ⊊ ( ‘ ( 𝑋 ) ) ↔ ( 𝑋 ⊆ ( ‘ ( 𝑋 ) ) ∧ 𝑋 ≠ ( ‘ ( 𝑋 ) ) ) )
29 25 27 28 sylanbrc ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → 𝑋 ⊊ ( ‘ ( 𝑋 ) ) )
30 1 3 4 2 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ⊆ 𝑉 )
31 6 21 30 syl2anc ( 𝜑 → ( 𝑋 ) ⊆ 𝑉 )
32 1 3 4 2 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 ) ⊆ 𝑉 ) → ( ‘ ( 𝑋 ) ) ⊆ 𝑉 )
33 6 31 32 syl2anc ( 𝜑 → ( ‘ ( 𝑋 ) ) ⊆ 𝑉 )
34 33 adantr ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) → ( ‘ ( 𝑋 ) ) ⊆ 𝑉 )
35 34 3ad2ant1 ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ‘ ( 𝑋 ) ) ⊆ 𝑉 )
36 simp3 ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 )
37 35 36 sseqtrrd ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ‘ ( 𝑋 ) ) ⊆ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
38 6 adantr ( ( 𝜑𝑣𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
39 1 3 38 dvhlvec ( ( 𝜑𝑣𝑉 ) → 𝑈 ∈ LVec )
40 19 adantr ( ( 𝜑𝑣𝑉 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
41 1 3 4 9 2 dochlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 ) ⊆ 𝑉 ) → ( ‘ ( 𝑋 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
42 6 31 41 syl2anc ( 𝜑 → ( ‘ ( 𝑋 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
43 42 adantr ( ( 𝜑𝑣𝑉 ) → ( ‘ ( 𝑋 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
44 simpr ( ( 𝜑𝑣𝑉 ) → 𝑣𝑉 )
45 4 9 8 10 39 40 43 44 lsmcv ( ( ( 𝜑𝑣𝑉 ) ∧ 𝑋 ⊊ ( ‘ ( 𝑋 ) ) ∧ ( ‘ ( 𝑋 ) ) ⊆ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ‘ ( 𝑋 ) ) = ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
46 18 29 37 45 syl3anc ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ‘ ( 𝑋 ) ) = ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
47 46 36 eqtrd ( ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ‘ ( 𝑋 ) ) = 𝑉 )
48 47 rexlimdv3a ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) → ( ∃ 𝑣𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 → ( ‘ ( 𝑋 ) ) = 𝑉 ) )
49 15 48 mpd ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) ≠ 𝑋 ) → ( ‘ ( 𝑋 ) ) = 𝑉 )
50 simpr ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) = 𝑉 ) → ( ‘ ( 𝑋 ) ) = 𝑉 )
51 4 5 11 7 lshpne ( 𝜑𝑋𝑉 )
52 51 adantr ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) = 𝑉 ) → 𝑋𝑉 )
53 52 necomd ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) = 𝑉 ) → 𝑉𝑋 )
54 50 53 eqnetrd ( ( 𝜑 ∧ ( ‘ ( 𝑋 ) ) = 𝑉 ) → ( ‘ ( 𝑋 ) ) ≠ 𝑋 )
55 49 54 impbida ( 𝜑 → ( ( ‘ ( 𝑋 ) ) ≠ 𝑋 ↔ ( ‘ ( 𝑋 ) ) = 𝑉 ) )