Metamath Proof Explorer

Theorem fvcofneq

Description: The values of two function compositions are equal if the values of the composed functions are pairwise equal. (Contributed by AV, 26-Jan-2019)

Ref Expression
Assertion fvcofneq ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐻 ∘ 𝐾 ) ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → 𝐺 Fn 𝐴 )
2 elinel1 ⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑋 ∈ 𝐴 )
3 2 3ad2ant1 ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) → 𝑋 ∈ 𝐴 )
4 fvco2 ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
5 1 3 4 syl2an ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) ∧ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
6 simpr ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → 𝐾 Fn 𝐵 )
7 elinel2 ⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑋 ∈ 𝐵 )
8 7 3ad2ant1 ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) → 𝑋 ∈ 𝐵 )
9 fvco2 ⊢ ( ( 𝐾 Fn 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐻 ∘ 𝐾 ) ‘ 𝑋 ) = ( 𝐻 ‘ ( 𝐾 ‘ 𝑋 ) ) )
10 6 8 9 syl2an ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) ∧ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝐻 ∘ 𝐾 ) ‘ 𝑋 ) = ( 𝐻 ‘ ( 𝐾 ‘ 𝑋 ) ) )
11 fveq2 ⊢ ( ( 𝐾 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) → ( 𝐻 ‘ ( 𝐾 ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) )
12 11 eqcoms ⊢ ( ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) → ( 𝐻 ‘ ( 𝐾 ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) )
13 12 3ad2ant2 ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) → ( 𝐻 ‘ ( 𝐾 ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) )
14 13 adantl ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) ∧ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝐻 ‘ ( 𝐾 ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) )
15 id ⊢ ( 𝐺 Fn 𝐴 → 𝐺 Fn 𝐴 )
16 fnfvelrn ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 )
17 15 2 16 syl2anr ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ 𝐺 Fn 𝐴 ) → ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 )
18 17 ex ⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) → ( 𝐺 Fn 𝐴 → ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 ) )
19 id ⊢ ( 𝐾 Fn 𝐵 → 𝐾 Fn 𝐵 )
20 fnfvelrn ⊢ ( ( 𝐾 Fn 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ‘ 𝑋 ) ∈ ran 𝐾 )
21 19 7 20 syl2anr ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ 𝐾 Fn 𝐵 ) → ( 𝐾 ‘ 𝑋 ) ∈ ran 𝐾 )
22 21 ex ⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) → ( 𝐾 Fn 𝐵 → ( 𝐾 ‘ 𝑋 ) ∈ ran 𝐾 ) )
23 18 22 anim12d ⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) → ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → ( ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 ∧ ( 𝐾 ‘ 𝑋 ) ∈ ran 𝐾 ) ) )
24 eleq1 ⊢ ( ( 𝐾 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) → ( ( 𝐾 ‘ 𝑋 ) ∈ ran 𝐾 ↔ ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐾 ) )
25 24 eqcoms ⊢ ( ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) → ( ( 𝐾 ‘ 𝑋 ) ∈ ran 𝐾 ↔ ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐾 ) )
26 25 anbi2d ⊢ ( ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 ∧ ( 𝐾 ‘ 𝑋 ) ∈ ran 𝐾 ) ↔ ( ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐾 ) ) )
27 elin ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∩ ran 𝐾 ) ↔ ( ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐾 ) )
28 27 biimpri ⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐾 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∩ ran 𝐾 ) )
29 26 28 biimtrdi ⊢ ( ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 ∧ ( 𝐾 ‘ 𝑋 ) ∈ ran 𝐾 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∩ ran 𝐾 ) ) )
30 23 29 sylan9 ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ) → ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∩ ran 𝐾 ) ) )
31 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
32 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) )
33 31 32 eqeq12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
34 33 rspcva ⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∩ ran 𝐾 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) )
35 34 eqcomd ⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∩ ran 𝐾 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) → ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
36 35 ex ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∩ ran 𝐾 ) → ( ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) → ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
37 30 36 syl6 ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ) → ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → ( ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) → ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) )
38 37 com23 ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) → ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) )
39 38 3impia ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) → ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
40 39 impcom ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) ∧ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝐻 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
41 10 14 40 3eqtrrd ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) ∧ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( ( 𝐻 ∘ 𝐾 ) ‘ 𝑋 ) )
42 5 41 eqtrd ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) ∧ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐻 ∘ 𝐾 ) ‘ 𝑋 ) )
43 42 ex ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵 ) → ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐻 ∘ 𝐾 ) ‘ 𝑋 ) ) )