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 𝐻 = ( LHyp ‘ 𝐾 )
dochkrshp2.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochkrshp2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochkrshp2.v 𝑉 = ( Base ‘ 𝑈 )
dochkrshp2.y 𝑌 = ( LSHyp ‘ 𝑈 )
dochkrshp2.f 𝐹 = ( LFnl ‘ 𝑈 )
dochkrshp2.l 𝐿 = ( LKer ‘ 𝑈 )
dochkrshp2.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dochkrshp2.g ( 𝜑𝐺𝐹 )
Assertion dochkrshp2 ( 𝜑 → ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) ≠ 𝑉 ↔ ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( 𝐿𝐺 ) ∈ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dochkrshp2.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochkrshp2.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochkrshp2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochkrshp2.v 𝑉 = ( Base ‘ 𝑈 )
5 dochkrshp2.y 𝑌 = ( LSHyp ‘ 𝑈 )
6 dochkrshp2.f 𝐹 = ( LFnl ‘ 𝑈 )
7 dochkrshp2.l 𝐿 = ( LKer ‘ 𝑈 )
8 dochkrshp2.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
9 dochkrshp2.g ( 𝜑𝐺𝐹 )
10 1 2 3 4 5 6 7 8 9 dochkrshp ( 𝜑 → ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) ≠ 𝑉 ↔ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) ∈ 𝑌 ) )
11 1 2 3 6 5 7 8 9 dochlkr ( 𝜑 → ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) ∈ 𝑌 ↔ ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( 𝐿𝐺 ) ∈ 𝑌 ) ) )
12 10 11 bitrd ( 𝜑 → ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) ≠ 𝑉 ↔ ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( 𝐿𝐺 ) ∈ 𝑌 ) ) )