Theorem lclkrlem2

Description: The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a through lclkrlem2y are used for the proof. Here we express lclkrlem2y in terms of membership in the set C of functionals with closed kernels. (Contributed by NM, 18-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lclkrlem2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrlem2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrlem2.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lclkrlem2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lclkrlem2.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lclkrlem2.p	⊢ + = ( +g ‘ 𝐷 )
	lclkrlem2.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lclkrlem2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lclkrlem2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐶 )
	lclkrlem2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
Assertion	lclkrlem2	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lclkrlem2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lclkrlem2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lclkrlem2.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
5		lclkrlem2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
6		lclkrlem2.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
7		lclkrlem2.p	⊢ + = ( +g ‘ 𝐷 )
8		lclkrlem2.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
9		lclkrlem2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lclkrlem2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐶 )
11		lclkrlem2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
12	8	lcfl1lem	⊢ ( 𝐸 ∈ 𝐶 ↔ ( 𝐸 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ) )
13	12	simplbi	⊢ ( 𝐸 ∈ 𝐶 → 𝐸 ∈ 𝐹 )
14	10 13	syl	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
15	8	lcfl1lem	⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
16	15	simplbi	⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐹 )
17	11 16	syl	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
18	8 14	lcfl1	⊢ ( 𝜑 → ( 𝐸 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ) )
19	10 18	mpbid	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) )
20	8 17	lcfl1	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
21	11 20	mpbid	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
22	5 1 2 3 4 6 7 9 14 17 19 21	lclkrlem2y	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
23	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
24	4 6 7 23 14 17	ldualvaddcl	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
25	8 24	lcfl1	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
26	22 25	mpbird	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐶 )