Metamath Proof Explorer

Theorem dochkrsat

Description: The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014)

Ref Expression
Hypotheses dochkrsat.h ⊢ H = LHyp ⁡ K
dochkrsat.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochkrsat.u ⊢ U = DVecH ⁡ K ⁡ W
dochkrsat.a ⊢ A = LSAtoms ⁡ U
dochkrsat.f ⊢ F = LFnl ⁡ U
dochkrsat.l ⊢ L = LKer ⁡ U
dochkrsat.z ⊢ 0 ˙ = 0 U
dochkrsat.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochkrsat.g ⊢ φ → G ∈ F
Assertion dochkrsat ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ≠ 0 ˙ ↔ ⊥ ˙ ⁡ L ⁡ G ∈ A

Proof

Step Hyp Ref Expression
1 dochkrsat.h ⊢ H = LHyp ⁡ K
2 dochkrsat.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochkrsat.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochkrsat.a ⊢ A = LSAtoms ⁡ U
5 dochkrsat.f ⊢ F = LFnl ⁡ U
6 dochkrsat.l ⊢ L = LKer ⁡ U
7 dochkrsat.z ⊢ 0 ˙ = 0 U
8 dochkrsat.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dochkrsat.g ⊢ φ → G ∈ F
10 eqid ⊢ Base U = Base U
11 eqid ⊢ LSHyp ⁡ U = LSHyp ⁡ U
12 1 2 3 10 11 5 6 8 9 dochkrshp ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ Base U ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ∈ LSHyp ⁡ U
13 1 3 8 dvhlmod ⊢ φ → U ∈ LMod
14 10 5 6 13 9 lkrssv ⊢ φ → L ⁡ G ⊆ Base U
15 1 2 3 10 7 8 14 dochn0nv ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ≠ 0 ˙ ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ Base U
16 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
17 1 3 10 16 2 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ L ⁡ G ⊆ Base U → ⊥ ˙ ⁡ L ⁡ G ∈ LSubSp ⁡ U
18 8 14 17 syl2anc ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ∈ LSubSp ⁡ U
19 1 2 3 16 4 11 8 18 dochsatshpb ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ∈ A ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ∈ LSHyp ⁡ U
20 12 15 19 3bitr4d ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ≠ 0 ˙ ↔ ⊥ ˙ ⁡ L ⁡ G ∈ A