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 syl5bi ( 𝜑 → ( ( 𝐿𝐺 ) ≠ 𝑉 → ( 𝐿𝐺 ) ∈ 𝑌 ) )
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 ( 𝜑 → ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) ≠ 𝑉 ↔ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) ∈ 𝑌 ) )