Metamath Proof Explorer


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 𝑅 𝐹 ) = 𝐹 )