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