Metamath Proof Explorer

Theorem lcfls1lem

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

Ref Expression
Hypothesis lcfls1.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f ∧ ⊥ ˙ ⁡ L ⁡ f ⊆ Q
Assertion lcfls1lem ⊢ G ∈ C ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ 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 fveq2 ⊢ f = G → L ⁡ f = L ⁡ G
3 2 fveq2d ⊢ f = G → ⊥ ˙ ⁡ L ⁡ f = ⊥ ˙ ⁡ L ⁡ G
4 3 fveq2d ⊢ f = G → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G
5 4 2 eqeq12d ⊢ f = G → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
6 3 sseq1d ⊢ f = G → ⊥ ˙ ⁡ L ⁡ f ⊆ Q ↔ ⊥ ˙ ⁡ L ⁡ G ⊆ Q
7 5 6 anbi12d ⊢ f = G → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f ∧ ⊥ ˙ ⁡ L ⁡ f ⊆ Q ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q
8 7 1 elrab2 ⊢ G ∈ C ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q
9 3anass ⊢ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q
10 8 9 bitr4i ⊢ G ∈ C ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ ⊥ ˙ ⁡ L ⁡ G ⊆ Q