Metamath Proof Explorer

Theorem lcfls1c

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

Ref Expression
Hypotheses lcfls1.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f ∧ ⊥ ˙ ⁡ L ⁡ f ⊆ Q
lcfls1c.c ⊢ D = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
Assertion lcfls1c ⊢ G ∈ C ↔ G ∈ D ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q

Proof

Step Hyp Ref Expression
1 lcfls1.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f ∧ ⊥ ˙ ⁡ L ⁡ f ⊆ Q
2 lcfls1c.c ⊢ D = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
3 df-3an ⊢ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q
4 1 lcfls1lem ⊢ G ∈ C ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q
5 2 lcfl1lem ⊢ G ∈ D ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
6 5 anbi1i ⊢ G ∈ D ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q
7 3 4 6 3bitr4i ⊢ G ∈ C ↔ G ∈ D ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q