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