Metamath Proof Explorer


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 ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐶 )