Metamath Proof Explorer

Theorem rescabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses rescabs.c 
|- ( ph -> C e. V )
rescabs.h 
|- ( ph -> H Fn ( S X. S ) )
rescabs.j 
|- ( ph -> J Fn ( T X. T ) )
rescabs.s 
|- ( ph -> S e. W )
rescabs.t 
|- ( ph -> T C_ S )
Assertion rescabs 
|- ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )

Proof

Step Hyp Ref Expression
1 rescabs.c 
 |-  ( ph -> C e. V )
2 rescabs.h 
 |-  ( ph -> H Fn ( S X. S ) )
3 rescabs.j 
 |-  ( ph -> J Fn ( T X. T ) )
4 rescabs.s 
 |-  ( ph -> S e. W )
5 rescabs.t 
 |-  ( ph -> T C_ S )
6 eqid 
 |-  ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J )
7 ovexd 
 |-  ( ph -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
8 4 5 ssexd 
 |-  ( ph -> T e. _V )
9 6 7 8 3 rescval2 
 |-  ( ph -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
10 simpr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( Base ` ( C |`s S ) ) C_ T )
11 ovexd 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
12 8 adantr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> T e. _V )
13 eqid 
 |-  ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T )
14 baseid 
 |-  Base = Slot ( Base ` ndx )
15 1re 
 |-  1 e. RR
16 1nn 
 |-  1 e. NN
17 4nn0 
 |-  4 e. NN0
18 1nn0 
 |-  1 e. NN0
19 1lt10 
 |-  1 < ; 1 0
20 16 17 18 19 declti 
 |-  1 < ; 1 4
21 15 20 ltneii 
 |-  1 =/= ; 1 4
22 basendx 
 |-  ( Base ` ndx ) = 1
23 homndx 
 |-  ( Hom ` ndx ) = ; 1 4
24 22 23 neeq12i 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) <-> 1 =/= ; 1 4 )
25 21 24 mpbir 
 |-  ( Base ` ndx ) =/= ( Hom ` ndx )
26 14 25 setsnid 
 |-  ( Base ` ( C |`s S ) ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
27 13 26 ressid2 
 |-  ( ( ( Base ` ( C |`s S ) ) C_ T /\ ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V /\ T e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
28 10 11 12 27 syl3anc 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
29 28 oveq1d 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) )
30 ovex 
 |-  ( C |`s S ) e. _V
31 8 8 xpexd 
 |-  ( ph -> ( T X. T ) e. _V )
32 fnex 
 |-  ( ( J Fn ( T X. T ) /\ ( T X. T ) e. _V ) -> J e. _V )
33 3 31 32 syl2anc 
 |-  ( ph -> J e. _V )
34 33 adantr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> J e. _V )
35 setsabs 
 |-  ( ( ( C |`s S ) e. _V /\ J e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) )
36 30 34 35 sylancr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) )
37 eqid 
 |-  ( C |`s S ) = ( C |`s S )
38 eqid 
 |-  ( Base ` C ) = ( Base ` C )
39 37 38 ressbas 
 |-  ( S e. W -> ( S i^i ( Base ` C ) ) = ( Base ` ( C |`s S ) ) )
40 4 39 syl 
 |-  ( ph -> ( S i^i ( Base ` C ) ) = ( Base ` ( C |`s S ) ) )
41 40 sseq1d 
 |-  ( ph -> ( ( S i^i ( Base ` C ) ) C_ T <-> ( Base ` ( C |`s S ) ) C_ T ) )
42 41 biimpar 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ T )
43 inss2 
 |-  ( S i^i ( Base ` C ) ) C_ ( Base ` C )
44 43 a1i 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ ( Base ` C ) )
45 42 44 ssind 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ ( T i^i ( Base ` C ) ) )
46 5 adantr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> T C_ S )
47 46 ssrind 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( T i^i ( Base ` C ) ) C_ ( S i^i ( Base ` C ) ) )
48 45 47 eqssd 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) = ( T i^i ( Base ` C ) ) )
49 48 oveq2d 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s ( S i^i ( Base ` C ) ) ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
50 4 adantr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> S e. W )
51 38 ressinbas 
 |-  ( S e. W -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
52 50 51 syl 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
53 38 ressinbas 
 |-  ( T e. _V -> ( C |`s T ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
54 12 53 syl 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s T ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
55 49 52 54 3eqtr4d 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) = ( C |`s T ) )
56 55 oveq1d 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
57 29 36 56 3eqtrd 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
58 simpr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> -. ( Base ` ( C |`s S ) ) C_ T )
59 ovexd 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
60 8 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> T e. _V )
61 13 26 ressval2 
 |-  ( ( -. ( Base ` ( C |`s S ) ) C_ T /\ ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V /\ T e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
62 58 59 60 61 syl3anc 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
63 ovexd 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) e. _V )
64 25 necomi 
 |-  ( Hom ` ndx ) =/= ( Base ` ndx )
65 64 a1i 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( Hom ` ndx ) =/= ( Base ` ndx ) )
66 4 4 xpexd 
 |-  ( ph -> ( S X. S ) e. _V )
67 fnex 
 |-  ( ( H Fn ( S X. S ) /\ ( S X. S ) e. _V ) -> H e. _V )
68 2 66 67 syl2anc 
 |-  ( ph -> H e. _V )
69 68 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> H e. _V )
70 fvex 
 |-  ( Base ` ( C |`s S ) ) e. _V
71 70 inex2 
 |-  ( T i^i ( Base ` ( C |`s S ) ) ) e. _V
72 71 a1i 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( T i^i ( Base ` ( C |`s S ) ) ) e. _V )
73 fvex 
 |-  ( Hom ` ndx ) e. _V
74 fvex 
 |-  ( Base ` ndx ) e. _V
75 73 74 setscom 
 |-  ( ( ( ( C |`s S ) e. _V /\ ( Hom ` ndx ) =/= ( Base ` ndx ) ) /\ ( H e. _V /\ ( T i^i ( Base ` ( C |`s S ) ) ) e. _V ) ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) )
76 63 65 69 72 75 syl22anc 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) )
77 eqid 
 |-  ( ( C |`s S ) |`s T ) = ( ( C |`s S ) |`s T )
78 eqid 
 |-  ( Base ` ( C |`s S ) ) = ( Base ` ( C |`s S ) )
79 77 78 ressval2 
 |-  ( ( -. ( Base ` ( C |`s S ) ) C_ T /\ ( C |`s S ) e. _V /\ T e. _V ) -> ( ( C |`s S ) |`s T ) = ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
80 58 63 60 79 syl3anc 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) |`s T ) = ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
81 4 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> S e. W )
82 5 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> T C_ S )
83 ressabs 
 |-  ( ( S e. W /\ T C_ S ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
84 81 82 83 syl2anc 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
85 80 84 eqtr3d 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( C |`s T ) )
86 85 oveq1d 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) )
87 62 76 86 3eqtrd 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) )
88 87 oveq1d 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) )
89 ovex 
 |-  ( C |`s T ) e. _V
90 33 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> J e. _V )
91 setsabs 
 |-  ( ( ( C |`s T ) e. _V /\ J e. _V ) -> ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
92 89 90 91 sylancr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
93 88 92 eqtrd 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
94 57 93 pm2.61dan 
 |-  ( ph -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
95 9 94 eqtrd 
 |-  ( ph -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
96 eqid 
 |-  ( C |`cat H ) = ( C |`cat H )
97 96 1 4 2 rescval2 
 |-  ( ph -> ( C |`cat H ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
98 97 oveq1d 
 |-  ( ph -> ( ( C |`cat H ) |`cat J ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) )
99 eqid 
 |-  ( C |`cat J ) = ( C |`cat J )
100 99 1 8 3 rescval2 
 |-  ( ph -> ( C |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
101 95 98 100 3eqtr4d 
 |-  ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )