caofid2

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	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	caofid2.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐵 𝑅 𝑥 ) = 𝐶 )
Assertion	caofid2	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘_f 𝑅 𝐹 ) = ( 𝐴 × { 𝐶 } ) )

Proof

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

Metamath Proof Explorer

Theorem caofid2

Proof