Theorem resvlem

Description: Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (Revised by AV, 31-Oct-2024)

	Ref	Expression
Hypotheses	resvlem.r	|- R = ( W |`v A )
	resvlem.e	|- C = ( E ` W )
	resvlem.f	|- E = Slot ( E ` ndx )
	resvlem.n	|- ( E ` ndx ) =/= ( Scalar ` ndx )
Assertion	resvlem	|- ( A e. V -> C = ( E ` R ) )

Proof

Step	Hyp	Ref	Expression
1		resvlem.r	|- R = ( W |`v A )
2		resvlem.e	|- C = ( E ` W )
3		resvlem.f	|- E = Slot ( E ` ndx )
4		resvlem.n	|- ( E ` ndx ) =/= ( Scalar ` ndx )
5		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
6		eqid	|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
7	1 5 6	resvid2	|- ( ( ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> R = W )
8	7	fveq2d	|- ( ( ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
9	8	3expib	|- ( ( Base ` ( Scalar ` W ) ) C_ A -> ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) ) )
10	1 5 6	resvval2	|- ( ( -. ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> R = ( W sSet <. ( Scalar ` ndx ) , ( ( Scalar ` W ) |`s A ) >. ) )
11	10	fveq2d	|- ( ( -. ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` ( W sSet <. ( Scalar ` ndx ) , ( ( Scalar ` W ) |`s A ) >. ) ) )
12	3 4	setsnid	|- ( E ` W ) = ( E ` ( W sSet <. ( Scalar ` ndx ) , ( ( Scalar ` W ) |`s A ) >. ) )
13	11 12	eqtr4di	|- ( ( -. ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
14	13	3expib	|- ( -. ( Base ` ( Scalar ` W ) ) C_ A -> ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) ) )
15	9 14	pm2.61i	|- ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
16	3	str0	|- (/) = ( E ` (/) )
17	16	eqcomi	|- ( E ` (/) ) = (/)
18		reldmresv	|- Rel dom |`v
19	17 1 18	oveqprc	|- ( -. W e. _V -> ( E ` W ) = ( E ` R ) )
20	19	eqcomd	|- ( -. W e. _V -> ( E ` R ) = ( E ` W ) )
21	20	adantr	|- ( ( -. W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
22	15 21	pm2.61ian	|- ( A e. V -> ( E ` R ) = ( E ` W ) )
23	2 22	eqtr4id	|- ( A e. V -> C = ( E ` R ) )