Metamath Proof Explorer

Theorem ofc1

Description: Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses ofc1.1 ${⊢}{\phi }\to {A}\in {V}$
ofc1.2 ${⊢}{\phi }\to {B}\in {W}$
ofc1.3 ${⊢}{\phi }\to {F}Fn{A}$
ofc1.4 ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to {F}\left({X}\right)={C}$
Assertion ofc1 ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to \left(\left({A}×\left\{{B}\right\}\right){{R}}_{f}{F}\right)\left({X}\right)={B}{R}{C}$

Proof

Step Hyp Ref Expression
1 ofc1.1 ${⊢}{\phi }\to {A}\in {V}$
2 ofc1.2 ${⊢}{\phi }\to {B}\in {W}$
3 ofc1.3 ${⊢}{\phi }\to {F}Fn{A}$
4 ofc1.4 ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to {F}\left({X}\right)={C}$
5 fnconstg ${⊢}{B}\in {W}\to \left({A}×\left\{{B}\right\}\right)Fn{A}$
6 2 5 syl ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right)Fn{A}$
7 inidm ${⊢}{A}\cap {A}={A}$
8 fvconst2g ${⊢}\left({B}\in {W}\wedge {X}\in {A}\right)\to \left({A}×\left\{{B}\right\}\right)\left({X}\right)={B}$
9 2 8 sylan ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to \left({A}×\left\{{B}\right\}\right)\left({X}\right)={B}$
10 6 3 1 1 7 9 4 ofval ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to \left(\left({A}×\left\{{B}\right\}\right){{R}}_{f}{F}\right)\left({X}\right)={B}{R}{C}$