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 \in R ⟼ c \circ T)$
	hgt750lemg.t	$⊢ φ \to T : (0 ..^3) \underset{1-1 onto}{⟶} (0 ..^3)$
	hgt750lemg.n	$⊢ φ \to N : (0 ..^3) ⟶ ℕ$
	hgt750lemg.l	$⊢ φ \to L : ℕ ⟶ ℝ$
	hgt750lemg.1	$⊢ φ \to N \in R$
Assertion	hgt750lemg	$⊢ φ \to L (F (N) (0)) L (F (N) (1)) L (F (N) (2)) = L (N (0)) L (N (1)) L (N (2))$

Proof

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

Metamath Proof Explorer

Theorem hgt750lemg

Proof