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 26 27 fexd 
 |-  ( ph -> T e. _V )
29 coexg 
 |-  ( ( N e. R /\ T e. _V ) -> ( N o. T ) e. _V )
30 5 28 29 syl2anc 
 |-  ( ph -> ( N o. T ) e. _V )
31 22 24 5 30 fvmptd 
 |-  ( ph -> ( F ` N ) = ( N o. T ) )
32 31 adantr 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( F ` N ) = ( N o. T ) )
33 32 fveq1d 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( ( F ` N ) ` b ) = ( ( N o. T ) ` b ) )
34 f1ofun 
 |-  ( T : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) -> Fun T )
35 2 34 syl 
 |-  ( ph -> Fun T )
36 35 adantr 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> Fun T )
37 f1odm 
 |-  ( T : { 0 , 1 , 2 } -1-1-onto-> { 0 , 1 , 2 } -> dom T = { 0 , 1 , 2 } )
38 12 37 syl 
 |-  ( ph -> dom T = { 0 , 1 , 2 } )
39 38 eleq2d 
 |-  ( ph -> ( b e. dom T <-> b e. { 0 , 1 , 2 } ) )
40 39 biimpar 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> b e. dom T )
41 fvco 
 |-  ( ( Fun T /\ b e. dom T ) -> ( ( N o. T ) ` b ) = ( N ` ( T ` b ) ) )
42 36 40 41 syl2anc 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( ( N o. T ) ` b ) = ( N ` ( T ` b ) ) )
43 33 42 eqtr2d 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( N ` ( T ` b ) ) = ( ( F ` N ) ` b ) )
44 43 fveq2d 
 |-  ( ( ph /\ b e. { 0 , 1 , 2 } ) -> ( L ` ( N ` ( T ` b ) ) ) = ( L ` ( ( F ` N ) ` b ) ) )
45 44 prodeq2dv 
 |-  ( ph -> prod_ b e. { 0 , 1 , 2 } ( L ` ( N ` ( T ` b ) ) ) = prod_ b e. { 0 , 1 , 2 } ( L ` ( ( F ` N ) ` b ) ) )
46 21 45 eqtr2d 
 |-  ( ph -> prod_ b e. { 0 , 1 , 2 } ( L ` ( ( F ` N ) ` b ) ) = prod_ a e. { 0 , 1 , 2 } ( L ` ( N ` a ) ) )
47 2fveq3 
 |-  ( b = 0 -> ( L ` ( ( F ` N ) ` b ) ) = ( L ` ( ( F ` N ) ` 0 ) ) )
48 2fveq3 
 |-  ( b = 1 -> ( L ` ( ( F ` N ) ` b ) ) = ( L ` ( ( F ` N ) ` 1 ) ) )
49 c0ex 
 |-  0 e. _V
50 49 a1i 
 |-  ( ph -> 0 e. _V )
51 1ex 
 |-  1 e. _V
52 51 a1i 
 |-  ( ph -> 1 e. _V )
53 31 fveq1d 
 |-  ( ph -> ( ( F ` N ) ` 0 ) = ( ( N o. T ) ` 0 ) )
54 49 tpid1 
 |-  0 e. { 0 , 1 , 2 }
55 54 38 eleqtrrid 
 |-  ( ph -> 0 e. dom T )
56 fvco 
 |-  ( ( Fun T /\ 0 e. dom T ) -> ( ( N o. T ) ` 0 ) = ( N ` ( T ` 0 ) ) )
57 35 55 56 syl2anc 
 |-  ( ph -> ( ( N o. T ) ` 0 ) = ( N ` ( T ` 0 ) ) )
58 53 57 eqtrd 
 |-  ( ph -> ( ( F ` N ) ` 0 ) = ( N ` ( T ` 0 ) ) )
59 54 9 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
60 59 a1i 
 |-  ( ph -> 0 e. ( 0 ..^ 3 ) )
61 26 60 ffvelrnd 
 |-  ( ph -> ( T ` 0 ) e. ( 0 ..^ 3 ) )
62 3 61 ffvelrnd 
 |-  ( ph -> ( N ` ( T ` 0 ) ) e. NN )
63 58 62 eqeltrd 
 |-  ( ph -> ( ( F ` N ) ` 0 ) e. NN )
64 4 63 ffvelrnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 0 ) ) e. RR )
65 64 recnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 0 ) ) e. CC )
66 31 fveq1d 
 |-  ( ph -> ( ( F ` N ) ` 1 ) = ( ( N o. T ) ` 1 ) )
67 51 tpid2 
 |-  1 e. { 0 , 1 , 2 }
68 67 38 eleqtrrid 
 |-  ( ph -> 1 e. dom T )
69 fvco 
 |-  ( ( Fun T /\ 1 e. dom T ) -> ( ( N o. T ) ` 1 ) = ( N ` ( T ` 1 ) ) )
70 35 68 69 syl2anc 
 |-  ( ph -> ( ( N o. T ) ` 1 ) = ( N ` ( T ` 1 ) ) )
71 66 70 eqtrd 
 |-  ( ph -> ( ( F ` N ) ` 1 ) = ( N ` ( T ` 1 ) ) )
72 67 9 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
73 72 a1i 
 |-  ( ph -> 1 e. ( 0 ..^ 3 ) )
74 26 73 ffvelrnd 
 |-  ( ph -> ( T ` 1 ) e. ( 0 ..^ 3 ) )
75 3 74 ffvelrnd 
 |-  ( ph -> ( N ` ( T ` 1 ) ) e. NN )
76 71 75 eqeltrd 
 |-  ( ph -> ( ( F ` N ) ` 1 ) e. NN )
77 4 76 ffvelrnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 1 ) ) e. RR )
78 77 recnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 1 ) ) e. CC )
79 0ne1 
 |-  0 =/= 1
80 79 a1i 
 |-  ( ph -> 0 =/= 1 )
81 2fveq3 
 |-  ( b = 2 -> ( L ` ( ( F ` N ) ` b ) ) = ( L ` ( ( F ` N ) ` 2 ) ) )
82 2ex 
 |-  2 e. _V
83 82 a1i 
 |-  ( ph -> 2 e. _V )
84 31 fveq1d 
 |-  ( ph -> ( ( F ` N ) ` 2 ) = ( ( N o. T ) ` 2 ) )
85 82 tpid3 
 |-  2 e. { 0 , 1 , 2 }
86 85 38 eleqtrrid 
 |-  ( ph -> 2 e. dom T )
87 fvco 
 |-  ( ( Fun T /\ 2 e. dom T ) -> ( ( N o. T ) ` 2 ) = ( N ` ( T ` 2 ) ) )
88 35 86 87 syl2anc 
 |-  ( ph -> ( ( N o. T ) ` 2 ) = ( N ` ( T ` 2 ) ) )
89 84 88 eqtrd 
 |-  ( ph -> ( ( F ` N ) ` 2 ) = ( N ` ( T ` 2 ) ) )
90 85 9 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
91 90 a1i 
 |-  ( ph -> 2 e. ( 0 ..^ 3 ) )
92 26 91 ffvelrnd 
 |-  ( ph -> ( T ` 2 ) e. ( 0 ..^ 3 ) )
93 3 92 ffvelrnd 
 |-  ( ph -> ( N ` ( T ` 2 ) ) e. NN )
94 89 93 eqeltrd 
 |-  ( ph -> ( ( F ` N ) ` 2 ) e. NN )
95 4 94 ffvelrnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 2 ) ) e. RR )
96 95 recnd 
 |-  ( ph -> ( L ` ( ( F ` N ) ` 2 ) ) e. CC )
97 0ne2 
 |-  0 =/= 2
98 97 a1i 
 |-  ( ph -> 0 =/= 2 )
99 1ne2 
 |-  1 =/= 2
100 99 a1i 
 |-  ( ph -> 1 =/= 2 )
101 47 48 50 52 65 78 80 81 83 96 98 100 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 ) ) ) )
102 2fveq3 
 |-  ( a = 0 -> ( L ` ( N ` a ) ) = ( L ` ( N ` 0 ) ) )
103 2fveq3 
 |-  ( a = 1 -> ( L ` ( N ` a ) ) = ( L ` ( N ` 1 ) ) )
104 3 60 ffvelrnd 
 |-  ( ph -> ( N ` 0 ) e. NN )
105 4 104 ffvelrnd 
 |-  ( ph -> ( L ` ( N ` 0 ) ) e. RR )
106 105 recnd 
 |-  ( ph -> ( L ` ( N ` 0 ) ) e. CC )
107 3 73 ffvelrnd 
 |-  ( ph -> ( N ` 1 ) e. NN )
108 4 107 ffvelrnd 
 |-  ( ph -> ( L ` ( N ` 1 ) ) e. RR )
109 108 recnd 
 |-  ( ph -> ( L ` ( N ` 1 ) ) e. CC )
110 2fveq3 
 |-  ( a = 2 -> ( L ` ( N ` a ) ) = ( L ` ( N ` 2 ) ) )
111 3 91 ffvelrnd 
 |-  ( ph -> ( N ` 2 ) e. NN )
112 4 111 ffvelrnd 
 |-  ( ph -> ( L ` ( N ` 2 ) ) e. RR )
113 112 recnd 
 |-  ( ph -> ( L ` ( N ` 2 ) ) e. CC )
114 102 103 50 52 106 109 80 110 83 113 98 100 prodtp 
 |-  ( ph -> prod_ a e. { 0 , 1 , 2 } ( L ` ( N ` a ) ) = ( ( ( L ` ( N ` 0 ) ) x. ( L ` ( N ` 1 ) ) ) x. ( L ` ( N ` 2 ) ) ) )
115 46 101 114 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 ) ) ) )
116 65 78 96 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 ) ) ) ) )
117 106 109 113 mulassd 
 |-  ( ph -> ( ( ( L ` ( N ` 0 ) ) x. ( L ` ( N ` 1 ) ) ) x. ( L ` ( N ` 2 ) ) ) = ( ( L ` ( N ` 0 ) ) x. ( ( L ` ( N ` 1 ) ) x. ( L ` ( N ` 2 ) ) ) ) )
118 115 116 117 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 ) ) ) ) )