Description: Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lcfl1.c | ⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } | |
Assertion | lcfl1lem | ⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcfl1.c | ⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } | |
2 | fveq2 | ⊢ ( 𝑓 = 𝐺 → ( 𝐿 ‘ 𝑓 ) = ( 𝐿 ‘ 𝐺 ) ) | |
3 | 2 | fveq2d | ⊢ ( 𝑓 = 𝐺 → ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) |
4 | 3 | fveq2d | ⊢ ( 𝑓 = 𝐺 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) |
5 | 4 2 | eqeq12d | ⊢ ( 𝑓 = 𝐺 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) ) |
6 | 5 1 | elrab2 | ⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) ) |