Metamath Proof Explorer


Theorem evlsvvvallem2

Description: Lemma for theorems using evlsvvval . (Contributed by SN, 8-Mar-2025)

Ref Expression
Hypotheses evlsvvvallem2.d D = h 0 I | h -1 Fin
evlsvvvallem2.p P = I mPoly U
evlsvvvallem2.u U = S 𝑠 R
evlsvvvallem2.b B = Base P
evlsvvvallem2.k K = Base S
evlsvvvallem2.m M = mulGrp S
evlsvvvallem2.w × ˙ = M
evlsvvvallem2.x · ˙ = S
evlsvvvallem2.i φ I V
evlsvvvallem2.s φ S CRing
evlsvvvallem2.r φ R SubRing S
evlsvvvallem2.f φ F B
evlsvvvallem2.a φ A K I
Assertion evlsvvvallem2 φ finSupp 0 S b D F b · ˙ M v I b v × ˙ A v

Proof

Step Hyp Ref Expression
1 evlsvvvallem2.d D = h 0 I | h -1 Fin
2 evlsvvvallem2.p P = I mPoly U
3 evlsvvvallem2.u U = S 𝑠 R
4 evlsvvvallem2.b B = Base P
5 evlsvvvallem2.k K = Base S
6 evlsvvvallem2.m M = mulGrp S
7 evlsvvvallem2.w × ˙ = M
8 evlsvvvallem2.x · ˙ = S
9 evlsvvvallem2.i φ I V
10 evlsvvvallem2.s φ S CRing
11 evlsvvvallem2.r φ R SubRing S
12 evlsvvvallem2.f φ F B
13 evlsvvvallem2.a φ A K I
14 ovex 0 I V
15 1 14 rabex2 D V
16 15 mptex b D F b · ˙ M v I b v × ˙ A v V
17 16 a1i φ b D F b · ˙ M v I b v × ˙ A v V
18 fvexd φ 0 S V
19 funmpt Fun b D F b · ˙ M v I b v × ˙ A v
20 19 a1i φ Fun b D F b · ˙ M v I b v × ˙ A v
21 eqid 0 U = 0 U
22 2 4 21 12 mplelsfi φ finSupp 0 U F
23 eqid Base U = Base U
24 2 23 4 1 12 mplelf φ F : D Base U
25 ssidd φ F supp 0 U F supp 0 U
26 fvexd φ 0 U V
27 24 25 12 26 suppssrg φ b D supp 0 U F F b = 0 U
28 eqid 0 S = 0 S
29 3 28 subrg0 R SubRing S 0 S = 0 U
30 11 29 syl φ 0 S = 0 U
31 30 eqcomd φ 0 U = 0 S
32 31 adantr φ b D supp 0 U F 0 U = 0 S
33 27 32 eqtrd φ b D supp 0 U F F b = 0 S
34 33 oveq1d φ b D supp 0 U F F b · ˙ M v I b v × ˙ A v = 0 S · ˙ M v I b v × ˙ A v
35 10 crngringd φ S Ring
36 35 adantr φ b D supp 0 U F S Ring
37 eldifi b D supp 0 U F b D
38 9 adantr φ b D I V
39 10 adantr φ b D S CRing
40 13 adantr φ b D A K I
41 simpr φ b D b D
42 1 5 6 7 38 39 40 41 evlsvvvallem φ b D M v I b v × ˙ A v K
43 37 42 sylan2 φ b D supp 0 U F M v I b v × ˙ A v K
44 5 8 28 36 43 ringlzd φ b D supp 0 U F 0 S · ˙ M v I b v × ˙ A v = 0 S
45 34 44 eqtrd φ b D supp 0 U F F b · ˙ M v I b v × ˙ A v = 0 S
46 15 a1i φ D V
47 45 46 suppss2 φ b D F b · ˙ M v I b v × ˙ A v supp 0 S F supp 0 U
48 17 18 20 22 47 fsuppsssuppgd φ finSupp 0 S b D F b · ˙ M v I b v × ˙ A v