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

Metamath Proof Explorer

Theorem dochlkr

Description: Equivalent conditions for the closure of a kernel to be a hyperplane. (Contributed by NM, 29-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 dochlkr.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochlkr.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochlkr.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochlkr.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
5 dochlkr.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6 dochlkr.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
7 dochlkr.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 dochlkr.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
10 1 3 7 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
11 9 4 6 10 8 lkrssv ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) )
12 1 3 9 2 dochocss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
13 7 11 12 syl2anc ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
15 1 3 7 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → 𝑈 ∈ LVec )
17 10 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → 𝑈 ∈ LMod )
18 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 )
19 9 5 17 18 lshpne ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( Base ‘ 𝑈 ) )
20 19 ex ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( Base ‘ 𝑈 ) ) )
21 9 5 4 6 15 8 lkrshpor ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ∨ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) )
22 21 ord ⊢ ( 𝜑 → ( ¬ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 → ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) )
23 2fveq3 ⊢ ( ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) )
24 23 adantl ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) )
25 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
26 1 3 2 9 25 dochoc1 ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) = ( Base ‘ 𝑈 ) )
27 24 26 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( Base ‘ 𝑈 ) )
28 27 ex ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( Base ‘ 𝑈 ) ) )
29 22 28 syld ⊢ ( 𝜑 → ( ¬ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( Base ‘ 𝑈 ) ) )
30 29 necon1ad ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( Base ‘ 𝑈 ) → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
31 20 30 syld ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
32 31 imp ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 )
33 5 16 32 18 lshpcmp ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ↔ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) )
34 14 33 mpbid ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
36 35 32 jca ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
37 36 ex ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) ) )
38 eleq1 ⊢ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ↔ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
39 38 biimpar ⊢ ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 )
40 37 39 impbid1 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) ) )