fucidcobi

Description: Componentwise functor laws for a correctly typed hom-family into a functor category. The source category T and object assignment O are arbitrary: the identity and composition laws are equivalent to their component equations. No functor law is assumed in the hypotheses. Functor composition is an application in fucoisfunc2 . (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fucidcobi.w	⊢ 𝑊 = ( Base ‘ 𝑇 )
	fucidcobi.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucidcobi.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	fucidcobi.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
	fucidcobi.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
	fucidcobi.j	⊢ 𝐽 = ( Id ‘ 𝑄 )
	fucidcobi.k	⊢ 𝐾 = ( Id ‘ 𝐸 )
	fucidcobi.x	⊢ · = ( comp ‘ 𝑇 )
	fucidcobi.y	⊢ ⚬ = ( comp ‘ 𝑄 )
	fucidcobi.v	⊢ ∙ = ( comp ‘ 𝐸 )
	fucidcobi.c	⊢ ( 𝜑 → 𝑇 ∈ Cat )
	fucidcobi.p	⊢ ( 𝜑 → 𝑃 ∈ X 𝑣 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑣 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑣 ) ) ) ↑_m ( 𝐻 ‘ 𝑣 ) ) )
Assertion	fucidcobi	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucidcobi.w	⊢ 𝑊 = ( Base ‘ 𝑇 )
2		fucidcobi.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
3		fucidcobi.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		fucidcobi.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
5		fucidcobi.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
6		fucidcobi.j	⊢ 𝐽 = ( Id ‘ 𝑄 )
7		fucidcobi.k	⊢ 𝐾 = ( Id ‘ 𝐸 )
8		fucidcobi.x	⊢ · = ( comp ‘ 𝑇 )
9		fucidcobi.y	⊢ ⚬ = ( comp ‘ 𝑄 )
10		fucidcobi.v	⊢ ∙ = ( comp ‘ 𝐸 )
11		fucidcobi.c	⊢ ( 𝜑 → 𝑇 ∈ Cat )
12		fucidcobi.p	⊢ ( 𝜑 → 𝑃 ∈ X 𝑣 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑣 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑣 ) ) ) ↑_m ( 𝐻 ‘ 𝑣 ) ) )
13		eqid	⊢ ( 𝐶 Nat 𝐸 ) = ( 𝐶 Nat 𝐸 )
14	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → 𝑃 ∈ X 𝑣 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑣 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑣 ) ) ) ↑_m ( 𝐻 ‘ 𝑣 ) ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → 𝑥 ∈ 𝑊 )
16	14 15 15	ixpovf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 𝑃 𝑥 ) : ( 𝑥 𝐻 𝑥 ) ⟶ ( ( 𝑂 ‘ 𝑥 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑥 ) ) )
17	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → 𝑇 ∈ Cat )
18	1 4 5 17 15	catidcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( 𝐼 ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )
19	16 18	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ ( ( 𝑂 ‘ 𝑥 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑥 ) ) )
20	2 13 3 6 7 19	natideq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ↔ ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ) )
21		simpl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) )
22	21	simpld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) )
23	22	simpld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) )
24	23	simpld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) )
25	24	simpld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝜑 )
26	25 12	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑃 ∈ X 𝑣 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑣 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑣 ) ) ) ↑_m ( 𝐻 ‘ 𝑣 ) ) )
27	24	simprd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑥 ∈ 𝑊 )
28	23	simprd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑦 ∈ 𝑊 )
29	26 27 28	ixpovf	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑥 𝑃 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝑂 ‘ 𝑥 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑦 ) ) )
30	21	simprd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) )
31	29 30	ffvelcdmd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ∈ ( ( 𝑂 ‘ 𝑥 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑦 ) ) )
32	22	simprd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑧 ∈ 𝑊 )
33	26 28 32	ixpovf	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑦 𝑃 𝑧 ) : ( 𝑦 𝐻 𝑧 ) ⟶ ( ( 𝑂 ‘ 𝑦 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑧 ) ) )
34		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) )
35	33 34	ffvelcdmd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ∈ ( ( 𝑂 ‘ 𝑦 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑧 ) ) )
36	26 27 32	ixpovf	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑥 𝑃 𝑧 ) : ( 𝑥 𝐻 𝑧 ) ⟶ ( ( 𝑂 ‘ 𝑥 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑧 ) ) )
37	25 11	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑇 ∈ Cat )
38	1 4 8 37 27 28 32 30 34	catcocl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ∈ ( 𝑥 𝐻 𝑧 ) )
39	36 38	ffvelcdmd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ∈ ( ( 𝑂 ‘ 𝑥 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑧 ) ) )
40	2 13 3 10 9 31 35 39	natcoeq	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) )
41	40	ralbidva	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ) → ( ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) )
42	41	ralbidva	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) → ( ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) )
43	42	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑊 ) → ( ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) )
44	43	ralbidva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) )
45	20 44	anbi12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ↔ ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) )
46	45	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) )

Metamath Proof Explorer

Theorem fucidcobi

Proof