fucoisfunc2lem1

Description: Lemma for fucoisfunc2lem2 . An equivalence that expands the transformation outputs of a composition-shaped hom-family into exact component functions, component typing, and naturality. The component values are arbitrary; no canonical value is imposed. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fucoisfunc.w	⊢ 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
	fucoisfunc2lem1.o	⊢ 𝑂 = ( ∘_func ↾ 𝑊 )
	fucoisfunc2lem1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	fucoisfunc2lem1.r	⊢ 𝑅 = ( Hom ‘ 𝐶 )
	fucoisfunc2lem1.s	⊢ 𝑆 = ( Hom ‘ 𝐸 )
	fucoisfunc2lem1.v	⊢ ∙ = ( comp ‘ 𝐸 )
Assertion	fucoisfunc2lem1	⊢ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ↔ ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	⊢ 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
2		fucoisfunc2lem1.o	⊢ 𝑂 = ( ∘_func ↾ 𝑊 )
3		fucoisfunc2lem1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		fucoisfunc2lem1.r	⊢ 𝑅 = ( Hom ‘ 𝐶 )
5		fucoisfunc2lem1.s	⊢ 𝑆 = ( Hom ‘ 𝐸 )
6		fucoisfunc2lem1.v	⊢ ∙ = ( comp ‘ 𝐸 )
7		eqid	⊢ ( 𝐶 Nat 𝐸 ) = ( 𝐶 Nat 𝐸 )
8		rescofuf	⊢ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 )
9	1	reseq2i	⊢ ( ∘_func ↾ 𝑊 ) = ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
10	2 9	eqtri	⊢ 𝑂 = ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
11	10 1	feq12i	⊢ ( 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) ↔ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 ) )
12	8 11	mpbir	⊢ 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 )
13	12	a1i	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) ∧ 𝑛 ∈ 𝑊 ) → 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) )
14		simplr	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) ∧ 𝑛 ∈ 𝑊 ) → 𝑚 ∈ 𝑊 )
15	13 14	ffvelcdmd	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) ∧ 𝑛 ∈ 𝑊 ) → ( 𝑂 ‘ 𝑚 ) ∈ ( 𝐶 Func 𝐸 ) )
16		simpr	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) ∧ 𝑛 ∈ 𝑊 ) → 𝑛 ∈ 𝑊 )
17	13 16	ffvelcdmd	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) ∧ 𝑛 ∈ 𝑊 ) → ( 𝑂 ‘ 𝑛 ) ∈ ( 𝐶 Func 𝐸 ) )
18	7 3 4 5 6 15 17	isnat3	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) ∧ 𝑛 ∈ 𝑊 ) → ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ↔ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) )
19	18	2ralbidv	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) ∧ 𝑛 ∈ 𝑊 ) → ( ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ↔ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) )
20	19	anbi2d	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) ∧ 𝑛 ∈ 𝑊 ) → ( ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ↔ ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) )
21	20	ralbidva	⊢ ( ( ⊤ ∧ 𝑚 ∈ 𝑊 ) → ( ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ↔ ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) )
22	21	ralbidva	⊢ ( ⊤ → ( ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ↔ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) )
23	22	anbi2d	⊢ ( ⊤ → ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ↔ ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) ) )
24	23	mptru	⊢ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ↔ ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Theorem fucoisfunc2lem1

Proof