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