Theorem ofc2

Description: Right operation by a constant. (Contributed by NM, 7-Oct-2014)

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

Proof

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