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	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) )