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

Metamath Proof Explorer

Theorem evlsevl

Description: Evaluation in a subring is the same as evaluation in the ring itself. (Contributed by SN, 9-Feb-2025)

Ref Expression
Hypotheses evlsevl.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsevl.o ⊢ 𝑂 = ( 𝐼 eval 𝑆 )
evlsevl.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
evlsevl.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsevl.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
evlsevl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlsevl.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsevl.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlsevl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion evlsevl ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( 𝑂 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 evlsevl.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsevl.o ⊢ 𝑂 = ( 𝐼 eval 𝑆 )
3 evlsevl.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
4 evlsevl.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evlsevl.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
6 evlsevl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7 evlsevl.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
8 evlsevl.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
9 evlsevl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10 eqid ⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) )
11 sneq ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑏 ) → { 𝑥 } = { ( 𝐹 ‘ 𝑏 ) } )
12 11 xpeq2d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑏 ) → ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) = ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) )
13 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
14 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
15 3 13 5 14 9 mplelf ⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑈 ) )
16 15 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ 𝑏 ) ∈ ( Base ‘ 𝑈 ) )
17 4 subrgbas ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
18 8 17 syl ⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑅 = ( Base ‘ 𝑈 ) )
20 16 19 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝑅 )
21 ovexd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ∈ V )
22 snex ⊢ { ( 𝐹 ‘ 𝑏 ) } ∈ V
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → { ( 𝐹 ‘ 𝑏 ) } ∈ V )
24 21 23 xpexd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ∈ V )
25 10 12 20 24 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) = ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) )
26 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) )
27 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
28 27 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
29 8 28 syl ⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
31 30 20 sseldd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
32 26 12 31 24 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) = ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) )
33 25 32 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) )
34 33 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
35 34 mpteq2dva ⊢ ( 𝜑 → ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) = ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) )
36 35 oveq2d ⊢ ( 𝜑 → ( ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) = ( ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
37 eqid ⊢ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) = ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) )
38 eqid ⊢ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) = ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
39 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
40 eqid ⊢ ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) = ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
41 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) )
42 1 3 5 14 27 4 37 38 39 40 10 41 6 7 8 9 evlsvval ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
43 2 27 evlval ⊢ 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ ( Base ‘ 𝑆 ) )
44 43 fveq1i ⊢ ( 𝑂 ‘ 𝐹 ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ ( Base ‘ 𝑆 ) ) ‘ 𝐹 )
45 eqid ⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ ( Base ‘ 𝑆 ) ) = ( ( 𝐼 evalSub 𝑆 ) ‘ ( Base ‘ 𝑆 ) )
46 eqid ⊢ ( 𝐼 mPoly ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) ) = ( 𝐼 mPoly ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) )
47 eqid ⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) ) )
48 eqid ⊢ ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) = ( 𝑆 ↾s ( Base ‘ 𝑆 ) )
49 7 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
50 27 subrgid ⊢ ( 𝑆 ∈ Ring → ( Base ‘ 𝑆 ) ∈ ( SubRing ‘ 𝑆 ) )
51 49 50 syl ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) ∈ ( SubRing ‘ 𝑆 ) )
52 eqid ⊢ ( 𝐼 mPoly 𝑆 ) = ( 𝐼 mPoly 𝑆 )
53 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) )
54 3 4 5 52 53 6 8 9 mplsubrgcl ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) )
55 27 ressid ⊢ ( 𝑆 ∈ CRing → ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) = 𝑆 )
56 7 55 syl ⊢ ( 𝜑 → ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) = 𝑆 )
57 56 oveq2d ⊢ ( 𝜑 → ( 𝐼 mPoly ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) ) = ( 𝐼 mPoly 𝑆 ) )
58 57 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) )
59 54 58 eleqtrrd ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) ) ) )
60 45 46 47 14 27 48 37 38 39 40 26 41 6 7 51 59 evlsvval ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ ( Base ‘ 𝑆 ) ) ‘ 𝐹 ) = ( ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
61 44 60 eqtrid ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) = ( ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
62 36 42 61 3eqtr4d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( 𝑂 ‘ 𝐹 ) )