comfeq

Description: Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	comfeq.1	⊢ · = ( comp ‘ 𝐶 )
	comfeq.2	⊢ ∙ = ( comp ‘ 𝐷 )
	comfeq.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	comfeq.3	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	comfeq.4	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
	comfeq.5	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
Assertion	comfeq	⊢ ( 𝜑 → ( ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		comfeq.1	⊢ · = ( comp ‘ 𝐶 )
2		comfeq.2	⊢ ∙ = ( comp ‘ 𝐷 )
3		comfeq.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		comfeq.3	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
5		comfeq.4	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
6		comfeq.5	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
7	4	sqxpeqd	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
8		eqidd	⊢ ( 𝜑 → ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) )
9	7 4 8	mpoeq123dv	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ) )
10		eqid	⊢ ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐶 )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12	10 11 3 1	comfffval	⊢ ( comp_f ‘ 𝐶 ) = ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) )
13	9 12	eqtr4di	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ) = ( comp_f ‘ 𝐶 ) )
14		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
15	6	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
16		xp2nd	⊢ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) → ( 2^nd ‘ 𝑢 ) ∈ 𝐵 )
17	16	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 2^nd ‘ 𝑢 ) ∈ 𝐵 )
18	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝐶 ) )
19	17 18	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 2^nd ‘ 𝑢 ) ∈ ( Base ‘ 𝐶 ) )
20		simp3	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
21	20 18	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
22	11 3 14 15 19 21	homfeqval	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) = ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) )
23		xp1st	⊢ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) → ( 1^st ‘ 𝑢 ) ∈ 𝐵 )
24	23	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 1^st ‘ 𝑢 ) ∈ 𝐵 )
25	24 18	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 1^st ‘ 𝑢 ) ∈ ( Base ‘ 𝐶 ) )
26	11 3 14 15 25 19	homfeqval	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 1^st ‘ 𝑢 ) 𝐻 ( 2^nd ‘ 𝑢 ) ) = ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) )
27		df-ov	⊢ ( ( 1^st ‘ 𝑢 ) 𝐻 ( 2^nd ‘ 𝑢 ) ) = ( 𝐻 ‘ ⟨ ( 1^st ‘ 𝑢 ) , ( 2^nd ‘ 𝑢 ) ⟩ )
28		df-ov	⊢ ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ 𝑢 ) , ( 2^nd ‘ 𝑢 ) ⟩ )
29	26 27 28	3eqtr3g	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐻 ‘ ⟨ ( 1^st ‘ 𝑢 ) , ( 2^nd ‘ 𝑢 ) ⟩ ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ 𝑢 ) , ( 2^nd ‘ 𝑢 ) ⟩ ) )
30		1st2nd2	⊢ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) → 𝑢 = ⟨ ( 1^st ‘ 𝑢 ) , ( 2^nd ‘ 𝑢 ) ⟩ )
31	30	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑢 = ⟨ ( 1^st ‘ 𝑢 ) , ( 2^nd ‘ 𝑢 ) ⟩ )
32	31	fveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ ⟨ ( 1^st ‘ 𝑢 ) , ( 2^nd ‘ 𝑢 ) ⟩ ) )
33	31	fveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ 𝑢 ) , ( 2^nd ‘ 𝑢 ) ⟩ ) )
34	29 32 33	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐻 ‘ 𝑢 ) = ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) )
35		eqidd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) = ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) )
36	22 34 35	mpoeq123dv	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) , 𝑓 ∈ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) )
37	36	mpoeq3dva	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) = ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) , 𝑓 ∈ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) )
38	5	sqxpeqd	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
39		eqidd	⊢ ( 𝜑 → ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) , 𝑓 ∈ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) , 𝑓 ∈ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) )
40	38 5 39	mpoeq123dv	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) , 𝑓 ∈ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) , 𝑓 ∈ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) )
41	37 40	eqtrd	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) , 𝑓 ∈ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) )
42		eqid	⊢ ( comp_f ‘ 𝐷 ) = ( comp_f ‘ 𝐷 )
43		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
44	42 43 14 2	comfffval	⊢ ( comp_f ‘ 𝐷 ) = ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) 𝑧 ) , 𝑓 ∈ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) )
45	41 44	eqtr4di	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) = ( comp_f ‘ 𝐷 ) )
46	13 45	eqeq12d	⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ) = ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) ↔ ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) ) )
47		ovex	⊢ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) ∈ V
48		fvex	⊢ ( 𝐻 ‘ 𝑢 ) ∈ V
49	47 48	mpoex	⊢ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ∈ V
50	49	rgen2w	⊢ ∀ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ∈ V
51		mpo2eqb	⊢ ( ∀ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ∈ V → ( ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ) = ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) )
52	50 51	ax-mp	⊢ ( ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ) = ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) )
53		vex	⊢ 𝑥 ∈ V
54		vex	⊢ 𝑦 ∈ V
55	53 54	op2ndd	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑢 ) = 𝑦 )
56	55	oveq1d	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) = ( 𝑦 𝐻 𝑧 ) )
57		fveq2	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
58		df-ov	⊢ ( 𝑥 𝐻 𝑦 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
59	57 58	eqtr4di	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑢 ) = ( 𝑥 𝐻 𝑦 ) )
60		oveq1	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑢 · 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) )
61	60	oveqd	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) )
62		oveq1	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑢 ∙ 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) )
63	62	oveqd	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
64	61 63	eqeq12d	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) = ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
65	59 64	raleqbidv	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) = ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ↔ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
66	56 65	raleqbidv	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) ∀ 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) = ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ↔ ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
67		ovex	⊢ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ∈ V
68	67	rgen2w	⊢ ∀ 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) ∀ 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ∈ V
69		mpo2eqb	⊢ ( ∀ 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) ∀ 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ∈ V → ( ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) ∀ 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) = ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) )
70	68 69	ax-mp	⊢ ( ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) ∀ 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) = ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) )
71		ralcom	⊢ ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ↔ ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
72	66 70 71	3bitr4g	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
73	72	ralbidv	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
74	73	ralxp	⊢ ( ∀ 𝑢 ∈ ( 𝐵 × 𝐵 ) ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
75	52 74	bitri	⊢ ( ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 · 𝑧 ) 𝑓 ) ) ) = ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑢 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑢 ) ↦ ( 𝑔 ( 𝑢 ∙ 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
76	46 75	bitr3di	⊢ ( 𝜑 → ( ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )

Metamath Proof Explorer

Theorem comfeq

Proof