Theorem lcfl4N

Description: Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lcfl4.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfl4.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl4.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl4.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfl4.y	⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
	lcfl4.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfl4.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfl4.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lcfl4.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfl4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lcfl4N	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcfl4.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfl4.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfl4.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfl4.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcfl4.y	⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6		lcfl4.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		lcfl4.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
8		lcfl4.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
9		lcfl4.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcfl4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11		eqid	⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
12	1 2 3 4 11 6 7 8 9 10	lcfl3	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )
13		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
14	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
15	4 6 7 14 10	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
16	1 3 4 13 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
17	9 15 16	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
18	1 2 3 13 11 5 9 17	dochsatshpb	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ) )
19	18	orbi1d	⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )
20	12 19	bitrd	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ 𝑌 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )