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

Metamath Proof Explorer

Theorem dochsnkrlem2

Description: Lemma for dochsnkr . (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochsnkr.h ⊢ H = LHyp ⁡ K
dochsnkr.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochsnkr.u ⊢ U = DVecH ⁡ K ⁡ W
dochsnkr.v ⊢ V = Base U
dochsnkr.z ⊢ 0 ˙ = 0 U
dochsnkr.f ⊢ F = LFnl ⁡ U
dochsnkr.l ⊢ L = LKer ⁡ U
dochsnkr.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochsnkr.g ⊢ φ → G ∈ F
dochsnkr.x ⊢ φ → X ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙
dochsnkr.a ⊢ A = LSAtoms ⁡ U
Assertion dochsnkrlem2 ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ∈ A

Proof

Step Hyp Ref Expression
1 dochsnkr.h ⊢ H = LHyp ⁡ K
2 dochsnkr.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochsnkr.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochsnkr.v ⊢ V = Base U
5 dochsnkr.z ⊢ 0 ˙ = 0 U
6 dochsnkr.f ⊢ F = LFnl ⁡ U
7 dochsnkr.l ⊢ L = LKer ⁡ U
8 dochsnkr.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dochsnkr.g ⊢ φ → G ∈ F
10 dochsnkr.x ⊢ φ → X ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙
11 dochsnkr.a ⊢ A = LSAtoms ⁡ U
12 1 2 3 4 5 6 7 8 9 10 dochsnkrlem1 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
13 1 2 3 4 11 6 7 8 9 dochkrsat2 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ L ⁡ G ∈ A
14 12 13 mpbid ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ∈ A