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

Metamath Proof Explorer

Theorem evlsvvvallem

Description: Lemma for evlsvvval akin to psrbagev2 . (Contributed by SN, 6-Mar-2025)

Ref Expression
Hypotheses evlsvvvallem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
evlsvvvallem.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
evlsvvvallem.m ⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
evlsvvvallem.w ⊢ ↑ = ( .g ‘ 𝑀 )
evlsvvvallem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlsvvvallem.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsvvvallem.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
evlsvvvallem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
Assertion evlsvvvallem ( 𝜑 → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 evlsvvvallem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2 evlsvvvallem.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 evlsvvvallem.m ⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
4 evlsvvvallem.w ⊢ ↑ = ( .g ‘ 𝑀 )
5 evlsvvvallem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 evlsvvvallem.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
7 evlsvvvallem.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
8 evlsvvvallem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
9 3 2 mgpbas ⊢ 𝐾 = ( Base ‘ 𝑀 )
10 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
11 3 10 ringidval ⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑀 )
12 3 crngmgp ⊢ ( 𝑆 ∈ CRing → 𝑀 ∈ CMnd )
13 6 12 syl ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
14 6 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
15 3 ringmgp ⊢ ( 𝑆 ∈ Ring → 𝑀 ∈ Mnd )
16 14 15 syl ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → 𝑀 ∈ Mnd )
18 1 psrbagf ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 : 𝐼 ⟶ ℕ0 )
19 8 18 syl ⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ ℕ0 )
20 19 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝐵 ‘ 𝑣 ) ∈ ℕ0 )
21 elmapi ⊢ ( 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐾 )
22 7 21 syl ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐾 )
23 22 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 )
24 9 4 17 20 23 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ∈ 𝐾 )
25 24 fmpttd ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) : 𝐼 ⟶ 𝐾 )
26 5 mptexd ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ∈ V )
27 fvexd ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ V )
28 25 ffund ⊢ ( 𝜑 → Fun ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
29 1 psrbagfsupp ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 finSupp 0 )
30 8 29 syl ⊢ ( 𝜑 → 𝐵 finSupp 0 )
31 ssidd ⊢ ( 𝜑 → ( 𝐵 supp 0 ) ⊆ ( 𝐵 supp 0 ) )
32 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
33 19 31 5 32 suppssr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝐵 ‘ 𝑣 ) = 0 )
34 33 oveq1d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) = ( 0 ↑ ( 𝐴 ‘ 𝑣 ) ) )
35 eldifi ⊢ ( 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) → 𝑣 ∈ 𝐼 )
36 35 23 sylan2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 )
37 9 11 4 mulg0 ⊢ ( ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 → ( 0 ↑ ( 𝐴 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
38 36 37 syl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 0 ↑ ( 𝐴 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
39 34 38 eqtrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
40 39 5 suppss2 ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) supp ( 1r ‘ 𝑆 ) ) ⊆ ( 𝐵 supp 0 ) )
41 26 27 28 30 40 fsuppsssuppgd ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) finSupp ( 1r ‘ 𝑆 ) )
42 9 11 13 5 25 41 gsumcl ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )