Metamath Proof Explorer


Theorem dochsnkrlem1

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 ˙
Assertion dochsnkrlem1 φ ˙ ˙ L G V

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 eldif X ˙ L G 0 ˙ X ˙ L G ¬ X 0 ˙
12 nelne1 X ˙ L G ¬ X 0 ˙ ˙ L G 0 ˙
13 11 12 sylbi X ˙ L G 0 ˙ ˙ L G 0 ˙
14 10 13 syl φ ˙ L G 0 ˙
15 1 3 8 dvhlmod φ U LMod
16 4 6 7 15 9 lkrssv φ L G V
17 1 2 3 4 5 8 16 dochn0nv φ ˙ L G 0 ˙ ˙ ˙ L G V
18 14 17 mpbid φ ˙ ˙ L G V