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 φ F : A B
coof.g φ G : A B
coof.h φ H Fn B
coof.a φ A V
coof.1 φ b B c B b R c B
coof.2 φ b B c B H b R c = H b S H c
Assertion coof φ H F R f G = H F S f H G

Proof

Step Hyp Ref Expression
1 coof.f φ F : A B
2 coof.g φ G : A B
3 coof.h φ H Fn B
4 coof.a φ A V
5 coof.1 φ b B c B b R c B
6 coof.2 φ b B c B H b R c = H b S H c
7 1 ffvelcdmda φ x A F x B
8 2 ffvelcdmda φ x A G x B
9 6 ralrimivva φ b B c B H b R c = H b S H c
10 9 adantr φ x A b B c 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 B G x B b B c 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 φ x A H F x R G x = H F x S H G x
22 21 mpteq2dva φ x A H F x R G x = x A H F x S H G x
23 1 ffnd φ F Fn A
24 2 ffnd φ G Fn A
25 inidm A A = A
26 eqidd φ x A F x = F x
27 eqidd φ x A G x = G x
28 23 24 4 4 25 26 27 offval φ F R f G = x A F x R G x
29 28 coeq2d φ H F R f G = H x A F x R G x
30 dffn3 H Fn B H : B ran H
31 3 30 sylib φ H : B ran H
32 7 8 jca φ x A F x B G x B
33 5 caovclg φ F x B G x B F x R G x B
34 32 33 syldan φ x A F x R G x B
35 31 34 cofmpt φ H x A F x R G x = x A H F x R G x
36 29 35 eqtrd φ H F R f G = x A H F x R G x
37 fnfco H Fn B F : A B H F Fn A
38 3 1 37 syl2anc φ H F Fn A
39 fnfco H Fn B G : A B H G Fn A
40 3 2 39 syl2anc φ H G Fn A
41 fvco2 F Fn A x A H F x = H F x
42 23 41 sylan φ x A H F x = H F x
43 fvco2 G Fn A x A H G x = H G x
44 24 43 sylan φ x A H G x = H G x
45 38 40 4 4 25 42 44 offval φ H F S f H G = x A H F x S H G x
46 22 36 45 3eqtr4d φ H F R f G = H F S f H G