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 ) ) )