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 𝐹 = ( 𝑐𝑅 ↦ ( 𝑐𝑇 ) )
hgt750lemg.t ( 𝜑𝑇 : ( 0 ..^ 3 ) –1-1-onto→ ( 0 ..^ 3 ) )
hgt750lemg.n ( 𝜑𝑁 : ( 0 ..^ 3 ) ⟶ ℕ )
hgt750lemg.l ( 𝜑𝐿 : ℕ ⟶ ℝ )
hgt750lemg.1 ( 𝜑𝑁𝑅 )
Assertion hgt750lemg ( 𝜑 → ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) · ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) ) ) = ( ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) · ( ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hgt750lemg.f 𝐹 = ( 𝑐𝑅 ↦ ( 𝑐𝑇 ) )
2 hgt750lemg.t ( 𝜑𝑇 : ( 0 ..^ 3 ) –1-1-onto→ ( 0 ..^ 3 ) )
3 hgt750lemg.n ( 𝜑𝑁 : ( 0 ..^ 3 ) ⟶ ℕ )
4 hgt750lemg.l ( 𝜑𝐿 : ℕ ⟶ ℝ )
5 hgt750lemg.1 ( 𝜑𝑁𝑅 )
6 2fveq3 ( 𝑎 = ( 𝑇𝑏 ) → ( 𝐿 ‘ ( 𝑁𝑎 ) ) = ( 𝐿 ‘ ( 𝑁 ‘ ( 𝑇𝑏 ) ) ) )
7 tpfi { 0 , 1 , 2 } ∈ Fin
8 7 a1i ( 𝜑 → { 0 , 1 , 2 } ∈ Fin )
9 fzo0to3tp ( 0 ..^ 3 ) = { 0 , 1 , 2 }
10 f1oeq23 ( ( ( 0 ..^ 3 ) = { 0 , 1 , 2 } ∧ ( 0 ..^ 3 ) = { 0 , 1 , 2 } ) → ( 𝑇 : ( 0 ..^ 3 ) –1-1-onto→ ( 0 ..^ 3 ) ↔ 𝑇 : { 0 , 1 , 2 } –1-1-onto→ { 0 , 1 , 2 } ) )
11 9 9 10 mp2an ( 𝑇 : ( 0 ..^ 3 ) –1-1-onto→ ( 0 ..^ 3 ) ↔ 𝑇 : { 0 , 1 , 2 } –1-1-onto→ { 0 , 1 , 2 } )
12 2 11 sylib ( 𝜑𝑇 : { 0 , 1 , 2 } –1-1-onto→ { 0 , 1 , 2 } )
13 eqidd ( ( 𝜑𝑏 ∈ { 0 , 1 , 2 } ) → ( 𝑇𝑏 ) = ( 𝑇𝑏 ) )
14 4 adantr ( ( 𝜑𝑎 ∈ { 0 , 1 , 2 } ) → 𝐿 : ℕ ⟶ ℝ )
15 3 adantr ( ( 𝜑𝑎 ∈ { 0 , 1 , 2 } ) → 𝑁 : ( 0 ..^ 3 ) ⟶ ℕ )
16 simpr ( ( 𝜑𝑎 ∈ { 0 , 1 , 2 } ) → 𝑎 ∈ { 0 , 1 , 2 } )
17 16 9 eleqtrrdi ( ( 𝜑𝑎 ∈ { 0 , 1 , 2 } ) → 𝑎 ∈ ( 0 ..^ 3 ) )
18 15 17 ffvelrnd ( ( 𝜑𝑎 ∈ { 0 , 1 , 2 } ) → ( 𝑁𝑎 ) ∈ ℕ )
19 14 18 ffvelrnd ( ( 𝜑𝑎 ∈ { 0 , 1 , 2 } ) → ( 𝐿 ‘ ( 𝑁𝑎 ) ) ∈ ℝ )
20 19 recnd ( ( 𝜑𝑎 ∈ { 0 , 1 , 2 } ) → ( 𝐿 ‘ ( 𝑁𝑎 ) ) ∈ ℂ )
21 6 8 12 13 20 fprodf1o ( 𝜑 → ∏ 𝑎 ∈ { 0 , 1 , 2 } ( 𝐿 ‘ ( 𝑁𝑎 ) ) = ∏ 𝑏 ∈ { 0 , 1 , 2 } ( 𝐿 ‘ ( 𝑁 ‘ ( 𝑇𝑏 ) ) ) )
22 1 a1i ( 𝜑𝐹 = ( 𝑐𝑅 ↦ ( 𝑐𝑇 ) ) )
23 simpr ( ( 𝜑𝑐 = 𝑁 ) → 𝑐 = 𝑁 )
24 23 coeq1d ( ( 𝜑𝑐 = 𝑁 ) → ( 𝑐𝑇 ) = ( 𝑁𝑇 ) )
25 f1of ( 𝑇 : ( 0 ..^ 3 ) –1-1-onto→ ( 0 ..^ 3 ) → 𝑇 : ( 0 ..^ 3 ) ⟶ ( 0 ..^ 3 ) )
26 2 25 syl ( 𝜑𝑇 : ( 0 ..^ 3 ) ⟶ ( 0 ..^ 3 ) )
27 ovexd ( 𝜑 → ( 0 ..^ 3 ) ∈ V )
28 26 27 fexd ( 𝜑𝑇 ∈ V )
29 coexg ( ( 𝑁𝑅𝑇 ∈ V ) → ( 𝑁𝑇 ) ∈ V )
30 5 28 29 syl2anc ( 𝜑 → ( 𝑁𝑇 ) ∈ V )
31 22 24 5 30 fvmptd ( 𝜑 → ( 𝐹𝑁 ) = ( 𝑁𝑇 ) )
32 31 adantr ( ( 𝜑𝑏 ∈ { 0 , 1 , 2 } ) → ( 𝐹𝑁 ) = ( 𝑁𝑇 ) )
33 32 fveq1d ( ( 𝜑𝑏 ∈ { 0 , 1 , 2 } ) → ( ( 𝐹𝑁 ) ‘ 𝑏 ) = ( ( 𝑁𝑇 ) ‘ 𝑏 ) )
34 f1ofun ( 𝑇 : ( 0 ..^ 3 ) –1-1-onto→ ( 0 ..^ 3 ) → Fun 𝑇 )
35 2 34 syl ( 𝜑 → Fun 𝑇 )
36 35 adantr ( ( 𝜑𝑏 ∈ { 0 , 1 , 2 } ) → Fun 𝑇 )
37 f1odm ( 𝑇 : { 0 , 1 , 2 } –1-1-onto→ { 0 , 1 , 2 } → dom 𝑇 = { 0 , 1 , 2 } )
38 12 37 syl ( 𝜑 → dom 𝑇 = { 0 , 1 , 2 } )
39 38 eleq2d ( 𝜑 → ( 𝑏 ∈ dom 𝑇𝑏 ∈ { 0 , 1 , 2 } ) )
40 39 biimpar ( ( 𝜑𝑏 ∈ { 0 , 1 , 2 } ) → 𝑏 ∈ dom 𝑇 )
41 fvco ( ( Fun 𝑇𝑏 ∈ dom 𝑇 ) → ( ( 𝑁𝑇 ) ‘ 𝑏 ) = ( 𝑁 ‘ ( 𝑇𝑏 ) ) )
42 36 40 41 syl2anc ( ( 𝜑𝑏 ∈ { 0 , 1 , 2 } ) → ( ( 𝑁𝑇 ) ‘ 𝑏 ) = ( 𝑁 ‘ ( 𝑇𝑏 ) ) )
43 33 42 eqtr2d ( ( 𝜑𝑏 ∈ { 0 , 1 , 2 } ) → ( 𝑁 ‘ ( 𝑇𝑏 ) ) = ( ( 𝐹𝑁 ) ‘ 𝑏 ) )
44 43 fveq2d ( ( 𝜑𝑏 ∈ { 0 , 1 , 2 } ) → ( 𝐿 ‘ ( 𝑁 ‘ ( 𝑇𝑏 ) ) ) = ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 𝑏 ) ) )
45 44 prodeq2dv ( 𝜑 → ∏ 𝑏 ∈ { 0 , 1 , 2 } ( 𝐿 ‘ ( 𝑁 ‘ ( 𝑇𝑏 ) ) ) = ∏ 𝑏 ∈ { 0 , 1 , 2 } ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 𝑏 ) ) )
46 21 45 eqtr2d ( 𝜑 → ∏ 𝑏 ∈ { 0 , 1 , 2 } ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 𝑏 ) ) = ∏ 𝑎 ∈ { 0 , 1 , 2 } ( 𝐿 ‘ ( 𝑁𝑎 ) ) )
47 2fveq3 ( 𝑏 = 0 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 𝑏 ) ) = ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) )
48 2fveq3 ( 𝑏 = 1 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 𝑏 ) ) = ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) )
49 c0ex 0 ∈ V
50 49 a1i ( 𝜑 → 0 ∈ V )
51 1ex 1 ∈ V
52 51 a1i ( 𝜑 → 1 ∈ V )
53 31 fveq1d ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 0 ) = ( ( 𝑁𝑇 ) ‘ 0 ) )
54 49 tpid1 0 ∈ { 0 , 1 , 2 }
55 54 38 eleqtrrid ( 𝜑 → 0 ∈ dom 𝑇 )
56 fvco ( ( Fun 𝑇 ∧ 0 ∈ dom 𝑇 ) → ( ( 𝑁𝑇 ) ‘ 0 ) = ( 𝑁 ‘ ( 𝑇 ‘ 0 ) ) )
57 35 55 56 syl2anc ( 𝜑 → ( ( 𝑁𝑇 ) ‘ 0 ) = ( 𝑁 ‘ ( 𝑇 ‘ 0 ) ) )
58 53 57 eqtrd ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 0 ) = ( 𝑁 ‘ ( 𝑇 ‘ 0 ) ) )
59 54 9 eleqtrri 0 ∈ ( 0 ..^ 3 )
60 59 a1i ( 𝜑 → 0 ∈ ( 0 ..^ 3 ) )
61 26 60 ffvelrnd ( 𝜑 → ( 𝑇 ‘ 0 ) ∈ ( 0 ..^ 3 ) )
62 3 61 ffvelrnd ( 𝜑 → ( 𝑁 ‘ ( 𝑇 ‘ 0 ) ) ∈ ℕ )
63 58 62 eqeltrd ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 0 ) ∈ ℕ )
64 4 63 ffvelrnd ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) ∈ ℝ )
65 64 recnd ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) ∈ ℂ )
66 31 fveq1d ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 1 ) = ( ( 𝑁𝑇 ) ‘ 1 ) )
67 51 tpid2 1 ∈ { 0 , 1 , 2 }
68 67 38 eleqtrrid ( 𝜑 → 1 ∈ dom 𝑇 )
69 fvco ( ( Fun 𝑇 ∧ 1 ∈ dom 𝑇 ) → ( ( 𝑁𝑇 ) ‘ 1 ) = ( 𝑁 ‘ ( 𝑇 ‘ 1 ) ) )
70 35 68 69 syl2anc ( 𝜑 → ( ( 𝑁𝑇 ) ‘ 1 ) = ( 𝑁 ‘ ( 𝑇 ‘ 1 ) ) )
71 66 70 eqtrd ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 1 ) = ( 𝑁 ‘ ( 𝑇 ‘ 1 ) ) )
72 67 9 eleqtrri 1 ∈ ( 0 ..^ 3 )
73 72 a1i ( 𝜑 → 1 ∈ ( 0 ..^ 3 ) )
74 26 73 ffvelrnd ( 𝜑 → ( 𝑇 ‘ 1 ) ∈ ( 0 ..^ 3 ) )
75 3 74 ffvelrnd ( 𝜑 → ( 𝑁 ‘ ( 𝑇 ‘ 1 ) ) ∈ ℕ )
76 71 75 eqeltrd ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 1 ) ∈ ℕ )
77 4 76 ffvelrnd ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) ∈ ℝ )
78 77 recnd ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) ∈ ℂ )
79 0ne1 0 ≠ 1
80 79 a1i ( 𝜑 → 0 ≠ 1 )
81 2fveq3 ( 𝑏 = 2 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 𝑏 ) ) = ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) )
82 2ex 2 ∈ V
83 82 a1i ( 𝜑 → 2 ∈ V )
84 31 fveq1d ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 2 ) = ( ( 𝑁𝑇 ) ‘ 2 ) )
85 82 tpid3 2 ∈ { 0 , 1 , 2 }
86 85 38 eleqtrrid ( 𝜑 → 2 ∈ dom 𝑇 )
87 fvco ( ( Fun 𝑇 ∧ 2 ∈ dom 𝑇 ) → ( ( 𝑁𝑇 ) ‘ 2 ) = ( 𝑁 ‘ ( 𝑇 ‘ 2 ) ) )
88 35 86 87 syl2anc ( 𝜑 → ( ( 𝑁𝑇 ) ‘ 2 ) = ( 𝑁 ‘ ( 𝑇 ‘ 2 ) ) )
89 84 88 eqtrd ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 2 ) = ( 𝑁 ‘ ( 𝑇 ‘ 2 ) ) )
90 85 9 eleqtrri 2 ∈ ( 0 ..^ 3 )
91 90 a1i ( 𝜑 → 2 ∈ ( 0 ..^ 3 ) )
92 26 91 ffvelrnd ( 𝜑 → ( 𝑇 ‘ 2 ) ∈ ( 0 ..^ 3 ) )
93 3 92 ffvelrnd ( 𝜑 → ( 𝑁 ‘ ( 𝑇 ‘ 2 ) ) ∈ ℕ )
94 89 93 eqeltrd ( 𝜑 → ( ( 𝐹𝑁 ) ‘ 2 ) ∈ ℕ )
95 4 94 ffvelrnd ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) ∈ ℝ )
96 95 recnd ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) ∈ ℂ )
97 0ne2 0 ≠ 2
98 97 a1i ( 𝜑 → 0 ≠ 2 )
99 1ne2 1 ≠ 2
100 99 a1i ( 𝜑 → 1 ≠ 2 )
101 47 48 50 52 65 78 80 81 83 96 98 100 prodtp ( 𝜑 → ∏ 𝑏 ∈ { 0 , 1 , 2 } ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 𝑏 ) ) = ( ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) ) )
102 2fveq3 ( 𝑎 = 0 → ( 𝐿 ‘ ( 𝑁𝑎 ) ) = ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) )
103 2fveq3 ( 𝑎 = 1 → ( 𝐿 ‘ ( 𝑁𝑎 ) ) = ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) )
104 3 60 ffvelrnd ( 𝜑 → ( 𝑁 ‘ 0 ) ∈ ℕ )
105 4 104 ffvelrnd ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) ∈ ℝ )
106 105 recnd ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) ∈ ℂ )
107 3 73 ffvelrnd ( 𝜑 → ( 𝑁 ‘ 1 ) ∈ ℕ )
108 4 107 ffvelrnd ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) ∈ ℝ )
109 108 recnd ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) ∈ ℂ )
110 2fveq3 ( 𝑎 = 2 → ( 𝐿 ‘ ( 𝑁𝑎 ) ) = ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) )
111 3 91 ffvelrnd ( 𝜑 → ( 𝑁 ‘ 2 ) ∈ ℕ )
112 4 111 ffvelrnd ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) ∈ ℝ )
113 112 recnd ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) ∈ ℂ )
114 102 103 50 52 106 109 80 110 83 113 98 100 prodtp ( 𝜑 → ∏ 𝑎 ∈ { 0 , 1 , 2 } ( 𝐿 ‘ ( 𝑁𝑎 ) ) = ( ( ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) ) )
115 46 101 114 3eqtr3d ( 𝜑 → ( ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) ) = ( ( ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) ) )
116 65 78 96 mulassd ( 𝜑 → ( ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) ) = ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) · ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) ) ) )
117 106 109 113 mulassd ( 𝜑 → ( ( ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) ) = ( ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) · ( ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) ) ) )
118 115 116 117 3eqtr3d ( 𝜑 → ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 0 ) ) · ( ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 1 ) ) · ( 𝐿 ‘ ( ( 𝐹𝑁 ) ‘ 2 ) ) ) ) = ( ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) · ( ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) · ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) ) ) )