Metamath Proof Explorer

Theorem coof

Description: The composition of ahomomorphism with a function operation. (Contributed by SN, 20-May-2025)

Ref Expression
Hypotheses coof.f 
|- ( ph -> F : A --> B )
coof.g 
|- ( ph -> G : A --> B )
coof.h 
|- ( ph -> H Fn B )
coof.a 
|- ( ph -> A e. V )
coof.1 
|- ( ( ph /\ ( b e. B /\ c e. B ) ) -> ( b R c ) e. B )
coof.2 
|- ( ( ph /\ ( b e. B /\ c e. B ) ) -> ( H ` ( b R c ) ) = ( ( H ` b ) S ( H ` c ) ) )
Assertion coof 
|- ( ph -> ( H o. ( F oF R G ) ) = ( ( H o. F ) oF S ( H o. G ) ) )

Proof

Step Hyp Ref Expression
1 coof.f 
 |-  ( ph -> F : A --> B )
2 coof.g 
 |-  ( ph -> G : A --> B )
3 coof.h 
 |-  ( ph -> H Fn B )
4 coof.a 
 |-  ( ph -> A e. V )
5 coof.1 
 |-  ( ( ph /\ ( b e. B /\ c e. B ) ) -> ( b R c ) e. B )
6 coof.2 
 |-  ( ( ph /\ ( b e. B /\ c e. B ) ) -> ( H ` ( b R c ) ) = ( ( H ` b ) S ( H ` c ) ) )
7 1 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
8 2 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. B )
9 6 ralrimivva 
 |-  ( ph -> A. b e. B A. c e. B ( H ` ( b R c ) ) = ( ( H ` b ) S ( H ` c ) ) )
10 9 adantr 
 |-  ( ( ph /\ x e. A ) -> A. b e. B A. c e. B ( H ` ( b R c ) ) = ( ( H ` b ) S ( H ` c ) ) )
11 fvoveq1 
 |-  ( b = ( F ` x ) -> ( H ` ( b R c ) ) = ( H ` ( ( F ` x ) R c ) ) )
12 fveq2 
 |-  ( b = ( F ` x ) -> ( H ` b ) = ( H ` ( F ` x ) ) )
13 12 oveq1d 
 |-  ( b = ( F ` x ) -> ( ( H ` b ) S ( H ` c ) ) = ( ( H ` ( F ` x ) ) S ( H ` c ) ) )
14 11 13 eqeq12d 
 |-  ( b = ( F ` x ) -> ( ( H ` ( b R c ) ) = ( ( H ` b ) S ( H ` c ) ) <-> ( H ` ( ( F ` x ) R c ) ) = ( ( H ` ( F ` x ) ) S ( H ` c ) ) ) )
15 oveq2 
 |-  ( c = ( G ` x ) -> ( ( F ` x ) R c ) = ( ( F ` x ) R ( G ` x ) ) )
16 15 fveq2d 
 |-  ( c = ( G ` x ) -> ( H ` ( ( F ` x ) R c ) ) = ( H ` ( ( F ` x ) R ( G ` x ) ) ) )
17 fveq2 
 |-  ( c = ( G ` x ) -> ( H ` c ) = ( H ` ( G ` x ) ) )
18 17 oveq2d 
 |-  ( c = ( G ` x ) -> ( ( H ` ( F ` x ) ) S ( H ` c ) ) = ( ( H ` ( F ` x ) ) S ( H ` ( G ` x ) ) ) )
19 16 18 eqeq12d 
 |-  ( c = ( G ` x ) -> ( ( H ` ( ( F ` x ) R c ) ) = ( ( H ` ( F ` x ) ) S ( H ` c ) ) <-> ( H ` ( ( F ` x ) R ( G ` x ) ) ) = ( ( H ` ( F ` x ) ) S ( H ` ( G ` x ) ) ) ) )
20 14 19 rspc2va 
 |-  ( ( ( ( F ` x ) e. B /\ ( G ` x ) e. B ) /\ A. b e. B A. c e. B ( H ` ( b R c ) ) = ( ( H ` b ) S ( H ` c ) ) ) -> ( H ` ( ( F ` x ) R ( G ` x ) ) ) = ( ( H ` ( F ` x ) ) S ( H ` ( G ` x ) ) ) )
21 7 8 10 20 syl21anc 
 |-  ( ( ph /\ x e. A ) -> ( H ` ( ( F ` x ) R ( G ` x ) ) ) = ( ( H ` ( F ` x ) ) S ( H ` ( G ` x ) ) ) )
22 21 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( H ` ( ( F ` x ) R ( G ` x ) ) ) ) = ( x e. A |-> ( ( H ` ( F ` x ) ) S ( H ` ( G ` x ) ) ) ) )
23 1 ffnd 
 |-  ( ph -> F Fn A )
24 2 ffnd 
 |-  ( ph -> G Fn A )
25 inidm 
 |-  ( A i^i A ) = A
26 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
27 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
28 23 24 4 4 25 26 27 offval 
 |-  ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) )
29 28 coeq2d 
 |-  ( ph -> ( H o. ( F oF R G ) ) = ( H o. ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) ) )
30 dffn3 
 |-  ( H Fn B <-> H : B --> ran H )
31 3 30 sylib 
 |-  ( ph -> H : B --> ran H )
32 7 8 jca 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) e. B /\ ( G ` x ) e. B ) )
33 5 caovclg 
 |-  ( ( ph /\ ( ( F ` x ) e. B /\ ( G ` x ) e. B ) ) -> ( ( F ` x ) R ( G ` x ) ) e. B )
34 32 33 syldan 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) R ( G ` x ) ) e. B )
35 31 34 cofmpt 
 |-  ( ph -> ( H o. ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) ) = ( x e. A |-> ( H ` ( ( F ` x ) R ( G ` x ) ) ) ) )
36 29 35 eqtrd 
 |-  ( ph -> ( H o. ( F oF R G ) ) = ( x e. A |-> ( H ` ( ( F ` x ) R ( G ` x ) ) ) ) )
37 fnfco 
 |-  ( ( H Fn B /\ F : A --> B ) -> ( H o. F ) Fn A )
38 3 1 37 syl2anc 
 |-  ( ph -> ( H o. F ) Fn A )
39 fnfco 
 |-  ( ( H Fn B /\ G : A --> B ) -> ( H o. G ) Fn A )
40 3 2 39 syl2anc 
 |-  ( ph -> ( H o. G ) Fn A )
41 fvco2 
 |-  ( ( F Fn A /\ x e. A ) -> ( ( H o. F ) ` x ) = ( H ` ( F ` x ) ) )
42 23 41 sylan 
 |-  ( ( ph /\ x e. A ) -> ( ( H o. F ) ` x ) = ( H ` ( F ` x ) ) )
43 fvco2 
 |-  ( ( G Fn A /\ x e. A ) -> ( ( H o. G ) ` x ) = ( H ` ( G ` x ) ) )
44 24 43 sylan 
 |-  ( ( ph /\ x e. A ) -> ( ( H o. G ) ` x ) = ( H ` ( G ` x ) ) )
45 38 40 4 4 25 42 44 offval 
 |-  ( ph -> ( ( H o. F ) oF S ( H o. G ) ) = ( x e. A |-> ( ( H ` ( F ` x ) ) S ( H ` ( G ` x ) ) ) ) )
46 22 36 45 3eqtr4d 
 |-  ( ph -> ( H o. ( F oF R G ) ) = ( ( H o. F ) oF S ( H o. G ) ) )