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