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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 0 , 1 , 2 } ) → ( 𝑁 ‘ 𝑎 ) ∈ ℕ )
19	14 18	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 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	ffvelcdmd	⊢ ( 𝜑 → ( 𝑇 ‘ 0 ) ∈ ( 0 ..^ 3 ) )
62	3 61	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑇 ‘ 0 ) ) ∈ ℕ )
63	58 62	eqeltrd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) ‘ 0 ) ∈ ℕ )
64	4 63	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹 ‘ 𝑁 ) ‘ 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	ffvelcdmd	⊢ ( 𝜑 → ( 𝑇 ‘ 1 ) ∈ ( 0 ..^ 3 ) )
75	3 74	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑇 ‘ 1 ) ) ∈ ℕ )
76	71 75	eqeltrd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) ‘ 1 ) ∈ ℕ )
77	4 76	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹 ‘ 𝑁 ) ‘ 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	ffvelcdmd	⊢ ( 𝜑 → ( 𝑇 ‘ 2 ) ∈ ( 0 ..^ 3 ) )
93	3 92	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑇 ‘ 2 ) ) ∈ ℕ )
94	89 93	eqeltrd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) ‘ 2 ) ∈ ℕ )
95	4 94	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ ( ( 𝐹 ‘ 𝑁 ) ‘ 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	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ 0 ) ∈ ℕ )
105	4 104	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) ∈ ℝ )
106	105	recnd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 0 ) ) ∈ ℂ )
107	3 73	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ 1 ) ∈ ℕ )
108	4 107	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) ∈ ℝ )
109	108	recnd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 1 ) ) ∈ ℂ )
110		2fveq3	⊢ ( 𝑎 = 2 → ( 𝐿 ‘ ( 𝑁 ‘ 𝑎 ) ) = ( 𝐿 ‘ ( 𝑁 ‘ 2 ) ) )
111	3 91	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ 2 ) ∈ ℕ )
112	4 111	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ‘ 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 ) ) ) ) )