Metamath Proof Explorer

Theorem dochkrshp3

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=BaseU
dochkrshp3.f ⊢F=LFnl⁡U
dochkrshp3.l ⊢L=LKer⁡U
dochkrshp3.k ⊢φ→K∈HL∧W∈H
dochkrshp3.g ⊢φ→G∈F
Assertion dochkrshp3 ⊢φ→⊥˙⁡⊥˙⁡L⁡G≠V↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧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=BaseU
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 eqid ⊢LSHyp⁡U=LSHyp⁡U
10 1 2 3 4 9 5 6 7 8 dochkrshp2 ⊢φ→⊥˙⁡⊥˙⁡L⁡G≠V↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧L⁡G∈LSHyp⁡U
11 1 3 7 dvhlvec ⊢φ→U∈LVec
12 4 9 5 6 11 8 lkrshp4 ⊢φ→L⁡G≠V↔L⁡G∈LSHyp⁡U
13 12 anbi2d ⊢φ→⊥˙⁡⊥˙⁡L⁡G=L⁡G∧L⁡G≠V↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧L⁡G∈LSHyp⁡U
14 10 13 bitr4d ⊢φ→⊥˙⁡⊥˙⁡L⁡G≠V↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧L⁡G≠V