This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )