Metamath Proof Explorer


Theorem dochkrshp4

Description: Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochkrshp3.h H = LHyp K
dochkrshp3.o ˙ = ocH K W
dochkrshp3.u U = DVecH K W
dochkrshp3.v V = Base U
dochkrshp3.f F = LFnl U
dochkrshp3.l L = LKer U
dochkrshp3.k φ K HL W H
dochkrshp3.g φ G F
Assertion dochkrshp4 φ ˙ ˙ L G = L G ˙ ˙ L G V L G = V

Proof

Step Hyp Ref Expression
1 dochkrshp3.h H = LHyp K
2 dochkrshp3.o ˙ = ocH K W
3 dochkrshp3.u U = DVecH K W
4 dochkrshp3.v V = Base U
5 dochkrshp3.f F = LFnl U
6 dochkrshp3.l L = LKer U
7 dochkrshp3.k φ K HL W H
8 dochkrshp3.g φ G F
9 df-ne L G V ¬ L G = V
10 1 2 3 4 5 6 7 8 dochkrshp3 φ ˙ ˙ L G V ˙ ˙ L G = L G L G V
11 10 biimprd φ ˙ ˙ L G = L G L G V ˙ ˙ L G V
12 11 expdimp φ ˙ ˙ L G = L G L G V ˙ ˙ L G V
13 9 12 syl5bir φ ˙ ˙ L G = L G ¬ L G = V ˙ ˙ L G V
14 13 orrd φ ˙ ˙ L G = L G L G = V ˙ ˙ L G V
15 14 orcomd φ ˙ ˙ L G = L G ˙ ˙ L G V L G = V
16 15 ex φ ˙ ˙ L G = L G ˙ ˙ L G V L G = V
17 simpl ˙ ˙ L G = L G L G V ˙ ˙ L G = L G
18 10 17 syl6bi φ ˙ ˙ L G V ˙ ˙ L G = L G
19 1 3 2 4 7 dochoc1 φ ˙ ˙ V = V
20 2fveq3 L G = V ˙ ˙ L G = ˙ ˙ V
21 id L G = V L G = V
22 20 21 eqeq12d L G = V ˙ ˙ L G = L G ˙ ˙ V = V
23 19 22 syl5ibrcom φ L G = V ˙ ˙ L G = L G
24 18 23 jaod φ ˙ ˙ L G V L G = V ˙ ˙ L G = L G
25 16 24 impbid φ ˙ ˙ L G = L G ˙ ˙ L G V L G = V