This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) ) ) ) )