fucocolem2

Description: Lemma for fucoco . The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-Oct-2025)

	Ref	Expression
Hypotheses	fucoco.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) )
	fucoco.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) )
	fucoco.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
	fucoco.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
	fucoco.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fucoco.x	⊢ ( 𝜑 → 𝑋 = ⟨ 𝐹 , 𝐺 ⟩ )
	fucoco.y	⊢ ( 𝜑 → 𝑌 = ⟨ 𝐾 , 𝐿 ⟩ )
	fucoco.z	⊢ ( 𝜑 → 𝑍 = ⟨ 𝑀 , 𝑁 ⟩ )
	fucoco.a	⊢ ( 𝜑 → 𝐴 = ⟨ 𝑅 , 𝑆 ⟩ )
	fucoco.b	⊢ ( 𝜑 → 𝐵 = ⟨ 𝑈 , 𝑉 ⟩ )
	fucocolem2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
	fucocolem2.ot	⊢ · = ( comp ‘ 𝑇 )
	fucocolem2.od	⊢ ∗ = ( comp ‘ 𝐷 )
Assertion	fucocolem2	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoco.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) )
2		fucoco.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) )
3		fucoco.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
4		fucoco.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
5		fucoco.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
6		fucoco.x	⊢ ( 𝜑 → 𝑋 = ⟨ 𝐹 , 𝐺 ⟩ )
7		fucoco.y	⊢ ( 𝜑 → 𝑌 = ⟨ 𝐾 , 𝐿 ⟩ )
8		fucoco.z	⊢ ( 𝜑 → 𝑍 = ⟨ 𝑀 , 𝑁 ⟩ )
9		fucoco.a	⊢ ( 𝜑 → 𝐴 = ⟨ 𝑅 , 𝑆 ⟩ )
10		fucoco.b	⊢ ( 𝜑 → 𝐵 = ⟨ 𝑈 , 𝑉 ⟩ )
11		fucocolem2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
12		fucocolem2.ot	⊢ · = ( comp ‘ 𝑇 )
13		fucocolem2.od	⊢ ∗ = ( comp ‘ 𝐷 )
14	6 7	opeq12d	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ = ⟨ ⟨ 𝐹 , 𝐺 ⟩ , ⟨ 𝐾 , 𝐿 ⟩ ⟩ )
15	14 8	oveq12d	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( ⟨ ⟨ 𝐹 , 𝐺 ⟩ , ⟨ 𝐾 , 𝐿 ⟩ ⟩ · ⟨ 𝑀 , 𝑁 ⟩ ) )
16	15 10 9	oveq123d	⊢ ( 𝜑 → ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) = ( ⟨ 𝑈 , 𝑉 ⟩ ( ⟨ ⟨ 𝐹 , 𝐺 ⟩ , ⟨ 𝐾 , 𝐿 ⟩ ⟩ · ⟨ 𝑀 , 𝑁 ⟩ ) ⟨ 𝑅 , 𝑆 ⟩ ) )
17		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
19		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
20	11 12 1 2 3 4 17 18 19 13	xpcfucco3	⊢ ( 𝜑 → ( ⟨ 𝑈 , 𝑉 ⟩ ( ⟨ ⟨ 𝐹 , 𝐺 ⟩ , ⟨ 𝐾 , 𝐿 ⟩ ⟩ · ⟨ 𝑀 , 𝑁 ⟩ ) ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) , ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ⟩ )
21	16 20	eqtrd	⊢ ( 𝜑 → ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) = ⟨ ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) , ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ⟩ )
22	21	fveq2d	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( ( 𝑋 𝑃 𝑍 ) ‘ ⟨ ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) , ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ⟩ ) )
23		df-ov	⊢ ( ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ( 𝑋 𝑃 𝑍 ) ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ) = ( ( 𝑋 𝑃 𝑍 ) ‘ ⟨ ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) , ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ⟩ )
24	22 23	eqtr4di	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ( 𝑋 𝑃 𝑍 ) ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ) )
25	11 12 1 2 3 4	xpcfuccocl	⊢ ( 𝜑 → ( ⟨ 𝑈 , 𝑉 ⟩ ( ⟨ ⟨ 𝐹 , 𝐺 ⟩ , ⟨ 𝐾 , 𝐿 ⟩ ⟩ · ⟨ 𝑀 , 𝑁 ⟩ ) ⟨ 𝑅 , 𝑆 ⟩ ) ∈ ( ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝑀 ) × ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝑁 ) ) )
26	20 25	eqeltrrd	⊢ ( 𝜑 → ⟨ ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) , ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ⟩ ∈ ( ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝑀 ) × ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝑁 ) ) )
27		opelxp2	⊢ ( ⟨ ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) , ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ⟩ ∈ ( ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝑀 ) × ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝑁 ) ) → ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
28	26 27	syl	⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
29		opelxp1	⊢ ( ⟨ ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) , ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ⟩ ∈ ( ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝑀 ) × ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝑁 ) ) → ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
30	26 29	syl	⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
31	5 6 8 28 30	fuco22a	⊢ ( 𝜑 → ( ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ( 𝑋 𝑃 𝑍 ) ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ‘ 𝑥 ) ) ) ) )
32		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
33		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
34	33	natrcl	⊢ ( 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
35	4 34	syl	⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
36	35	simprd	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐶 Func 𝐷 ) )
37		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
38	32 36 37	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
39	18 17 38	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
40	39	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
41		fveq2	⊢ ( 𝑝 = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) = ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
42		fveq2	⊢ ( 𝑝 = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) = ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
43	41 42	opeq12d	⊢ ( 𝑝 = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) → ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ )
44		fveq2	⊢ ( 𝑝 = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) → ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) = ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
45	43 44	oveq12d	⊢ ( 𝑝 = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) → ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) )
46		fveq2	⊢ ( 𝑝 = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) → ( 𝑈 ‘ 𝑝 ) = ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
47		fveq2	⊢ ( 𝑝 = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) → ( 𝑅 ‘ 𝑝 ) = ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
48	45 46 47	oveq123d	⊢ ( 𝑝 = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) → ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) )
49		eqid	⊢ ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) = ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) )
50		ovex	⊢ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ∈ V
51	48 49 50	fvmpt3i	⊢ ( ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) )
52	40 51	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) )
53		fveq2	⊢ ( 𝑝 = 𝑥 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) )
54		fveq2	⊢ ( 𝑝 = 𝑥 → ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) )
55	53 54	opeq12d	⊢ ( 𝑝 = 𝑥 → ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ )
56		fveq2	⊢ ( 𝑝 = 𝑥 → ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) = ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) )
57	55 56	oveq12d	⊢ ( 𝑝 = 𝑥 → ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) = ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
58		fveq2	⊢ ( 𝑝 = 𝑥 → ( 𝑉 ‘ 𝑝 ) = ( 𝑉 ‘ 𝑥 ) )
59		fveq2	⊢ ( 𝑝 = 𝑥 → ( 𝑆 ‘ 𝑝 ) = ( 𝑆 ‘ 𝑥 ) )
60	57 58 59	oveq123d	⊢ ( 𝑝 = 𝑥 → ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) )
61		eqid	⊢ ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) = ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) )
62		ovex	⊢ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ∈ V
63	60 61 62	fvmpt3i	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ‘ 𝑥 ) = ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) )
64	63	fveq2d	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ) )
65	64	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ) )
66	52 65	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ‘ 𝑥 ) ) ) = ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ) ) )
67	66	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑝 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑈 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑝 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑝 ) ) ( 𝑅 ‘ 𝑝 ) ) ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑉 ‘ 𝑝 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( 𝑆 ‘ 𝑝 ) ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ) ) ) )
68	24 31 67	3eqtrd	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ⟩ ∗ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Theorem fucocolem2

Proof