Metamath Proof Explorer

Theorem dochkrshp2

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

Ref Expression
Hypotheses dochkrshp2.h ⊢H=LHyp⁡K
dochkrshp2.o ⊢⊥˙=ocH⁡K⁡W
dochkrshp2.u ⊢U=DVecH⁡K⁡W
dochkrshp2.v ⊢V=BaseU
dochkrshp2.y ⊢Y=LSHyp⁡U
dochkrshp2.f ⊢F=LFnl⁡U
dochkrshp2.l ⊢L=LKer⁡U
dochkrshp2.k ⊢φ→K∈HL∧W∈H
dochkrshp2.g ⊢φ→G∈F
Assertion dochkrshp2 ⊢φ→⊥˙⁡⊥˙⁡L⁡G≠V↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧L⁡G∈Y

Proof

Step Hyp Ref Expression
1 dochkrshp2.h ⊢H=LHyp⁡K
2 dochkrshp2.o ⊢⊥˙=ocH⁡K⁡W
3 dochkrshp2.u ⊢U=DVecH⁡K⁡W
4 dochkrshp2.v ⊢V=BaseU
5 dochkrshp2.y ⊢Y=LSHyp⁡U
6 dochkrshp2.f ⊢F=LFnl⁡U
7 dochkrshp2.l ⊢L=LKer⁡U
8 dochkrshp2.k ⊢φ→K∈HL∧W∈H
9 dochkrshp2.g ⊢φ→G∈F
10 1 2 3 4 5 6 7 8 9 dochkrshp ⊢φ→⊥˙⁡⊥˙⁡L⁡G≠V↔⊥˙⁡⊥˙⁡L⁡G∈Y
11 1 2 3 6 5 7 8 9 dochlkr ⊢φ→⊥˙⁡⊥˙⁡L⁡G∈Y↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧L⁡G∈Y
12 10 11 bitrd ⊢φ→⊥˙⁡⊥˙⁡L⁡G≠V↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧L⁡G∈Y