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