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 ⊢ Base U = Base U
10 1 3 7 dvhlmod ⊢ φ → U ∈ LMod
11 9 4 6 10 8 lkrssv ⊢ φ → L ⁡ G ⊆ Base U
12 1 3 9 2 dochocss ⊢ K ∈ HL ∧ W ∈ H ∧ L ⁡ G ⊆ Base U → 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 ≠ Base U
20 19 ex ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ∈ Y → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ Base U
21 9 5 4 6 15 8 lkrshpor ⊢ φ → L ⁡ G ∈ Y ∨ L ⁡ G = Base U
22 21 ord ⊢ φ → ¬ L ⁡ G ∈ Y → L ⁡ G = Base U
23 2fveq3 ⊢ L ⁡ G = Base U → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = ⊥ ˙ ⁡ ⊥ ˙ ⁡ Base U
24 23 adantl ⊢ φ ∧ L ⁡ G = Base U → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = ⊥ ˙ ⁡ ⊥ ˙ ⁡ Base U
25 7 adantr ⊢ φ ∧ L ⁡ G = Base U → K ∈ HL ∧ W ∈ H
26 1 3 2 9 25 dochoc1 ⊢ φ ∧ L ⁡ G = Base U → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Base U = Base U
27 24 26 eqtrd ⊢ φ ∧ L ⁡ G = Base U → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = Base U
28 27 ex ⊢ φ → L ⁡ G = Base U → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = Base U
29 22 28 syld ⊢ φ → ¬ L ⁡ G ∈ Y → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = Base U
30 29 necon1ad ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ Base U → 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