Metamath Proof Explorer

Theorem dochsnkrlem3

Description: Lemma for dochsnkr . (Contributed by NM, 2-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 ˙
Assertion dochsnkrlem3 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G

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 1 2 3 4 5 6 7 8 9 10 dochsnkrlem1 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
12 11 orcd ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V
13 1 2 3 4 6 7 8 9 dochkrshp4 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V
14 12 13 mpbird ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G