Metamath Proof Explorer

Theorem caofcan

Description: Transfer a cancellation law like mulcan to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015)

Ref Expression
Hypotheses caofcan.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
caofcan.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑇 )
caofcan.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
caofcan.4 ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝑆 )
caofcan.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 𝑅 𝑦 ) = ( 𝑥 𝑅 𝑧 ) ↔ 𝑦 = 𝑧 ) )
Assertion caofcan ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐹 ∘f 𝑅 𝐻 ) ↔ 𝐺 = 𝐻 ) )

Proof

Step Hyp Ref Expression
1 caofcan.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 caofcan.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑇 )
3 caofcan.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
4 caofcan.4 ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝑆 )
5 caofcan.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 𝑅 𝑦 ) = ( 𝑥 𝑅 𝑧 ) ↔ 𝑦 = 𝑧 ) )
6 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
7 3 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
8 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
9 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
10 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
11 6 7 1 1 8 9 10 ofval ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) )
12 4 ffnd ⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
13 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) )
14 6 12 1 1 8 9 13 ofval ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) )
15 11 14 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ 𝑤 ) ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) ) )
16 simpl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 𝜑 )
17 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑇 )
18 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
19 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑤 ) ∈ 𝑆 )
20 5 caovcang ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑇 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐻 ‘ 𝑤 ) ∈ 𝑆 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) ↔ ( 𝐺 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) ) )
21 16 17 18 19 20 syl13anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) ↔ ( 𝐺 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) ) )
22 15 21 bitrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ 𝑤 ) ↔ ( 𝐺 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) ) )
23 22 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐺 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) ) )
24 6 7 1 1 8 offn ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) Fn 𝐴 )
25 6 12 1 1 8 offn ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐻 ) Fn 𝐴 )
26 eqfnfv ⊢ ( ( ( 𝐹 ∘f 𝑅 𝐺 ) Fn 𝐴 ∧ ( 𝐹 ∘f 𝑅 𝐻 ) Fn 𝐴 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐹 ∘f 𝑅 𝐻 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ 𝑤 ) ) )
27 24 25 26 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐹 ∘f 𝑅 𝐻 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ 𝑤 ) ) )
28 eqfnfv ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐻 Fn 𝐴 ) → ( 𝐺 = 𝐻 ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐺 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) ) )
29 7 12 28 syl2anc ⊢ ( 𝜑 → ( 𝐺 = 𝐻 ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐺 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) ) )
30 23 27 29 3bitr4d ⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐹 ∘f 𝑅 𝐻 ) ↔ 𝐺 = 𝐻 ) )