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

Metamath Proof Explorer

Theorem dochkrshp

Description: The closure of a kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014)

Ref Expression
Hypotheses dochkrshp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochkrshp.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochkrshp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochkrshp.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochkrshp.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
dochkrshp.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
dochkrshp.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochkrshp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochkrshp.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion dochkrshp ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dochkrshp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochkrshp.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochkrshp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochkrshp.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochkrshp.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6 dochkrshp.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 dochkrshp.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
8 dochkrshp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dochkrshp.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) )
11 8 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 2fveq3 ⊢ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) )
13 1 3 2 4 8 dochoc1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
14 12 13 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 )
15 simpr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
16 14 15 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
17 16 ex ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
18 17 necon3d ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) → ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) )
19 df-ne ⊢ ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ↔ ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 )
20 1 3 8 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
21 4 5 6 7 20 9 lkrshpor ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
22 21 orcomd ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
23 22 ord ⊢ ( 𝜑 → ( ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
24 19 23 biimtrid ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
25 18 24 syld ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
26 25 imp ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 )
27 1 2 3 4 5 11 26 dochshpncl ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 ) )
28 10 27 mpbid ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 )
29 28 ex ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 ) )
30 29 necon1d ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
31 14 ex ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 ) )
32 31 necon3ad ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
33 32 23 syld ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
34 30 33 jcad ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) ) )
35 1 2 3 6 5 7 8 9 dochlkr ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) ) )
36 34 35 sylibrd ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) )
37 1 3 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → 𝑈 ∈ LMod )
39 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 )
40 4 5 38 39 lshpne ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
41 40 ex ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
42 36 41 impbid ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) )