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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
coof.g ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
coof.h ⊢ ( 𝜑 → 𝐻 Fn 𝐵 )
coof.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
coof.1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑏 𝑅 𝑐 ) ∈ 𝐵 )
coof.2 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝐻 ‘ ( 𝑏 𝑅 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
Assertion coof ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ∘f 𝑅 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∘f 𝑆 ( 𝐻 ∘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 coof.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 coof.g ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
3 coof.h ⊢ ( 𝜑 → 𝐻 Fn 𝐵 )
4 coof.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 coof.1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑏 𝑅 𝑐 ) ∈ 𝐵 )
6 coof.2 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝐻 ‘ ( 𝑏 𝑅 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
7 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
8 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐵 )
9 6 ralrimivva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑏 𝑅 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑏 𝑅 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
11 fvoveq1 ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑥 ) → ( 𝐻 ‘ ( 𝑏 𝑅 𝑐 ) ) = ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝑐 ) ) )
12 fveq2 ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑥 ) → ( 𝐻 ‘ 𝑏 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) )
13 12 oveq1d ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
14 11 13 eqeq12d ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐻 ‘ ( 𝑏 𝑅 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝑐 ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) ) )
15 oveq2 ⊢ ( 𝑐 = ( 𝐺 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝑐 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
16 15 fveq2d ⊢ ( 𝑐 = ( 𝐺 ‘ 𝑥 ) → ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝑐 ) ) = ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
17 fveq2 ⊢ ( 𝑐 = ( 𝐺 ‘ 𝑥 ) → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) )
18 17 oveq2d ⊢ ( 𝑐 = ( 𝐺 ‘ 𝑥 ) → ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
19 16 18 eqeq12d ⊢ ( 𝑐 = ( 𝐺 ‘ 𝑥 ) → ( ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝑐 ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
20 14 19 rspc2va ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑏 𝑅 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) ) → ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
21 7 8 10 20 syl21anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
22 21 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
23 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
24 2 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
25 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
26 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
27 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
28 23 24 4 4 25 26 27 offval ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
29 28 coeq2d ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ∘f 𝑅 𝐺 ) ) = ( 𝐻 ∘ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ) )
30 dffn3 ⊢ ( 𝐻 Fn 𝐵 ↔ 𝐻 : 𝐵 ⟶ ran 𝐻 )
31 3 30 sylib ⊢ ( 𝜑 → 𝐻 : 𝐵 ⟶ ran 𝐻 )
32 7 8 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐵 ) )
33 5 caovclg ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐵 )
34 32 33 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐵 )
35 31 34 cofmpt ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ) )
36 29 35 eqtrd ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ∘f 𝑅 𝐺 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ) )
37 fnfco ⊢ ( ( 𝐻 Fn 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐻 ∘ 𝐹 ) Fn 𝐴 )
38 3 1 37 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) Fn 𝐴 )
39 fnfco ⊢ ( ( 𝐻 Fn 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐻 ∘ 𝐺 ) Fn 𝐴 )
40 3 2 39 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) Fn 𝐴 )
41 fvco2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) )
42 23 41 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) )
43 fvco2 ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) )
44 24 43 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) )
45 38 40 4 4 25 42 44 offval ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ∘f 𝑆 ( 𝐻 ∘ 𝐺 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐻 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
46 22 36 45 3eqtr4d ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ∘f 𝑅 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∘f 𝑆 ( 𝐻 ∘ 𝐺 ) ) )