Theorem precofvallem

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

	Ref	Expression
Hypotheses	precofvallem.a	|- A = ( Base ` C )
	precofvallem.b	|- B = ( Base ` E )
	precofvallem.1	|- .1. = ( Id ` D )
	precofvallem.i	|- I = ( Id ` E )
	precofvallem.f	|- ( ph -> F ( C Func D ) G )
	precofvallem.k	|- ( ph -> K ( D Func E ) L )
	precofvallem.x	|- ( ph -> X e. A )
Assertion	precofvallem	|- ( ph -> ( ( ( ( F ` X ) L ( F ` X ) ) ` ( ( .1. o. F ) ` X ) ) = ( I ` ( K ` ( F ` X ) ) ) /\ ( K ` ( F ` X ) ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		precofvallem.a	|- A = ( Base ` C )
2		precofvallem.b	|- B = ( Base ` E )
3		precofvallem.1	|- .1. = ( Id ` D )
4		precofvallem.i	|- I = ( Id ` E )
5		precofvallem.f	|- ( ph -> F ( C Func D ) G )
6		precofvallem.k	|- ( ph -> K ( D Func E ) L )
7		precofvallem.x	|- ( ph -> X e. A )
8		eqid	|- ( Base ` D ) = ( Base ` D )
9	1 8 5	funcf1	|- ( ph -> F : A --> ( Base ` D ) )
10	9 7	fvco3d	|- ( ph -> ( ( .1. o. F ) ` X ) = ( .1. ` ( F ` X ) ) )
11	10	fveq2d	|- ( ph -> ( ( ( F ` X ) L ( F ` X ) ) ` ( ( .1. o. F ) ` X ) ) = ( ( ( F ` X ) L ( F ` X ) ) ` ( .1. ` ( F ` X ) ) ) )
12	9 7	ffvelcdmd	|- ( ph -> ( F ` X ) e. ( Base ` D ) )
13	8 3 4 6 12	funcid	|- ( ph -> ( ( ( F ` X ) L ( F ` X ) ) ` ( .1. ` ( F ` X ) ) ) = ( I ` ( K ` ( F ` X ) ) ) )
14	11 13	eqtrd	|- ( ph -> ( ( ( F ` X ) L ( F ` X ) ) ` ( ( .1. o. F ) ` X ) ) = ( I ` ( K ` ( F ` X ) ) ) )
15	8 2 6	funcf1	|- ( ph -> K : ( Base ` D ) --> B )
16	15 12	ffvelcdmd	|- ( ph -> ( K ` ( F ` X ) ) e. B )
17	14 16	jca	|- ( ph -> ( ( ( ( F ` X ) L ( F ` X ) ) ` ( ( .1. o. F ) ` X ) ) = ( I ` ( K ` ( F ` X ) ) ) /\ ( K ` ( F ` X ) ) e. B ) )