Metamath Proof Explorer

Theorem hgt750lemg

Description: Lemma for the statement 7.50 of Helfgott p. 69. Applying a permutation T to the three factors of a product does not change the result. (Contributed by Thierry Arnoux, 1-Jan-2022)

Ref Expression
Hypotheses hgt750lemg.f 
|- F = ( c e. R |-> ( c o. T ) )
hgt750lemg.t 
|- ( ph -> T : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) )
hgt750lemg.n 
|- ( ph -> N : ( 0 ..^ 3 ) --> NN )
hgt750lemg.l 
|- ( ph -> L : NN --> RR )
hgt750lemg.1 
|- ( ph -> N e. R )
Assertion hgt750lemg 
|- ( ph -> ( ( L ` ( ( F ` N ) ` 0 ) ) x. ( ( L ` ( ( F ` N ) ` 1 ) ) x. ( L ` ( ( F ` N ) ` 2 ) ) ) ) = ( ( L ` ( N ` 0 ) ) x. ( ( L ` ( N ` 1 ) ) x. ( L ` ( N ` 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hgt750lemg.f 
 |-  F = ( c e. R |-> ( c o. T ) )
2 hgt750lemg.t 
 |-  ( ph -> T : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) )
3 hgt750lemg.n 
 |-  ( ph -> N : ( 0 ..^ 3 ) --> NN )
4 hgt750lemg.l 
 |-  ( ph -> L : NN --> RR )
5 hgt750lemg.1 
 |-  ( ph -> N e. R )
6 2fveq3 
 |-  ( a = ( T ` b ) -> ( L ` ( N ` a ) ) = ( L ` ( N ` ( T ` b ) ) ) )
7 tpfi 
 |-  { 0 , 1 , 2 } e. Fin
8 7 a1i 
 |-  ( ph -> { 0 , 1 , 2 } e. Fin )
9 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
10 f1oeq23 
 |-  ( ( ( 0 ..^ 3 ) = { 0 , 1 , 2 } /\ ( 0 ..^ 3 ) = { 0 , 1 , 2 } ) -> ( T : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) <-> T : { 0 , 1 , 2 } -1-1-onto-> { 0 , 1 , 2 } ) )
11 9 9 10 mp2an 
 |-  ( T : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) <-> T : { 0 , 1 , 2 } -1-1-onto-> { 0 , 1 , 2 } )
12 2 11 sylib 
 |-  ( ph -> T : { 0 , 1 , 2 } -1-1-onto-> { 0 , 1 , 2 } )
13 eqidd 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( T ` b ) = ( T ` b ) )
14 4 adantr 
 |-  ( ( ph /\ a e. { 0 , 1 , 2 } ) -> L : NN --> RR )
15 3 adantr 
 |-  ( ( ph /\ a e. { 0 , 1 , 2 } ) -> N : ( 0 ..^ 3 ) --> NN )
16 simpr 
 |-  ( ( ph /\ a e. { 0 , 1 , 2 } ) -> a e. { 0 , 1 , 2 } )
17 16 9 eleqtrrdi 
 |-  ( ( ph /\ a e. { 0 , 1 , 2 } ) -> a e. ( 0 ..^ 3 ) )
18 15 17 ffvelrnd 
 |-  ( ( ph /\ a e. { 0 , 1 , 2 } ) -> ( N ` a ) e. NN )
19 14 18 ffvelrnd 
 |-  ( ( ph /\ a e. { 0 , 1 , 2 } ) -> ( L ` ( N ` a ) ) e. RR )
20 19 recnd 
 |-  ( ( ph /\ a e. { 0 , 1 , 2 } ) -> ( L ` ( N ` a ) ) e. CC )
21 6 8 12 13 20 fprodf1o 
 |-  ( ph -> prod_ a e. { 0 , 1 , 2 } ( L ` ( N ` a ) ) = prod_ b e. { 0 , 1 , 2 } ( L ` ( N ` ( T ` b ) ) ) )
22 1 a1i 
 |-  ( ph -> F = ( c e. R |-> ( c o. T ) ) )
23 simpr 
 |-  ( ( ph /\ c = N ) -> c = N )
24 23 coeq1d 
 |-  ( ( ph /\ c = N ) -> ( c o. T ) = ( N o. T ) )
25 f1of 
 |-  ( T : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) -> T : ( 0 ..^ 3 ) --> ( 0 ..^ 3 ) )
26 2 25 syl 
 |-  ( ph -> T : ( 0 ..^ 3 ) --> ( 0 ..^ 3 ) )
27 ovexd 
 |-  ( ph -> ( 0 ..^ 3 ) e. _V )
28 fex2 
 |-  ( ( T : ( 0 ..^ 3 ) --> ( 0 ..^ 3 ) /\ ( 0 ..^ 3 ) e. _V /\ ( 0 ..^ 3 ) e. _V ) -> T e. _V )
29 26 27 27 28 syl3anc 
 |-  ( ph -> T e. _V )
30 coexg 
 |-  ( ( N e. R /\ T e. _V ) -> ( N o. T ) e. _V )
31 5 29 30 syl2anc 
 |-  ( ph -> ( N o. T ) e. _V )
32 22 24 5 31 fvmptd 
 |-  ( ph -> ( F ` N ) = ( N o. T ) )
33 32 adantr 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( F ` N ) = ( N o. T ) )
34 33 fveq1d 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( ( F ` N ) ` b ) = ( ( N o. T ) ` b ) )
35 f1ofun 
 |-  ( T : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) -> Fun T )
36 2 35 syl 
 |-  ( ph -> Fun T )
37 36 adantr 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> Fun T )
38 f1odm 
 |-  ( T : { 0 , 1 , 2 } -1-1-onto-> { 0 , 1 , 2 } -> dom T = { 0 , 1 , 2 } )
39 12 38 syl 
 |-  ( ph -> dom T = { 0 , 1 , 2 } )
40 39 eleq2d 
 |-  ( ph -> ( b e. dom T <-> b e. { 0 , 1 , 2 } ) )
41 40 biimpar 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> b e. dom T )
42 fvco 
 |-  ( ( Fun T /\ b e. dom T ) -> ( ( N o. T ) ` b ) = ( N ` ( T ` b ) ) )
43 37 41 42 syl2anc 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( ( N o. T ) ` b ) = ( N ` ( T ` b ) ) )
44 34 43 eqtr2d 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( N ` ( T ` b ) ) = ( ( F ` N ) ` b ) )
45 44 fveq2d 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( L ` ( N ` ( T ` b ) ) ) = ( L ` ( ( F ` N ) ` b ) ) )
46 45 prodeq2dv 
 |-  ( ph -> prod_ b e. { 0 , 1 , 2 } ( L ` ( N ` ( T ` b ) ) ) = prod_ b e. { 0 , 1 , 2 } ( L ` ( ( F ` N ) ` b ) ) )
47 21 46 eqtr2d 
 |-  ( ph -> prod_ b e. { 0 , 1 , 2 } ( L ` ( ( F ` N ) ` b ) ) = prod_ a e. { 0 , 1 , 2 } ( L ` ( N ` a ) ) )
48 2fveq3 
 |-  ( b = 0 -> ( L ` ( ( F ` N ) ` b ) ) = ( L ` ( ( F ` N ) ` 0 ) ) )
49 2fveq3 
 |-  ( b = 1 -> ( L ` ( ( F ` N ) ` b ) ) = ( L ` ( ( F ` N ) ` 1 ) ) )
50 c0ex 
 |-  0 e. _V
51 50 a1i 
 |-  ( ph -> 0 e. _V )
52 1ex 
 |-  1 e. _V
53 52 a1i 
 |-  ( ph -> 1 e. _V )
54 32 fveq1d 
 |-  ( ph -> ( ( F ` N ) ` 0 ) = ( ( N o. T ) ` 0 ) )
55 50 tpid1 
 |-  0 e. { 0 , 1 , 2 }
56 55 39 eleqtrrid 
 |-  ( ph -> 0 e. dom T )
57 fvco 
 |-  ( ( Fun T /\ 0 e. dom T ) -> ( ( N o. T ) ` 0 ) = ( N ` ( T ` 0 ) ) )
58 36 56 57 syl2anc 
 |-  ( ph -> ( ( N o. T ) ` 0 ) = ( N ` ( T ` 0 ) ) )
59 54 58 eqtrd 
 |-  ( ph -> ( ( F ` N ) ` 0 ) = ( N ` ( T ` 0 ) ) )
60 55 9 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
61 60 a1i 
 |-  ( ph -> 0 e. ( 0 ..^ 3 ) )
62 26 61 ffvelrnd 
 |-  ( ph -> ( T ` 0 ) e. ( 0 ..^ 3 ) )
63 3 62 ffvelrnd 
 |-  ( ph -> ( N ` ( T ` 0 ) ) e. NN )
64 59 63 eqeltrd 
 |-  ( ph -> ( ( F ` N ) ` 0 ) e. NN )
65 4 64 ffvelrnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 0 ) ) e. RR )
66 65 recnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 0 ) ) e. CC )
67 32 fveq1d 
 |-  ( ph -> ( ( F ` N ) ` 1 ) = ( ( N o. T ) ` 1 ) )
68 52 tpid2 
 |-  1 e. { 0 , 1 , 2 }
69 68 39 eleqtrrid 
 |-  ( ph -> 1 e. dom T )
70 fvco 
 |-  ( ( Fun T /\ 1 e. dom T ) -> ( ( N o. T ) ` 1 ) = ( N ` ( T ` 1 ) ) )
71 36 69 70 syl2anc 
 |-  ( ph -> ( ( N o. T ) ` 1 ) = ( N ` ( T ` 1 ) ) )
72 67 71 eqtrd 
 |-  ( ph -> ( ( F ` N ) ` 1 ) = ( N ` ( T ` 1 ) ) )
73 68 9 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
74 73 a1i 
 |-  ( ph -> 1 e. ( 0 ..^ 3 ) )
75 26 74 ffvelrnd 
 |-  ( ph -> ( T ` 1 ) e. ( 0 ..^ 3 ) )
76 3 75 ffvelrnd 
 |-  ( ph -> ( N ` ( T ` 1 ) ) e. NN )
77 72 76 eqeltrd 
 |-  ( ph -> ( ( F ` N ) ` 1 ) e. NN )
78 4 77 ffvelrnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 1 ) ) e. RR )
79 78 recnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 1 ) ) e. CC )
80 0ne1 
 |-  0 =/= 1
81 80 a1i 
 |-  ( ph -> 0 =/= 1 )
82 2fveq3 
 |-  ( b = 2 -> ( L ` ( ( F ` N ) ` b ) ) = ( L ` ( ( F ` N ) ` 2 ) ) )
83 2ex 
 |-  2 e. _V
84 83 a1i 
 |-  ( ph -> 2 e. _V )
85 32 fveq1d 
 |-  ( ph -> ( ( F ` N ) ` 2 ) = ( ( N o. T ) ` 2 ) )
86 83 tpid3 
 |-  2 e. { 0 , 1 , 2 }
87 86 39 eleqtrrid 
 |-  ( ph -> 2 e. dom T )
88 fvco 
 |-  ( ( Fun T /\ 2 e. dom T ) -> ( ( N o. T ) ` 2 ) = ( N ` ( T ` 2 ) ) )
89 36 87 88 syl2anc 
 |-  ( ph -> ( ( N o. T ) ` 2 ) = ( N ` ( T ` 2 ) ) )
90 85 89 eqtrd 
 |-  ( ph -> ( ( F ` N ) ` 2 ) = ( N ` ( T ` 2 ) ) )
91 86 9 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
92 91 a1i 
 |-  ( ph -> 2 e. ( 0 ..^ 3 ) )
93 26 92 ffvelrnd 
 |-  ( ph -> ( T ` 2 ) e. ( 0 ..^ 3 ) )
94 3 93 ffvelrnd 
 |-  ( ph -> ( N ` ( T ` 2 ) ) e. NN )
95 90 94 eqeltrd 
 |-  ( ph -> ( ( F ` N ) ` 2 ) e. NN )
96 4 95 ffvelrnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 2 ) ) e. RR )
97 96 recnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 2 ) ) e. CC )
98 0ne2 
 |-  0 =/= 2
99 98 a1i 
 |-  ( ph -> 0 =/= 2 )
100 1ne2 
 |-  1 =/= 2
101 100 a1i 
 |-  ( ph -> 1 =/= 2 )
102 48 49 51 53 66 79 81 82 84 97 99 101 prodtp 
 |-  ( ph -> prod_ b e. { 0 , 1 , 2 } ( L ` ( ( F ` N ) ` b ) ) = ( ( ( L ` ( ( F ` N ) ` 0 ) ) x. ( L ` ( ( F ` N ) ` 1 ) ) ) x. ( L ` ( ( F ` N ) ` 2 ) ) ) )
103 2fveq3 
 |-  ( a = 0 -> ( L ` ( N ` a ) ) = ( L ` ( N ` 0 ) ) )
104 2fveq3 
 |-  ( a = 1 -> ( L ` ( N ` a ) ) = ( L ` ( N ` 1 ) ) )
105 3 61 ffvelrnd 
 |-  ( ph -> ( N ` 0 ) e. NN )
106 4 105 ffvelrnd 
 |-  ( ph -> ( L ` ( N ` 0 ) ) e. RR )
107 106 recnd 
 |-  ( ph -> ( L ` ( N ` 0 ) ) e. CC )
108 3 74 ffvelrnd 
 |-  ( ph -> ( N ` 1 ) e. NN )
109 4 108 ffvelrnd 
 |-  ( ph -> ( L ` ( N ` 1 ) ) e. RR )
110 109 recnd 
 |-  ( ph -> ( L ` ( N ` 1 ) ) e. CC )
111 2fveq3 
 |-  ( a = 2 -> ( L ` ( N ` a ) ) = ( L ` ( N ` 2 ) ) )
112 3 92 ffvelrnd 
 |-  ( ph -> ( N ` 2 ) e. NN )
113 4 112 ffvelrnd 
 |-  ( ph -> ( L ` ( N ` 2 ) ) e. RR )
114 113 recnd 
 |-  ( ph -> ( L ` ( N ` 2 ) ) e. CC )
115 103 104 51 53 107 110 81 111 84 114 99 101 prodtp 
 |-  ( ph -> prod_ a e. { 0 , 1 , 2 } ( L ` ( N ` a ) ) = ( ( ( L ` ( N ` 0 ) ) x. ( L ` ( N ` 1 ) ) ) x. ( L ` ( N ` 2 ) ) ) )
116 47 102 115 3eqtr3d 
 |-  ( ph -> ( ( ( L ` ( ( F ` N ) ` 0 ) ) x. ( L ` ( ( F ` N ) ` 1 ) ) ) x. ( L ` ( ( F ` N ) ` 2 ) ) ) = ( ( ( L ` ( N ` 0 ) ) x. ( L ` ( N ` 1 ) ) ) x. ( L ` ( N ` 2 ) ) ) )
117 66 79 97 mulassd 
 |-  ( ph -> ( ( ( L ` ( ( F ` N ) ` 0 ) ) x. ( L ` ( ( F ` N ) ` 1 ) ) ) x. ( L ` ( ( F ` N ) ` 2 ) ) ) = ( ( L ` ( ( F ` N ) ` 0 ) ) x. ( ( L ` ( ( F ` N ) ` 1 ) ) x. ( L ` ( ( F ` N ) ` 2 ) ) ) ) )
118 107 110 114 mulassd 
 |-  ( ph -> ( ( ( L ` ( N ` 0 ) ) x. ( L ` ( N ` 1 ) ) ) x. ( L ` ( N ` 2 ) ) ) = ( ( L ` ( N ` 0 ) ) x. ( ( L ` ( N ` 1 ) ) x. ( L ` ( N ` 2 ) ) ) ) )
119 116 117 118 3eqtr3d 
 |-  ( ph -> ( ( L ` ( ( F ` N ) ` 0 ) ) x. ( ( L ` ( ( F ` N ) ` 1 ) ) x. ( L ` ( ( F ` N ) ` 2 ) ) ) ) = ( ( L ` ( N ` 0 ) ) x. ( ( L ` ( N ` 1 ) ) x. ( L ` ( N ` 2 ) ) ) ) )