Metamath Proof Explorer

Theorem restco

Description: Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion restco 
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J |`t A ) |`t B ) = ( J |`t ( A i^i B ) ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  y e. _V
2 1 inex1 
 |-  ( y i^i A ) e. _V
3 ineq1 
 |-  ( x = ( y i^i A ) -> ( x i^i B ) = ( ( y i^i A ) i^i B ) )
4 inass 
 |-  ( ( y i^i A ) i^i B ) = ( y i^i ( A i^i B ) )
5 3 4 eqtrdi 
 |-  ( x = ( y i^i A ) -> ( x i^i B ) = ( y i^i ( A i^i B ) ) )
6 2 5 abrexco 
 |-  { z | E. x e. { w | E. y e. J w = ( y i^i A ) } z = ( x i^i B ) } = { z | E. y e. J z = ( y i^i ( A i^i B ) ) }
7 eqid 
 |-  ( y e. J |-> ( y i^i A ) ) = ( y e. J |-> ( y i^i A ) )
8 7 rnmpt 
 |-  ran ( y e. J |-> ( y i^i A ) ) = { w | E. y e. J w = ( y i^i A ) }
9 8 mpteq1i 
 |-  ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) = ( x e. { w | E. y e. J w = ( y i^i A ) } |-> ( x i^i B ) )
10 9 rnmpt 
 |-  ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) = { z | E. x e. { w | E. y e. J w = ( y i^i A ) } z = ( x i^i B ) }
11 eqid 
 |-  ( y e. J |-> ( y i^i ( A i^i B ) ) ) = ( y e. J |-> ( y i^i ( A i^i B ) ) )
12 11 rnmpt 
 |-  ran ( y e. J |-> ( y i^i ( A i^i B ) ) ) = { z | E. y e. J z = ( y i^i ( A i^i B ) ) }
13 6 10 12 3eqtr4i 
 |-  ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) = ran ( y e. J |-> ( y i^i ( A i^i B ) ) )
14 restval 
 |-  ( ( J e. V /\ A e. W ) -> ( J |`t A ) = ran ( y e. J |-> ( y i^i A ) ) )
15 14 3adant3 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> ( J |`t A ) = ran ( y e. J |-> ( y i^i A ) ) )
16 15 oveq1d 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J |`t A ) |`t B ) = ( ran ( y e. J |-> ( y i^i A ) ) |`t B ) )
17 ovex 
 |-  ( J |`t A ) e. _V
18 15 17 eqeltrrdi 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> ran ( y e. J |-> ( y i^i A ) ) e. _V )
19 simp3 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> B e. X )
20 restval 
 |-  ( ( ran ( y e. J |-> ( y i^i A ) ) e. _V /\ B e. X ) -> ( ran ( y e. J |-> ( y i^i A ) ) |`t B ) = ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) )
21 18 19 20 syl2anc 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> ( ran ( y e. J |-> ( y i^i A ) ) |`t B ) = ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) )
22 16 21 eqtrd 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J |`t A ) |`t B ) = ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) )
23 simp1 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> J e. V )
24 inex1g 
 |-  ( A e. W -> ( A i^i B ) e. _V )
25 24 3ad2ant2 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> ( A i^i B ) e. _V )
26 restval 
 |-  ( ( J e. V /\ ( A i^i B ) e. _V ) -> ( J |`t ( A i^i B ) ) = ran ( y e. J |-> ( y i^i ( A i^i B ) ) ) )
27 23 25 26 syl2anc 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> ( J |`t ( A i^i B ) ) = ran ( y e. J |-> ( y i^i ( A i^i B ) ) ) )
28 13 22 27 3eqtr4a 
 |-  ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J |`t A ) |`t B ) = ( J |`t ( A i^i B ) ) )