Theorem caofid1

Description: Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	caofid0.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	caofid1.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	caofid1.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 𝑅 𝐵 ) = 𝐶 )
Assertion	caofid1	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 ( 𝐴 × { 𝐵 } ) ) = ( 𝐴 × { 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3		caofid0.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		caofid1.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
5		caofid1.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 𝑅 𝐵 ) = 𝐶 )
6	2	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
7		fnconstg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
8	3 7	syl	⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
9		fnconstg	⊢ ( 𝐶 ∈ 𝑋 → ( 𝐴 × { 𝐶 } ) Fn 𝐴 )
10	4 9	syl	⊢ ( 𝜑 → ( 𝐴 × { 𝐶 } ) Fn 𝐴 )
11		eqidd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
12		fvconst2g	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
13	3 12	sylan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
14	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝑥 𝑅 𝐵 ) = 𝐶 )
15	2	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
16		oveq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑅 𝐵 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) )
17	16	eqeq1d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑥 𝑅 𝐵 ) = 𝐶 ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = 𝐶 ) )
18	17	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑆 ( 𝑥 𝑅 𝐵 ) = 𝐶 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = 𝐶 )
19	14 15 18	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = 𝐶 )
20		fvconst2g	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐶 } ) ‘ 𝑤 ) = 𝐶 )
21	4 20	sylan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐶 } ) ‘ 𝑤 ) = 𝐶 )
22	19 21	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = ( ( 𝐴 × { 𝐶 } ) ‘ 𝑤 ) )
23	1 6 8 10 11 13 22	offveq	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 ( 𝐴 × { 𝐵 } ) ) = ( 𝐴 × { 𝐶 } ) )