Metamath Proof Explorer


Theorem lcfl5

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

Ref Expression
Hypotheses lcfl5.h 𝐻 = ( LHyp ‘ 𝐾 )
lcfl5.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
lcfl5.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfl5.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfl5.f 𝐹 = ( LFnl ‘ 𝑈 )
lcfl5.l 𝐿 = ( LKer ‘ 𝑈 )
lcfl5.c 𝐶 = { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
lcfl5.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lcfl5.g ( 𝜑𝐺𝐹 )
Assertion lcfl5 ( 𝜑 → ( 𝐺𝐶 ↔ ( 𝐿𝐺 ) ∈ ran 𝐼 ) )

Proof

Step Hyp Ref Expression
1 lcfl5.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfl5.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfl5.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfl5.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 lcfl5.f 𝐹 = ( LFnl ‘ 𝑈 )
6 lcfl5.l 𝐿 = ( LKer ‘ 𝑈 )
7 lcfl5.c 𝐶 = { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
8 lcfl5.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
9 lcfl5.g ( 𝜑𝐺𝐹 )
10 7 9 lcfl1 ( 𝜑 → ( 𝐺𝐶 ↔ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ) )
11 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
12 1 4 8 dvhlmod ( 𝜑𝑈 ∈ LMod )
13 11 5 6 12 9 lkrssv ( 𝜑 → ( 𝐿𝐺 ) ⊆ ( Base ‘ 𝑈 ) )
14 1 2 4 11 3 8 13 dochoccl ( 𝜑 → ( ( 𝐿𝐺 ) ∈ ran 𝐼 ↔ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ) )
15 10 14 bitr4d ( 𝜑 → ( 𝐺𝐶 ↔ ( 𝐿𝐺 ) ∈ ran 𝐼 ) )