Metamath Proof Explorer

Theorem reprinrn

Description: Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses reprval.a 
|- ( ph -> A C_ NN )
reprval.m 
|- ( ph -> M e. ZZ )
reprval.s 
|- ( ph -> S e. NN0 )
Assertion reprinrn 
|- ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ( c e. ( A ( repr ` S ) M ) /\ ran c C_ B ) ) )

Proof

Step Hyp Ref Expression
1 reprval.a 
 |-  ( ph -> A C_ NN )
2 reprval.m 
 |-  ( ph -> M e. ZZ )
3 reprval.s 
 |-  ( ph -> S e. NN0 )
4 fin 
 |-  ( c : ( 0 ..^ S ) --> ( A i^i B ) <-> ( c : ( 0 ..^ S ) --> A /\ c : ( 0 ..^ S ) --> B ) )
5 df-f 
 |-  ( c : ( 0 ..^ S ) --> B <-> ( c Fn ( 0 ..^ S ) /\ ran c C_ B ) )
6 ffn 
 |-  ( c : ( 0 ..^ S ) --> A -> c Fn ( 0 ..^ S ) )
7 6 adantl 
 |-  ( ( ph /\ c : ( 0 ..^ S ) --> A ) -> c Fn ( 0 ..^ S ) )
8 7 biantrurd 
 |-  ( ( ph /\ c : ( 0 ..^ S ) --> A ) -> ( ran c C_ B <-> ( c Fn ( 0 ..^ S ) /\ ran c C_ B ) ) )
9 8 bicomd 
 |-  ( ( ph /\ c : ( 0 ..^ S ) --> A ) -> ( ( c Fn ( 0 ..^ S ) /\ ran c C_ B ) <-> ran c C_ B ) )
10 5 9 bitrid 
 |-  ( ( ph /\ c : ( 0 ..^ S ) --> A ) -> ( c : ( 0 ..^ S ) --> B <-> ran c C_ B ) )
11 10 pm5.32da 
 |-  ( ph -> ( ( c : ( 0 ..^ S ) --> A /\ c : ( 0 ..^ S ) --> B ) <-> ( c : ( 0 ..^ S ) --> A /\ ran c C_ B ) ) )
12 4 11 bitrid 
 |-  ( ph -> ( c : ( 0 ..^ S ) --> ( A i^i B ) <-> ( c : ( 0 ..^ S ) --> A /\ ran c C_ B ) ) )
13 nnex 
 |-  NN e. _V
14 13 a1i 
 |-  ( ph -> NN e. _V )
15 14 1 ssexd 
 |-  ( ph -> A e. _V )
16 inex1g 
 |-  ( A e. _V -> ( A i^i B ) e. _V )
17 15 16 syl 
 |-  ( ph -> ( A i^i B ) e. _V )
18 ovex 
 |-  ( 0 ..^ S ) e. _V
19 elmapg 
 |-  ( ( ( A i^i B ) e. _V /\ ( 0 ..^ S ) e. _V ) -> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> ( A i^i B ) ) )
20 17 18 19 sylancl 
 |-  ( ph -> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> ( A i^i B ) ) )
21 elmapg 
 |-  ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) )
22 15 18 21 sylancl 
 |-  ( ph -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) )
23 22 anbi1d 
 |-  ( ph -> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) <-> ( c : ( 0 ..^ S ) --> A /\ ran c C_ B ) ) )
24 12 20 23 3bitr4d 
 |-  ( ph -> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) <-> ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) ) )
25 24 anbi1d 
 |-  ( ph -> ( ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) <-> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) )
26 inss1 
 |-  ( A i^i B ) C_ A
27 26 1 sstrid 
 |-  ( ph -> ( A i^i B ) C_ NN )
28 27 2 3 reprval 
 |-  ( ph -> ( ( A i^i B ) ( repr ` S ) M ) = { c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
29 28 eleq2d 
 |-  ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> c e. { c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) )
30 rabid 
 |-  ( c e. { c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } <-> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) )
31 29 30 bitrdi 
 |-  ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) )
32 1 2 3 reprval 
 |-  ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
33 32 eleq2d 
 |-  ( ph -> ( c e. ( A ( repr ` S ) M ) <-> c e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) )
34 rabid 
 |-  ( c e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } <-> ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) )
35 33 34 bitrdi 
 |-  ( ph -> ( c e. ( A ( repr ` S ) M ) <-> ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) )
36 35 anbi1d 
 |-  ( ph -> ( ( c e. ( A ( repr ` S ) M ) /\ ran c C_ B ) <-> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) /\ ran c C_ B ) ) )
37 an32 
 |-  ( ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) /\ ran c C_ B ) <-> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) )
38 36 37 bitrdi 
 |-  ( ph -> ( ( c e. ( A ( repr ` S ) M ) /\ ran c C_ B ) <-> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) )
39 25 31 38 3bitr4d 
 |-  ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ( c e. ( A ( repr ` S ) M ) /\ ran c C_ B ) ) )