Theorem fucoaltvallem

Description: Lemma for fucoaltval . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fucoaltfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoaltval.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 )
	fucoaltval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoaltval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	fucoaltval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
	fucoaltval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
	fucoaltval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
	fucoaltval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
	fucoaltval.i	⊢ 𝐼 = ( idfunc ‘ 𝐶 )
	fucoaltval.j	⊢ 𝐽 = ( Id ‘ ( 𝐶 FuncCat 𝐶 ) )
	fucoaltvallem.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐶 ) )
Assertion	fucoaltvallem	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
2		fucoaltval.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 )
3		fucoaltval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		fucoaltval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
5		fucoaltval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
6		fucoaltval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
7		fucoaltval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
8		fucoaltval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
9		fucoaltval.i	⊢ 𝐼 = ( idfunc ‘ 𝐶 )
10		fucoaltval.j	⊢ 𝐽 = ( Id ‘ ( 𝐶 FuncCat 𝐶 ) )
11		fucoaltvallem.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐶 ) )
12		df-ov	⊢ ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ‘ ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ )
13	11	xpcfucbas	⊢ ( ( 𝐶 Func 𝐸 ) × ( 𝐶 Func 𝐶 ) ) = ( Base ‘ 𝑇 )
14	11 1 3 3 4	fucofunca	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 ) ∈ ( 𝑇 Func 𝑄 ) )
15	2 14	eqeltrid	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑇 Func 𝑄 ) )
16	9	idfucl	⊢ ( 𝐶 ∈ Cat → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
17	3 16	syl	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
18	6 17	opelxpd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐼 ⟩ ∈ ( ( 𝐶 Func 𝐸 ) × ( 𝐶 Func 𝐶 ) ) )
19	7 17	opelxpd	⊢ ( 𝜑 → ⟨ 𝐺 , 𝐼 ⟩ ∈ ( ( 𝐶 Func 𝐸 ) × ( 𝐶 Func 𝐶 ) ) )
20		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
21		eqid	⊢ ( 𝐶 FuncCat 𝐶 ) = ( 𝐶 FuncCat 𝐶 )
22	21	fucbas	⊢ ( 𝐶 Func 𝐶 ) = ( Base ‘ ( 𝐶 FuncCat 𝐶 ) )
23		eqid	⊢ ( 𝐶 Nat 𝐶 ) = ( 𝐶 Nat 𝐶 )
24	21 23	fuchom	⊢ ( 𝐶 Nat 𝐶 ) = ( Hom ‘ ( 𝐶 FuncCat 𝐶 ) )
25	21 3 3	fuccat	⊢ ( 𝜑 → ( 𝐶 FuncCat 𝐶 ) ∈ Cat )
26	22 24 10 25 17	catidcl	⊢ ( 𝜑 → ( 𝐽 ‘ 𝐼 ) ∈ ( 𝐼 ( 𝐶 Nat 𝐶 ) 𝐼 ) )
27	8 26	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ ∈ ( ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) × ( 𝐼 ( 𝐶 Nat 𝐶 ) 𝐼 ) ) )
28	11 6 17 7 17 20	xpcfuchom2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐼 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝐺 , 𝐼 ⟩ ) = ( ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) × ( 𝐼 ( 𝐶 Nat 𝐶 ) 𝐼 ) ) )
29	27 28	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ ∈ ( ⟨ 𝐹 , 𝐼 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝐺 , 𝐼 ⟩ ) )
30	13 15 5 18 19 20 29	cofu2	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ‘ ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ ) = ( ( ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐹 , 𝐼 ⟩ ) ( 2nd ‘ 𝐾 ) ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐺 , 𝐼 ⟩ ) ) ‘ ( ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ‘ ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ ) ) )
31		df-ov	⊢ ( 𝐹 ( 1st ‘ 𝐿 ) 𝐼 ) = ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐹 , 𝐼 ⟩ )
32	2	eqcomi	⊢ ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 ) = 𝐿
33	32	fveq2i	⊢ ( 1st ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 ) ) = ( 1st ‘ 𝐿 )
34	33	a1i	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 ) ) = ( 1st ‘ 𝐿 ) )
35	34 17 6	fuco11b	⊢ ( 𝜑 → ( 𝐹 ( 1st ‘ 𝐿 ) 𝐼 ) = ( 𝐹 ∘func 𝐼 ) )
36	6 9	cofurid	⊢ ( 𝜑 → ( 𝐹 ∘func 𝐼 ) = 𝐹 )
37	35 36	eqtrd	⊢ ( 𝜑 → ( 𝐹 ( 1st ‘ 𝐿 ) 𝐼 ) = 𝐹 )
38	31 37	eqtr3id	⊢ ( 𝜑 → ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐹 , 𝐼 ⟩ ) = 𝐹 )
39		df-ov	⊢ ( 𝐺 ( 1st ‘ 𝐿 ) 𝐼 ) = ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐺 , 𝐼 ⟩ )
40	34 17 7	fuco11b	⊢ ( 𝜑 → ( 𝐺 ( 1st ‘ 𝐿 ) 𝐼 ) = ( 𝐺 ∘func 𝐼 ) )
41	7 9	cofurid	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐼 ) = 𝐺 )
42	40 41	eqtrd	⊢ ( 𝜑 → ( 𝐺 ( 1st ‘ 𝐿 ) 𝐼 ) = 𝐺 )
43	39 42	eqtr3id	⊢ ( 𝜑 → ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐺 , 𝐼 ⟩ ) = 𝐺 )
44	38 43	oveq12d	⊢ ( 𝜑 → ( ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐹 , 𝐼 ⟩ ) ( 2nd ‘ 𝐾 ) ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐺 , 𝐼 ⟩ ) ) = ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) )
45		df-ov	⊢ ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ‘ ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ )
46	32	fveq2i	⊢ ( 2nd ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 ) ) = ( 2nd ‘ 𝐿 )
47	46	a1i	⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 ) ) = ( 2nd ‘ 𝐿 ) )
48	47 21 10 9 3 8	fucoridid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = 𝐴 )
49	45 48	eqtr3id	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ‘ ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ ) = 𝐴 )
50	44 49	fveq12d	⊢ ( 𝜑 → ( ( ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐹 , 𝐼 ⟩ ) ( 2nd ‘ 𝐾 ) ( ( 1st ‘ 𝐿 ) ‘ ⟨ 𝐺 , 𝐼 ⟩ ) ) ‘ ( ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ‘ ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ ) ) = ( ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) )
51	30 50	eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ‘ ⟨ 𝐴 , ( 𝐽 ‘ 𝐼 ) ⟩ ) = ( ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) )
52	12 51	eqtrid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) )