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 ⊢H=LHyp⁡K
dochlkr.o ⊢⊥˙=ocH⁡K⁡W
dochlkr.u ⊢U=DVecH⁡K⁡W
dochlkr.f ⊢F=LFnl⁡U
dochlkr.y ⊢Y=LSHyp⁡U
dochlkr.l ⊢L=LKer⁡U
dochlkr.k ⊢φ→K∈HL∧W∈H
dochlkr.g ⊢φ→G∈F
Assertion dochlkr ⊢φ→⊥˙⁡⊥˙⁡L⁡G∈Y↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧L⁡G∈Y

Proof

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