Theorem lcfl3

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

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

Proof

Step	Hyp	Ref	Expression
1		lcfl3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfl3.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfl3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfl3.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcfl3.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
6		lcfl3.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		lcfl3.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
8		lcfl3.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
9		lcfl3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcfl3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11	1 2 3 4 6 7 8 9 10	lcfl2	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )
12	1 2 3 4 5 6 7 9 10	dochkrsat2	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )
13	12	orbi1d	⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )
14	11 13	bitrd	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )