Theorem precofvallem

Description: Lemma for precofval to enable catlid or catrid . (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	precofvallem.a	$$⊢A={\mathrm{Base}}_C$$
	precofvallem.b	$$⊢B={\mathrm{Base}}_E$$
	precofvallem.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(D\right)$$
	precofvallem.i	$$⊢I=\mathrm{Id}\left(E\right)$$
	precofvallem.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
	precofvallem.k	$$⊢\phi \to K\left(D\mathrm{Func}E\right)L$$
	precofvallem.x	$$⊢\phi \to X\in A$$
Assertion	precofvallem	$$⊢\phi \to \left(\left(F\left(X\right)LF\left(X\right)\right)\left(\left(\underset{\dot{}}{1}\circ F\right)\left(X\right)\right)=I\left(K\left(F\left(X\right)\right)\right)\wedge K\left(F\left(X\right)\right)\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		precofvallem.a	$$⊢A={\mathrm{Base}}_C$$
2		precofvallem.b	$$⊢B={\mathrm{Base}}_E$$
3		precofvallem.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(D\right)$$
4		precofvallem.i	$$⊢I=\mathrm{Id}\left(E\right)$$
5		precofvallem.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
6		precofvallem.k	$$⊢\phi \to K\left(D\mathrm{Func}E\right)L$$
7		precofvallem.x	$$⊢\phi \to X\in A$$
8		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
9	1 8 5	funcf1	$$⊢\phi \to F:A⟶{\mathrm{Base}}_D$$
10	9 7	fvco3d	$$⊢\phi \to \left(\underset{\dot{}}{1}\circ F\right)\left(X\right)=\underset{\dot{}}{1}\left(F\left(X\right)\right)$$
11	10	fveq2d	$$⊢\phi \to \left(F\left(X\right)LF\left(X\right)\right)\left(\left(\underset{\dot{}}{1}\circ F\right)\left(X\right)\right)=\left(F\left(X\right)LF\left(X\right)\right)\left(\underset{\dot{}}{1}\left(F\left(X\right)\right)\right)$$
12	9 7	ffvelcdmd	$$⊢\phi \to F\left(X\right)\in {\mathrm{Base}}_D$$
13	8 3 4 6 12	funcid	$$⊢\phi \to \left(F\left(X\right)LF\left(X\right)\right)\left(\underset{\dot{}}{1}\left(F\left(X\right)\right)\right)=I\left(K\left(F\left(X\right)\right)\right)$$
14	11 13	eqtrd	$$⊢\phi \to \left(F\left(X\right)LF\left(X\right)\right)\left(\left(\underset{\dot{}}{1}\circ F\right)\left(X\right)\right)=I\left(K\left(F\left(X\right)\right)\right)$$
15	8 2 6	funcf1	$$⊢\phi \to K:{\mathrm{Base}}_D⟶B$$
16	15 12	ffvelcdmd	$$⊢\phi \to K\left(F\left(X\right)\right)\in B$$
17	14 16	jca	$$⊢\phi \to \left(\left(F\left(X\right)LF\left(X\right)\right)\left(\left(\underset{\dot{}}{1}\circ F\right)\left(X\right)\right)=I\left(K\left(F\left(X\right)\right)\right)\wedge K\left(F\left(X\right)\right)\in B\right)$$