Metamath Proof Explorer

Theorem resvlem

Description: Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Hypotheses resvlem.r 
|- R = ( W |`v A )
resvlem.e 
|- C = ( E ` W )
resvlem.f 
|- E = Slot N
resvlem.n 
|- N e. NN
resvlem.b 
|- N =/= 5
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 N
4 resvlem.n 
 |-  N e. NN
5 resvlem.b 
 |-  N =/= 5
6 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
7 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
8 1 6 7 resvid2 
 |-  ( ( ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> R = W )
9 8 fveq2d 
 |-  ( ( ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
10 9 3expib 
 |-  ( ( Base ` ( Scalar ` W ) ) C_ A -> ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) ) )
11 1 6 7 resvval2 
 |-  ( ( -. ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> R = ( W sSet <. ( Scalar ` ndx ) , ( ( Scalar ` W ) |`s A ) >. ) )
12 11 fveq2d 
 |-  ( ( -. ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` ( W sSet <. ( Scalar ` ndx ) , ( ( Scalar ` W ) |`s A ) >. ) ) )
13 3 4 ndxid 
 |-  E = Slot ( E ` ndx )
14 3 4 ndxarg 
 |-  ( E ` ndx ) = N
15 14 5 eqnetri 
 |-  ( E ` ndx ) =/= 5
16 scandx 
 |-  ( Scalar ` ndx ) = 5
17 15 16 neeqtrri 
 |-  ( E ` ndx ) =/= ( Scalar ` ndx )
18 13 17 setsnid 
 |-  ( E ` W ) = ( E ` ( W sSet <. ( Scalar ` ndx ) , ( ( Scalar ` W ) |`s A ) >. ) )
19 12 18 eqtr4di 
 |-  ( ( -. ( Base ` ( Scalar ` W ) ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
20 19 3expib 
 |-  ( -. ( Base ` ( Scalar ` W ) ) C_ A -> ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) ) )
21 10 20 pm2.61i 
 |-  ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
22 reldmresv 
 |-  Rel dom |`v
23 22 ovprc1 
 |-  ( -. W e. _V -> ( W |`v A ) = (/) )
24 1 23 syl5eq 
 |-  ( -. W e. _V -> R = (/) )
25 24 fveq2d 
 |-  ( -. W e. _V -> ( E ` R ) = ( E ` (/) ) )
26 3 str0 
 |-  (/) = ( E ` (/) )
27 25 26 eqtr4di 
 |-  ( -. W e. _V -> ( E ` R ) = (/) )
28 fvprc 
 |-  ( -. W e. _V -> ( E ` W ) = (/) )
29 27 28 eqtr4d 
 |-  ( -. W e. _V -> ( E ` R ) = ( E ` W ) )
30 29 adantr 
 |-  ( ( -. W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
31 21 30 pm2.61ian 
 |-  ( A e. V -> ( E ` R ) = ( E ` W ) )
32 2 31 eqtr4id 
 |-  ( A e. V -> C = ( E ` R ) )