Metamath Proof Explorer

Theorem tmachlem-agreeprod

Description: Agreement set can be written as infinite product of acceptable values for tape's cells. (Contributed by Ender Ting, 27-Jul-2026)

Ref Expression
Hypotheses tmach.finalph 
|- ( ph -> U e. Fin )
tmach.exindex 
|- ( ph -> I e. _V )
tmach.tapelist 
|- ( ph -> T = ( U ^m I ) )
tmach.scanmap 
|- ( ph -> S : T --> ( ~P I i^i Fin ) )
tmach.agreemap 
|- ( ph -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
tmach.agreement 
|- ( ph -> A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) )
Assertion tmachlem-agreeprod 
|- ( ( ph /\ a e. T ) -> ( A ` a ) = X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) )

Proof

Step Hyp Ref Expression
1 tmach.finalph 
 |-  ( ph -> U e. Fin )
2 tmach.exindex 
 |-  ( ph -> I e. _V )
3 tmach.tapelist 
 |-  ( ph -> T = ( U ^m I ) )
4 tmach.scanmap 
 |-  ( ph -> S : T --> ( ~P I i^i Fin ) )
5 tmach.agreemap 
 |-  ( ph -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
6 tmach.agreement 
 |-  ( ph -> A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) )
7 fveq2 
 |-  ( z = a -> ( S ` z ) = ( S ` a ) )
8 7 reseq2d 
 |-  ( z = a -> ( y |` ( S ` z ) ) = ( y |` ( S ` a ) ) )
9 id 
 |-  ( z = a -> z = a )
10 9 7 reseq12d 
 |-  ( z = a -> ( z |` ( S ` z ) ) = ( a |` ( S ` a ) ) )
11 8 10 eqeq12d 
 |-  ( z = a -> ( ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) <-> ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) ) )
12 11 rabbidv 
 |-  ( z = a -> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } = { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } )
13 5 adantr 
 |-  ( ( ph /\ a e. T ) -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
14 simpr 
 |-  ( ( ph /\ a e. T ) -> a e. T )
15 1 2 3 4 5 6 tmachlem-extapes 
 |-  ( ph -> T e. _V )
16 15 adantr 
 |-  ( ( ph /\ a e. T ) -> T e. _V )
17 ssrab2 
 |-  { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } C_ T
18 17 a1i 
 |-  ( ( ph /\ a e. T ) -> { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } C_ T )
19 16 18 ssexd 
 |-  ( ( ph /\ a e. T ) -> { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } e. _V )
20 12 13 14 19 fvmptd4 
 |-  ( ( ph /\ a e. T ) -> ( A ` a ) = { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } )
21 snfi 
 |-  { ( a ` i ) } e. Fin
22 21 a1i 
 |-  ( ( ( ph /\ a e. T ) /\ i e. I ) -> { ( a ` i ) } e. Fin )
23 1 ad2antrr 
 |-  ( ( ( ph /\ a e. T ) /\ i e. I ) -> U e. Fin )
24 22 23 ifcld 
 |-  ( ( ( ph /\ a e. T ) /\ i e. I ) -> if ( i e. ( S ` a ) , { ( a ` i ) } , U ) e. Fin )
25 24 ralrimiva 
 |-  ( ( ph /\ a e. T ) -> A. i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) e. Fin )
26 ixpssmapg 
 |-  ( A. i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) e. Fin -> X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) C_ ( U_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ^m I ) )
27 25 26 syl 
 |-  ( ( ph /\ a e. T ) -> X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) C_ ( U_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ^m I ) )
28 ifssun 
 |-  if ( i e. ( S ` a ) , { ( a ` i ) } , U ) C_ ( { ( a ` i ) } u. U )
29 3 eleq2d 
 |-  ( ph -> ( a e. T <-> a e. ( U ^m I ) ) )
30 29 biimpd 
 |-  ( ph -> ( a e. T -> a e. ( U ^m I ) ) )
31 30 imp 
 |-  ( ( ph /\ a e. T ) -> a e. ( U ^m I ) )
32 elmapi 
 |-  ( a e. ( U ^m I ) -> a : I --> U )
33 31 32 syl 
 |-  ( ( ph /\ a e. T ) -> a : I --> U )
34 33 ffvelcdmda 
 |-  ( ( ( ph /\ a e. T ) /\ i e. I ) -> ( a ` i ) e. U )
35 34 snssd 
 |-  ( ( ( ph /\ a e. T ) /\ i e. I ) -> { ( a ` i ) } C_ U )
36 ssequn1 
 |-  ( { ( a ` i ) } C_ U <-> ( { ( a ` i ) } u. U ) = U )
37 35 36 sylib 
 |-  ( ( ( ph /\ a e. T ) /\ i e. I ) -> ( { ( a ` i ) } u. U ) = U )
38 28 37 sseqtrid 
 |-  ( ( ( ph /\ a e. T ) /\ i e. I ) -> if ( i e. ( S ` a ) , { ( a ` i ) } , U ) C_ U )
39 38 iunssd 
 |-  ( ( ph /\ a e. T ) -> U_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) C_ U )
40 mapss 
 |-  ( ( U e. Fin /\ U_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) C_ U ) -> ( U_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ^m I ) C_ ( U ^m I ) )
41 1 39 40 syl2an2r 
 |-  ( ( ph /\ a e. T ) -> ( U_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ^m I ) C_ ( U ^m I ) )
42 27 41 sstrd 
 |-  ( ( ph /\ a e. T ) -> X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) C_ ( U ^m I ) )
43 3 adantr 
 |-  ( ( ph /\ a e. T ) -> T = ( U ^m I ) )
44 42 43 sseqtrrd 
 |-  ( ( ph /\ a e. T ) -> X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) C_ T )
45 simplr 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) ) -> i e. ( S ` a ) )
46 simpr 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) ) -> ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) )
47 45 46 mpd 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) ) -> ( y ` i ) = ( a ` i ) )
48 fvex 
 |-  ( y ` i ) e. _V
49 48 elsn 
 |-  ( ( y ` i ) e. { ( a ` i ) } <-> ( y ` i ) = ( a ` i ) )
50 47 49 sylibr 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) ) -> ( y ` i ) e. { ( a ` i ) } )
51 45 iftrued 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) ) -> if ( i e. ( S ` a ) , { ( a ` i ) } , U ) = { ( a ` i ) } )
52 50 51 eleqtrrd 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) ) -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) )
53 52 ex 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) -> ( ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) )
54 53 a1dd 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) -> ( ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) -> ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) )
55 4 ffvelcdmda 
 |-  ( ( ph /\ a e. T ) -> ( S ` a ) e. ( ~P I i^i Fin ) )
56 55 elin1d 
 |-  ( ( ph /\ a e. T ) -> ( S ` a ) e. ~P I )
57 56 elpwid 
 |-  ( ( ph /\ a e. T ) -> ( S ` a ) C_ I )
58 57 adantr 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> ( S ` a ) C_ I )
59 58 sselda 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) -> i e. I )
60 59 adantr 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> i e. I )
61 simpr 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) )
62 60 61 mpd 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) )
63 simplr 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> i e. ( S ` a ) )
64 63 iftrued 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> if ( i e. ( S ` a ) , { ( a ` i ) } , U ) = { ( a ` i ) } )
65 62 64 eleqtrd 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> ( y ` i ) e. { ( a ` i ) } )
66 65 elsnd 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> ( y ` i ) = ( a ` i ) )
67 66 ex 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) -> ( ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) -> ( y ` i ) = ( a ` i ) ) )
68 67 a1dd 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) -> ( ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) -> ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) ) )
69 54 68 impbid 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ i e. ( S ` a ) ) -> ( ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) <-> ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) )
70 3 eleq2d 
 |-  ( ph -> ( y e. T <-> y e. ( U ^m I ) ) )
71 70 biimpd 
 |-  ( ph -> ( y e. T -> y e. ( U ^m I ) ) )
72 71 adantr 
 |-  ( ( ph /\ a e. T ) -> ( y e. T -> y e. ( U ^m I ) ) )
73 72 imp 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> y e. ( U ^m I ) )
74 elmapi 
 |-  ( y e. ( U ^m I ) -> y : I --> U )
75 73 74 syl 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> y : I --> U )
76 75 adantr 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) -> y : I --> U )
77 76 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) /\ i e. I ) -> ( y ` i ) e. U )
78 simplr 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) /\ i e. I ) -> -. i e. ( S ` a ) )
79 78 iffalsed 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) /\ i e. I ) -> if ( i e. ( S ` a ) , { ( a ` i ) } , U ) = U )
80 77 79 eleqtrrd 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) /\ i e. I ) -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) )
81 80 ex 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) -> ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) )
82 81 a1d 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) -> ( ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) -> ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) )
83 simplr 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> -. i e. ( S ` a ) )
84 83 pm2.21d 
 |-  ( ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) /\ ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) -> ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) )
85 84 ex 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) -> ( ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) -> ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) ) )
86 82 85 impbid 
 |-  ( ( ( ( ph /\ a e. T ) /\ y e. T ) /\ -. i e. ( S ` a ) ) -> ( ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) <-> ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) )
87 69 86 pm2.61dan 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> ( ( i e. ( S ` a ) -> ( y ` i ) = ( a ` i ) ) <-> ( i e. I -> ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) )
88 87 ralbidv2 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> ( A. i e. ( S ` a ) ( y ` i ) = ( a ` i ) <-> A. i e. I ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) )
89 71 imp 
 |-  ( ( ph /\ y e. T ) -> y e. ( U ^m I ) )
90 elmapfn 
 |-  ( y e. ( U ^m I ) -> y Fn I )
91 89 90 syl 
 |-  ( ( ph /\ y e. T ) -> y Fn I )
92 91 adantlr 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> y Fn I )
93 92 biantrurd 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> ( A. i e. I ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) <-> ( y Fn I /\ A. i e. I ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) )
94 88 93 bitr2d 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> ( ( y Fn I /\ A. i e. I ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) <-> A. i e. ( S ` a ) ( y ` i ) = ( a ` i ) ) )
95 vex 
 |-  y e. _V
96 95 elixp 
 |-  ( y e. X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) <-> ( y Fn I /\ A. i e. I ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) )
97 96 a1i 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> ( y e. X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) <-> ( y Fn I /\ A. i e. I ( y ` i ) e. if ( i e. ( S ` a ) , { ( a ` i ) } , U ) ) ) )
98 elmapfn 
 |-  ( a e. ( U ^m I ) -> a Fn I )
99 31 98 syl 
 |-  ( ( ph /\ a e. T ) -> a Fn I )
100 99 adantr 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> a Fn I )
101 fvreseq 
 |-  ( ( ( y Fn I /\ a Fn I ) /\ ( S ` a ) C_ I ) -> ( ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) <-> A. i e. ( S ` a ) ( y ` i ) = ( a ` i ) ) )
102 92 100 58 101 syl21anc 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> ( ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) <-> A. i e. ( S ` a ) ( y ` i ) = ( a ` i ) ) )
103 94 97 102 3bitr4d 
 |-  ( ( ( ph /\ a e. T ) /\ y e. T ) -> ( y e. X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) <-> ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) ) )
104 44 103 eqrrabd 
 |-  ( ( ph /\ a e. T ) -> X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) = { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } )
105 20 104 eqtr4d 
 |-  ( ( ph /\ a e. T ) -> ( A ` a ) = X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) )