Theorem dochkrshp

Description: The closure of a kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014)

	Ref	Expression
Hypotheses	dochkrshp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochkrshp.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochkrshp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochkrshp.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochkrshp.y	⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
	dochkrshp.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	dochkrshp.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	dochkrshp.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochkrshp.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	dochkrshp	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		dochkrshp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochkrshp.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochkrshp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochkrshp.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochkrshp.y	⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6		dochkrshp.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		dochkrshp.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
8		dochkrshp.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		dochkrshp.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10		simpr	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) )
11	8	adantr	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		2fveq3	⊢ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) )
13	1 3 2 4 8	dochoc1	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
14	12 13	sylan9eqr	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 )
15		simpr	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
16	14 15	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
17	16	ex	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
18	17	necon3d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) → ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) )
19		df-ne	⊢ ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ↔ ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 )
20	1 3 8	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
21	4 5 6 7 20 9	lkrshpor	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
22	21	orcomd	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
23	22	ord	⊢ ( 𝜑 → ( ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
24	19 23	syl5bi	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
25	18 24	syld	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
26	25	imp	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 )
27	1 2 3 4 5 11 26	dochshpncl	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 ) )
28	10 27	mpbid	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 )
29	28	ex	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( 𝐿 ‘ 𝐺 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 ) )
30	29	necon1d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
31	14	ex	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑉 ) )
32	31	necon3ad	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
33	32 23	syld	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
34	30 33	jcad	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) ) )
35	1 2 3 6 5 7 8 9	dochlkr	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) ) )
36	34 35	sylibrd	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) )
37	1 3 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
38	37	adantr	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → 𝑈 ∈ LMod )
39		simpr	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 )
40	4 5 38 39	lshpne	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
41	40	ex	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
42	36 41	impbid	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) )