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