Metamath Proof Explorer

Theorem resvval

Description: Value of 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 resvval 
|- ( ( W e. X /\ A e. Y ) -> R = if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )

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 elex 
 |-  ( W e. X -> W e. _V )
5 elex 
 |-  ( A e. Y -> A e. _V )
6 ovex 
 |-  ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) e. _V
7 ifcl 
 |-  ( ( W e. _V /\ ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) e. _V ) -> if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) e. _V )
8 6 7 mpan2 
 |-  ( W e. _V -> if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) e. _V )
9 8 adantr 
 |-  ( ( W e. _V /\ A e. _V ) -> if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) e. _V )
10 simpl 
 |-  ( ( w = W /\ x = A ) -> w = W )
11 10 fveq2d 
 |-  ( ( w = W /\ x = A ) -> ( Scalar ` w ) = ( Scalar ` W ) )
12 11 2 eqtr4di 
 |-  ( ( w = W /\ x = A ) -> ( Scalar ` w ) = F )
13 12 fveq2d 
 |-  ( ( w = W /\ x = A ) -> ( Base ` ( Scalar ` w ) ) = ( Base ` F ) )
14 13 3 eqtr4di 
 |-  ( ( w = W /\ x = A ) -> ( Base ` ( Scalar ` w ) ) = B )
15 simpr 
 |-  ( ( w = W /\ x = A ) -> x = A )
16 14 15 sseq12d 
 |-  ( ( w = W /\ x = A ) -> ( ( Base ` ( Scalar ` w ) ) C_ x <-> B C_ A ) )
17 12 15 oveq12d 
 |-  ( ( w = W /\ x = A ) -> ( ( Scalar ` w ) |`s x ) = ( F |`s A ) )
18 17 opeq2d 
 |-  ( ( w = W /\ x = A ) -> <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >. = <. ( Scalar ` ndx ) , ( F |`s A ) >. )
19 10 18 oveq12d 
 |-  ( ( w = W /\ x = A ) -> ( w sSet <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >. ) = ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) )
20 16 10 19 ifbieq12d 
 |-  ( ( w = W /\ x = A ) -> if ( ( Base ` ( Scalar ` w ) ) C_ x , w , ( w sSet <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >. ) ) = if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )
21 df-resv 
 |-  |`v = ( w e. _V , x e. _V |-> if ( ( Base ` ( Scalar ` w ) ) C_ x , w , ( w sSet <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >. ) ) )
22 20 21 ovmpoga 
 |-  ( ( W e. _V /\ A e. _V /\ if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) e. _V ) -> ( W |`v A ) = if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )
23 9 22 mpd3an3 
 |-  ( ( W e. _V /\ A e. _V ) -> ( W |`v A ) = if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )
24 4 5 23 syl2an 
 |-  ( ( W e. X /\ A e. Y ) -> ( W |`v A ) = if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )
25 1 24 eqtrid 
 |-  ( ( W e. X /\ A e. Y ) -> R = if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )