This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 dochkrshp3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochkrshp3.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochkrshp3.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochkrshp3.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochkrshp3.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6 dochkrshp3.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
7 dochkrshp3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 dochkrshp3.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 eqid ⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
10 1 2 3 4 9 5 6 7 8 dochkrshp2 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ) )
11 1 3 7 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
12 4 9 5 6 11 8 lkrshp4 ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ↔ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) )
13 12 anbi2d ⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ) )
14 10 13 bitr4d ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) )