Metamath Proof Explorer


Theorem lcfls1N

Description: Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lcfls1.c C = f F | ˙ ˙ L f = L f ˙ L f Q
lcfls1.g φ G F
Assertion lcfls1N φ G C ˙ ˙ L G = L G ˙ L G Q

Proof

Step Hyp Ref Expression
1 lcfls1.c C = f F | ˙ ˙ L f = L f ˙ L f Q
2 lcfls1.g φ G F
3 1 lcfls1lem G C G F ˙ ˙ L G = L G ˙ L G Q
4 3anass G F ˙ ˙ L G = L G ˙ L G Q G F ˙ ˙ L G = L G ˙ L G Q
5 3 4 bitri G C G F ˙ ˙ L G = L G ˙ L G Q
6 2 biantrurd φ ˙ ˙ L G = L G ˙ L G Q G F ˙ ˙ L G = L G ˙ L G Q
7 5 6 bitr4id φ G C ˙ ˙ L G = L G ˙ L G Q