Metamath Proof Explorer

Theorem resvsca

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

Ref Expression
Hypotheses resvsca.r 
|- R = ( W |`v A )
resvsca.f 
|- F = ( Scalar ` W )
resvsca.b 
|- B = ( Base ` F )
Assertion resvsca 
|- ( A e. V -> ( F |`s A ) = ( Scalar ` R ) )

Proof

Step Hyp Ref Expression
1 resvsca.r 
 |-  R = ( W |`v A )
2 resvsca.f 
 |-  F = ( Scalar ` W )
3 resvsca.b 
 |-  B = ( Base ` F )
4 2 fvexi 
 |-  F e. _V
5 eqid 
 |-  ( F |`s A ) = ( F |`s A )
6 5 3 ressid2 
 |-  ( ( B C_ A /\ F e. _V /\ A e. V ) -> ( F |`s A ) = F )
7 4 6 mp3an2 
 |-  ( ( B C_ A /\ A e. V ) -> ( F |`s A ) = F )
8 7 3adant2 
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> ( F |`s A ) = F )
9 1 2 3 resvid2 
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> R = W )
10 9 fveq2d 
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> ( Scalar ` R ) = ( Scalar ` W ) )
11 2 8 10 3eqtr4a 
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> ( F |`s A ) = ( Scalar ` R ) )
12 11 3expib 
 |-  ( B C_ A -> ( ( W e. _V /\ A e. V ) -> ( F |`s A ) = ( Scalar ` R ) ) )
13 simp2 
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> W e. _V )
14 ovex 
 |-  ( F |`s A ) e. _V
15 scaid 
 |-  Scalar = Slot ( Scalar ` ndx )
16 15 setsid 
 |-  ( ( W e. _V /\ ( F |`s A ) e. _V ) -> ( F |`s A ) = ( Scalar ` ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )
17 13 14 16 sylancl 
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> ( F |`s A ) = ( Scalar ` ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )
18 1 2 3 resvval2 
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> R = ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) )
19 18 fveq2d 
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> ( Scalar ` R ) = ( Scalar ` ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )
20 17 19 eqtr4d 
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> ( F |`s A ) = ( Scalar ` R ) )
21 20 3expib 
 |-  ( -. B C_ A -> ( ( W e. _V /\ A e. V ) -> ( F |`s A ) = ( Scalar ` R ) ) )
22 12 21 pm2.61i 
 |-  ( ( W e. _V /\ A e. V ) -> ( F |`s A ) = ( Scalar ` R ) )
23 0fv 
 |-  ( (/) ` ( Scalar ` ndx ) ) = (/)
24 0ex 
 |-  (/) e. _V
25 24 15 strfvn 
 |-  ( Scalar ` (/) ) = ( (/) ` ( Scalar ` ndx ) )
26 ress0 
 |-  ( (/) |`s A ) = (/)
27 23 25 26 3eqtr4ri 
 |-  ( (/) |`s A ) = ( Scalar ` (/) )
28 fvprc 
 |-  ( -. W e. _V -> ( Scalar ` W ) = (/) )
29 2 28 eqtrid 
 |-  ( -. W e. _V -> F = (/) )
30 29 oveq1d 
 |-  ( -. W e. _V -> ( F |`s A ) = ( (/) |`s A ) )
31 reldmresv 
 |-  Rel dom |`v
32 31 ovprc1 
 |-  ( -. W e. _V -> ( W |`v A ) = (/) )
33 1 32 eqtrid 
 |-  ( -. W e. _V -> R = (/) )
34 33 fveq2d 
 |-  ( -. W e. _V -> ( Scalar ` R ) = ( Scalar ` (/) ) )
35 27 30 34 3eqtr4a 
 |-  ( -. W e. _V -> ( F |`s A ) = ( Scalar ` R ) )
36 35 adantr 
 |-  ( ( -. W e. _V /\ A e. V ) -> ( F |`s A ) = ( Scalar ` R ) )
37 22 36 pm2.61ian 
 |-  ( A e. V -> ( F |`s A ) = ( Scalar ` R ) )