Theorem ofc12

Description: Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ofc12.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ofc12.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		ofc12.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
4	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
6		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	6	a1i	⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
8		fconstmpt	⊢ ( 𝐴 × { 𝐶 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
9	8	a1i	⊢ ( 𝜑 → ( 𝐴 × { 𝐶 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
10	1 4 5 7 9	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 ( 𝐴 × { 𝐶 } ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
11		fconstmpt	⊢ ( 𝐴 × { ( 𝐵 𝑅 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) )
12	10 11	eqtr4di	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 ( 𝐴 × { 𝐶 } ) ) = ( 𝐴 × { ( 𝐵 𝑅 𝐶 ) } ) )