dochlkr

Description: Equivalent conditions for the closure of a kernel to be a hyperplane. (Contributed by NM, 29-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dochlkr.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochlkr.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochlkr.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochlkr.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
5		dochlkr.y	⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6		dochlkr.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		dochlkr.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		dochlkr.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
10	1 3 7	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
11	9 4 6 10 8	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) )
12	1 3 9 2	dochocss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
13	7 11 12	syl2anc	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
15	1 3 7	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → 𝑈 ∈ LVec )
17	10	adantr	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → 𝑈 ∈ LMod )
18		simpr	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 )
19	9 5 17 18	lshpne	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( Base ‘ 𝑈 ) )
20	19	ex	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( Base ‘ 𝑈 ) ) )
21	9 5 4 6 15 8	lkrshpor	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ∨ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) )
22	21	ord	⊢ ( 𝜑 → ( ¬ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 → ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) )
23		2fveq3	⊢ ( ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) )
25	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
26	1 3 2 9 25	dochoc1	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) = ( Base ‘ 𝑈 ) )
27	24 26	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( Base ‘ 𝑈 ) )
28	27	ex	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = ( Base ‘ 𝑈 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( Base ‘ 𝑈 ) ) )
29	22 28	syld	⊢ ( 𝜑 → ( ¬ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( Base ‘ 𝑈 ) ) )
30	29	necon1ad	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( Base ‘ 𝑈 ) → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
31	20 30	syld	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
32	31	imp	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 )
33	5 16 32 18	lshpcmp	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ↔ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) )
34	14 33	mpbid	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
35	34	eqcomd	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
36	35 32	jca	⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
37	36	ex	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) ) )
38		eleq1	⊢ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ↔ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) )
39	38	biimpar	⊢ ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 )
40	37 39	impbid1	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ∈ 𝑌 ) ) )

Metamath Proof Explorer

Theorem dochlkr

Proof