Theorem caofid0l

Description: Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3		caofid0.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		caofid0l.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐵 𝑅 𝑥 ) = 𝑥 )
5		fnconstg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
6	3 5	syl	⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
7	2	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
8		fvconst2g	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
9	3 8	sylan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
10		eqidd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
11	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝐵 𝑅 𝑥 ) = 𝑥 )
12	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
13		oveq2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝐵 𝑅 𝑥 ) = ( 𝐵 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
14		id	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → 𝑥 = ( 𝐹 ‘ 𝑤 ) )
15	13 14	eqeq12d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝐵 𝑅 𝑥 ) = 𝑥 ↔ ( 𝐵 𝑅 ( 𝐹 ‘ 𝑤 ) ) = ( 𝐹 ‘ 𝑤 ) ) )
16	15	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑆 ( 𝐵 𝑅 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ) → ( 𝐵 𝑅 ( 𝐹 ‘ 𝑤 ) ) = ( 𝐹 ‘ 𝑤 ) )
17	11 12 16	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐵 𝑅 ( 𝐹 ‘ 𝑤 ) ) = ( 𝐹 ‘ 𝑤 ) )
18	1 6 7 7 9 10 17	offveq	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 𝐹 ) = 𝐹 )