Theorem ofcc

Description: Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcc.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofcc.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	ofcc.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
Assertion	ofcc	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f/c 𝑅 𝐶 ) = ( 𝐴 × { ( 𝐵 𝑅 𝐶 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		ofcc.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ofcc.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		ofcc.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
4		fnconstg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
5	2 4	syl	⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
6		fvconst2g	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑥 ) = 𝐵 )
7	2 6	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑥 ) = 𝐵 )
8	5 1 3 7	ofcfval	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
9		fconstmpt	⊢ ( 𝐴 × { ( 𝐵 𝑅 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) )
10	8 9	eqtr4di	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f/c 𝑅 𝐶 ) = ( 𝐴 × { ( 𝐵 𝑅 𝐶 ) } ) )