Metamath Proof Explorer


Theorem lcfl5a

Description: Property of a functional with a closed kernel. TODO: Make lcfl5 etc. obsolete and rewrite without C hypothesis? (Contributed by NM, 29-Jan-2015)

Ref Expression
Hypotheses lcfl5a.h H = LHyp K
lcfl5a.i I = DIsoH K W
lcfl5a.o ˙ = ocH K W
lcfl5a.u U = DVecH K W
lcfl5a.f F = LFnl U
lcfl5a.l L = LKer U
lcfl5a.k φ K HL W H
lcfl5a.g φ G F
Assertion lcfl5a φ ˙ ˙ L G = L G L G ran I

Proof

Step Hyp Ref Expression
1 lcfl5a.h H = LHyp K
2 lcfl5a.i I = DIsoH K W
3 lcfl5a.o ˙ = ocH K W
4 lcfl5a.u U = DVecH K W
5 lcfl5a.f F = LFnl U
6 lcfl5a.l L = LKer U
7 lcfl5a.k φ K HL W H
8 lcfl5a.g φ G F
9 eqid f F | ˙ ˙ L f = L f = f F | ˙ ˙ L f = L f
10 9 8 lcfl1 φ G f F | ˙ ˙ L f = L f ˙ ˙ L G = L G
11 1 2 3 4 5 6 9 7 8 lcfl5 φ G f F | ˙ ˙ L f = L f L G ran I
12 10 11 bitr3d φ ˙ ˙ L G = L G L G ran I