Theorem ofc1

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

	Ref	Expression
Hypotheses	ofc1.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofc1.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	ofc1.3	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	ofc1.4	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )
Assertion	ofc1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 𝐹 ) ‘ 𝑋 ) = ( 𝐵 𝑅 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		ofc1.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ofc1.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		ofc1.3	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
4		ofc1.4	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )
5		fnconstg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
6	2 5	syl	⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
7		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
8		fvconst2g	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = 𝐵 )
9	2 8	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = 𝐵 )
10	6 3 1 1 7 9 4	ofval	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 𝐹 ) ‘ 𝑋 ) = ( 𝐵 𝑅 𝐶 ) )