Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  evls1fpws Structured version   Visualization version   GIF version

Theorem evls1fpws 32589
Description: Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.)
Hypotheses
Ref Expression
ressply1evl.q 𝑄 = (𝑆 evalSub1 𝑅)
ressply1evl.k 𝐾 = (Base‘𝑆)
ressply1evl.w 𝑊 = (Poly1𝑈)
ressply1evl.u 𝑈 = (𝑆s 𝑅)
ressply1evl.b 𝐵 = (Base‘𝑊)
evls1fpws.s (𝜑𝑆 ∈ CRing)
evls1fpws.r (𝜑𝑅 ∈ (SubRing‘𝑆))
evls1fpws.y (𝜑𝑀𝐵)
evls1fpws.1 · = (.r𝑆)
evls1fpws.2 = (.g‘(mulGrp‘𝑆))
evls1fpws.a 𝐴 = (coe1𝑀)
Assertion
Ref Expression
evls1fpws (𝜑 → (𝑄𝑀) = (𝑥𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑘 𝑥))))))
Distinct variable groups:   · ,𝑘,𝑥   𝐴,𝑘,𝑥   𝐵,𝑘   𝑘,𝐾,𝑥   𝑘,𝑀   𝑄,𝑘,𝑥   𝑆,𝑘,𝑥   𝑈,𝑘,𝑥   𝑘,𝑊,𝑥   𝜑,𝑘,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥,𝑘)   (𝑥,𝑘)   𝑀(𝑥)

Proof of Theorem evls1fpws
Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evls1fpws.r . . . . 5 (𝜑𝑅 ∈ (SubRing‘𝑆))
2 ressply1evl.u . . . . . 6 𝑈 = (𝑆s 𝑅)
32subrgring 20343 . . . . 5 (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
41, 3syl 17 . . . 4 (𝜑𝑈 ∈ Ring)
5 evls1fpws.y . . . 4 (𝜑𝑀𝐵)
6 ressply1evl.w . . . . 5 𝑊 = (Poly1𝑈)
7 eqid 2733 . . . . 5 (var1𝑈) = (var1𝑈)
8 ressply1evl.b . . . . 5 𝐵 = (Base‘𝑊)
9 eqid 2733 . . . . 5 ( ·𝑠𝑊) = ( ·𝑠𝑊)
10 eqid 2733 . . . . 5 (mulGrp‘𝑊) = (mulGrp‘𝑊)
11 eqid 2733 . . . . 5 (.g‘(mulGrp‘𝑊)) = (.g‘(mulGrp‘𝑊))
12 evls1fpws.a . . . . 5 𝐴 = (coe1𝑀)
136, 7, 8, 9, 10, 11, 12ply1coe 21789 . . . 4 ((𝑈 ∈ Ring ∧ 𝑀𝐵) → 𝑀 = (𝑊 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))))))
144, 5, 13syl2anc 585 . . 3 (𝜑𝑀 = (𝑊 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))))))
1514fveq2d 6885 . 2 (𝜑 → (𝑄𝑀) = (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))))
16 ressply1evl.q . . . 4 𝑄 = (𝑆 evalSub1 𝑅)
17 ressply1evl.k . . . 4 𝐾 = (Base‘𝑆)
18 eqid 2733 . . . 4 (0g𝑊) = (0g𝑊)
19 eqid 2733 . . . 4 (𝑆s 𝐾) = (𝑆s 𝐾)
20 evls1fpws.s . . . 4 (𝜑𝑆 ∈ CRing)
216ply1lmod 21745 . . . . . . 7 (𝑈 ∈ Ring → 𝑊 ∈ LMod)
224, 21syl 17 . . . . . 6 (𝜑𝑊 ∈ LMod)
2322adantr 482 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝑊 ∈ LMod)
24 eqid 2733 . . . . . . . 8 (Base‘𝑈) = (Base‘𝑈)
2512, 8, 6, 24coe1fvalcl 21705 . . . . . . 7 ((𝑀𝐵𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ (Base‘𝑈))
265, 25sylan 581 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ (Base‘𝑈))
276ply1sca 21746 . . . . . . . . 9 (𝑈 ∈ Ring → 𝑈 = (Scalar‘𝑊))
284, 27syl 17 . . . . . . . 8 (𝜑𝑈 = (Scalar‘𝑊))
2928fveq2d 6885 . . . . . . 7 (𝜑 → (Base‘𝑈) = (Base‘(Scalar‘𝑊)))
3029adantr 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (Base‘𝑈) = (Base‘(Scalar‘𝑊)))
3126, 30eleqtrd 2836 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ (Base‘(Scalar‘𝑊)))
3210, 8mgpbas 19976 . . . . . 6 𝐵 = (Base‘(mulGrp‘𝑊))
336ply1ring 21741 . . . . . . . . 9 (𝑈 ∈ Ring → 𝑊 ∈ Ring)
344, 33syl 17 . . . . . . . 8 (𝜑𝑊 ∈ Ring)
3534adantr 482 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑊 ∈ Ring)
3610ringmgp 20044 . . . . . . 7 (𝑊 ∈ Ring → (mulGrp‘𝑊) ∈ Mnd)
3735, 36syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (mulGrp‘𝑊) ∈ Mnd)
38 simpr 486 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
394adantr 482 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑈 ∈ Ring)
407, 6, 8vr1cl 21710 . . . . . . 7 (𝑈 ∈ Ring → (var1𝑈) ∈ 𝐵)
4139, 40syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (var1𝑈) ∈ 𝐵)
4232, 11, 37, 38, 41mulgnn0cld 18960 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)) ∈ 𝐵)
43 eqid 2733 . . . . . 6 (Scalar‘𝑊) = (Scalar‘𝑊)
44 eqid 2733 . . . . . 6 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
458, 43, 9, 44lmodvscl 20466 . . . . 5 ((𝑊 ∈ LMod ∧ (𝐴𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)) ∈ 𝐵) → ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))) ∈ 𝐵)
4623, 31, 42, 45syl3anc 1372 . . . 4 ((𝜑𝑘 ∈ ℕ0) → ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))) ∈ 𝐵)
47 ssidd 4003 . . . 4 (𝜑 → ℕ0 ⊆ ℕ0)
48 fvexd 6896 . . . . 5 (𝜑 → (0g𝑊) ∈ V)
49 fveq2 6881 . . . . . 6 (𝑘 = 𝑗 → (𝐴𝑘) = (𝐴𝑗))
50 oveq1 7403 . . . . . 6 (𝑘 = 𝑗 → (𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)) = (𝑗(.g‘(mulGrp‘𝑊))(var1𝑈)))
5149, 50oveq12d 7414 . . . . 5 (𝑘 = 𝑗 → ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))) = ((𝐴𝑗)( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))))
52 eqid 2733 . . . . . . . 8 (0g𝑈) = (0g𝑈)
5312, 8, 6, 52coe1ae0 21709 . . . . . . 7 (𝑀𝐵 → ∃𝑖 ∈ ℕ0𝑗 ∈ ℕ0 (𝑖 < 𝑗 → (𝐴𝑗) = (0g𝑈)))
545, 53syl 17 . . . . . 6 (𝜑 → ∃𝑖 ∈ ℕ0𝑗 ∈ ℕ0 (𝑖 < 𝑗 → (𝐴𝑗) = (0g𝑈)))
55 simpr 486 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → (𝐴𝑗) = (0g𝑈))
5628ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → 𝑈 = (Scalar‘𝑊))
5756fveq2d 6885 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → (0g𝑈) = (0g‘(Scalar‘𝑊)))
5855, 57eqtrd 2773 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → (𝐴𝑗) = (0g‘(Scalar‘𝑊)))
5958oveq1d 7411 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → ((𝐴𝑗)( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))))
6022ad3antrrr 729 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → 𝑊 ∈ LMod)
6134, 36syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (mulGrp‘𝑊) ∈ Mnd)
6261adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (mulGrp‘𝑊) ∈ Mnd)
63 simpr 486 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
644, 40syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (var1𝑈) ∈ 𝐵)
6564adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (var1𝑈) ∈ 𝐵)
6632, 11, 62, 63, 65mulgnn0cld 18960 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑗(.g‘(mulGrp‘𝑊))(var1𝑈)) ∈ 𝐵)
6766ad4ant13 750 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → (𝑗(.g‘(mulGrp‘𝑊))(var1𝑈)) ∈ 𝐵)
68 eqid 2733 . . . . . . . . . . . . 13 (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
698, 43, 9, 68, 18lmod0vs 20482 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ (𝑗(.g‘(mulGrp‘𝑊))(var1𝑈)) ∈ 𝐵) → ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = (0g𝑊))
7060, 67, 69syl2anc 585 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = (0g𝑊))
7159, 70eqtrd 2773 . . . . . . . . . 10 ((((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) ∧ (𝐴𝑗) = (0g𝑈)) → ((𝐴𝑗)( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = (0g𝑊))
7271ex 414 . . . . . . . . 9 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) → ((𝐴𝑗) = (0g𝑈) → ((𝐴𝑗)( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = (0g𝑊)))
7372imim2d 57 . . . . . . . 8 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0) → ((𝑖 < 𝑗 → (𝐴𝑗) = (0g𝑈)) → (𝑖 < 𝑗 → ((𝐴𝑗)( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = (0g𝑊))))
7473ralimdva 3168 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (∀𝑗 ∈ ℕ0 (𝑖 < 𝑗 → (𝐴𝑗) = (0g𝑈)) → ∀𝑗 ∈ ℕ0 (𝑖 < 𝑗 → ((𝐴𝑗)( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = (0g𝑊))))
7574reximdva 3169 . . . . . 6 (𝜑 → (∃𝑖 ∈ ℕ0𝑗 ∈ ℕ0 (𝑖 < 𝑗 → (𝐴𝑗) = (0g𝑈)) → ∃𝑖 ∈ ℕ0𝑗 ∈ ℕ0 (𝑖 < 𝑗 → ((𝐴𝑗)( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = (0g𝑊))))
7654, 75mpd 15 . . . . 5 (𝜑 → ∃𝑖 ∈ ℕ0𝑗 ∈ ℕ0 (𝑖 < 𝑗 → ((𝐴𝑗)( ·𝑠𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1𝑈))) = (0g𝑊)))
7748, 46, 51, 76mptnn0fsuppd 13950 . . . 4 (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))) finSupp (0g𝑊))
7816, 17, 6, 18, 2, 19, 8, 20, 1, 46, 47, 77evls1gsumadd 21812 . . 3 (𝜑 → (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))) = ((𝑆s 𝐾) Σg (𝑘 ∈ ℕ0 ↦ (𝑄‘((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))))
7916, 17, 19, 2, 6evls1rhm 21810 . . . . . . . . 9 ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom (𝑆s 𝐾)))
8020, 1, 79syl2anc 585 . . . . . . . 8 (𝜑𝑄 ∈ (𝑊 RingHom (𝑆s 𝐾)))
8180adantr 482 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑄 ∈ (𝑊 RingHom (𝑆s 𝐾)))
82 eqid 2733 . . . . . . . . . 10 (algSc‘𝑊) = (algSc‘𝑊)
8382, 43, 34, 22, 44, 8asclf 21407 . . . . . . . . 9 (𝜑 → (algSc‘𝑊):(Base‘(Scalar‘𝑊))⟶𝐵)
8483adantr 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (algSc‘𝑊):(Base‘(Scalar‘𝑊))⟶𝐵)
8584, 31ffvelcdmd 7075 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((algSc‘𝑊)‘(𝐴𝑘)) ∈ 𝐵)
86 eqid 2733 . . . . . . . 8 (.r𝑊) = (.r𝑊)
87 eqid 2733 . . . . . . . 8 (.r‘(𝑆s 𝐾)) = (.r‘(𝑆s 𝐾))
888, 86, 87rhmmul 20242 . . . . . . 7 ((𝑄 ∈ (𝑊 RingHom (𝑆s 𝐾)) ∧ ((algSc‘𝑊)‘(𝐴𝑘)) ∈ 𝐵 ∧ (𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)) ∈ 𝐵) → (𝑄‘(((algSc‘𝑊)‘(𝐴𝑘))(.r𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))) = ((𝑄‘((algSc‘𝑊)‘(𝐴𝑘)))(.r‘(𝑆s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))
8981, 85, 42, 88syl3anc 1372 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘(((algSc‘𝑊)‘(𝐴𝑘))(.r𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))) = ((𝑄‘((algSc‘𝑊)‘(𝐴𝑘)))(.r‘(𝑆s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))
902subrgcrng 20344 . . . . . . . . . . 11 ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing)
9120, 1, 90syl2anc 585 . . . . . . . . . 10 (𝜑𝑈 ∈ CRing)
926ply1assa 21692 . . . . . . . . . 10 (𝑈 ∈ CRing → 𝑊 ∈ AssAlg)
9391, 92syl 17 . . . . . . . . 9 (𝜑𝑊 ∈ AssAlg)
9493adantr 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝑊 ∈ AssAlg)
9582, 43, 44, 8, 86, 9asclmul1 21411 . . . . . . . 8 ((𝑊 ∈ AssAlg ∧ (𝐴𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)) ∈ 𝐵) → (((algSc‘𝑊)‘(𝐴𝑘))(.r𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))) = ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))))
9694, 31, 42, 95syl3anc 1372 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((algSc‘𝑊)‘(𝐴𝑘))(.r𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))) = ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))))
9796fveq2d 6885 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘(((algSc‘𝑊)‘(𝐴𝑘))(.r𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))) = (𝑄‘((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))
98 eqid 2733 . . . . . . . 8 (Base‘(𝑆s 𝐾)) = (Base‘(𝑆s 𝐾))
9920adantr 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝑆 ∈ CRing)
10017fvexi 6895 . . . . . . . . 9 𝐾 ∈ V
101100a1i 11 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝐾 ∈ V)
1028, 98rhmf 20241 . . . . . . . . . 10 (𝑄 ∈ (𝑊 RingHom (𝑆s 𝐾)) → 𝑄:𝐵⟶(Base‘(𝑆s 𝐾)))
10381, 102syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝑄:𝐵⟶(Base‘(𝑆s 𝐾)))
104103, 85ffvelcdmd 7075 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴𝑘))) ∈ (Base‘(𝑆s 𝐾)))
105103, 42ffvelcdmd 7075 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))) ∈ (Base‘(𝑆s 𝐾)))
106 evls1fpws.1 . . . . . . . 8 · = (.r𝑆)
10719, 98, 99, 101, 104, 105, 106, 87pwsmulrval 17424 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴𝑘)))(.r‘(𝑆s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))) = ((𝑄‘((algSc‘𝑊)‘(𝐴𝑘))) ∘f · (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))
10819, 17, 98, 99, 101, 104pwselbas 17422 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴𝑘))):𝐾𝐾)
109108ffnd 6708 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴𝑘))) Fn 𝐾)
11019, 17, 98, 99, 101, 105pwselbas 17422 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))):𝐾𝐾)
111110ffnd 6708 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))) Fn 𝐾)
112 inidm 4216 . . . . . . . 8 (𝐾𝐾) = 𝐾
11320ad2antrr 725 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → 𝑆 ∈ CRing)
1141ad2antrr 725 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → 𝑅 ∈ (SubRing‘𝑆))
11517subrgss 20341 . . . . . . . . . . . . . 14 (𝑅 ∈ (SubRing‘𝑆) → 𝑅𝐾)
1161, 115syl 17 . . . . . . . . . . . . 13 (𝜑𝑅𝐾)
1172, 17ressbas2 17169 . . . . . . . . . . . . 13 (𝑅𝐾𝑅 = (Base‘𝑈))
118116, 117syl 17 . . . . . . . . . . . 12 (𝜑𝑅 = (Base‘𝑈))
119118adantr 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 𝑅 = (Base‘𝑈))
12026, 119eleqtrrd 2837 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ 𝑅)
121120adantr 482 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → (𝐴𝑘) ∈ 𝑅)
122 simpr 486 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → 𝑥𝐾)
12316, 6, 2, 17, 82, 113, 114, 121, 122evls1scafv 32586 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → ((𝑄‘((algSc‘𝑊)‘(𝐴𝑘)))‘𝑥) = (𝐴𝑘))
124 evls1fpws.2 . . . . . . . . 9 = (.g‘(mulGrp‘𝑆))
125 simplr 768 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → 𝑘 ∈ ℕ0)
12616, 2, 6, 7, 17, 11, 124, 113, 114, 125, 122evls1varpwval 32588 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → ((𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))‘𝑥) = (𝑘 𝑥))
127109, 111, 101, 101, 112, 123, 126offval 7666 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴𝑘))) ∘f · (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))) = (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))))
128107, 127eqtrd 2773 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴𝑘)))(.r‘(𝑆s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))) = (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))))
12989, 97, 1283eqtr3d 2781 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑄‘((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))) = (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))))
130129mpteq2dva 5244 . . . 4 (𝜑 → (𝑘 ∈ ℕ0 ↦ (𝑄‘((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈))))) = (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))))
131130oveq2d 7412 . . 3 (𝜑 → ((𝑆s 𝐾) Σg (𝑘 ∈ ℕ0 ↦ (𝑄‘((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))) = ((𝑆s 𝐾) Σg (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))))))
132 eqid 2733 . . . 4 (0g‘(𝑆s 𝐾)) = (0g‘(𝑆s 𝐾))
133100a1i 11 . . . 4 (𝜑𝐾 ∈ V)
134 nn0ex 12465 . . . . 5 0 ∈ V
135134a1i 11 . . . 4 (𝜑 → ℕ0 ∈ V)
13620crngringd 20051 . . . . 5 (𝜑𝑆 ∈ Ring)
137136ringcmnd 20082 . . . 4 (𝜑𝑆 ∈ CMnd)
138136ad2antrr 725 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → 𝑆 ∈ Ring)
1391adantr 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 𝑅 ∈ (SubRing‘𝑆))
140139, 115syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → 𝑅𝐾)
141140, 120sseldd 3981 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ 𝐾)
142141adantr 482 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → (𝐴𝑘) ∈ 𝐾)
143 eqid 2733 . . . . . . . . . 10 (mulGrp‘𝑆) = (mulGrp‘𝑆)
144143, 17mgpbas 19976 . . . . . . . . 9 𝐾 = (Base‘(mulGrp‘𝑆))
145143ringmgp 20044 . . . . . . . . . . 11 (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
146136, 145syl 17 . . . . . . . . . 10 (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
147146ad2antrr 725 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → (mulGrp‘𝑆) ∈ Mnd)
148144, 124, 147, 125, 122mulgnn0cld 18960 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → (𝑘 𝑥) ∈ 𝐾)
14917, 106, 138, 142, 148ringcld 20061 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑥𝐾) → ((𝐴𝑘) · (𝑘 𝑥)) ∈ 𝐾)
1501493impa 1111 . . . . . 6 ((𝜑𝑘 ∈ ℕ0𝑥𝐾) → ((𝐴𝑘) · (𝑘 𝑥)) ∈ 𝐾)
1511503com23 1127 . . . . 5 ((𝜑𝑥𝐾𝑘 ∈ ℕ0) → ((𝐴𝑘) · (𝑘 𝑥)) ∈ 𝐾)
1521513expb 1121 . . . 4 ((𝜑 ∧ (𝑥𝐾𝑘 ∈ ℕ0)) → ((𝐴𝑘) · (𝑘 𝑥)) ∈ 𝐾)
153135mptexd 7213 . . . . 5 (𝜑 → (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))) ∈ V)
154 funmpt 6578 . . . . . 6 Fun (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))))
155154a1i 11 . . . . 5 (𝜑 → Fun (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))))
156 fvexd 6896 . . . . 5 (𝜑 → (0g‘(𝑆s 𝐾)) ∈ V)
15712, 8, 6, 52coe1sfi 21706 . . . . . . 7 (𝑀𝐵𝐴 finSupp (0g𝑈))
1585, 157syl 17 . . . . . 6 (𝜑𝐴 finSupp (0g𝑈))
159158fsuppimpd 9357 . . . . 5 (𝜑 → (𝐴 supp (0g𝑈)) ∈ Fin)
16012, 8, 6, 24coe1f 21704 . . . . . . . . . . . . . . . . 17 (𝑀𝐵𝐴:ℕ0⟶(Base‘𝑈))
1615, 160syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐴:ℕ0⟶(Base‘𝑈))
162161ffnd 6708 . . . . . . . . . . . . . . 15 (𝜑𝐴 Fn ℕ0)
163162adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → 𝐴 Fn ℕ0)
164134a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → ℕ0 ∈ V)
165 fvexd 6896 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → (0g𝑈) ∈ V)
166 simpr 486 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈))))
167163, 164, 165, 166fvdifsupp 31877 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → (𝐴𝑘) = (0g𝑈))
168 eqid 2733 . . . . . . . . . . . . . . . 16 (0g𝑆) = (0g𝑆)
1692, 168subrg0 20347 . . . . . . . . . . . . . . 15 (𝑅 ∈ (SubRing‘𝑆) → (0g𝑆) = (0g𝑈))
1701, 169syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0g𝑆) = (0g𝑈))
171170adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → (0g𝑆) = (0g𝑈))
172167, 171eqtr4d 2776 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → (𝐴𝑘) = (0g𝑆))
173172adantr 482 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → (𝐴𝑘) = (0g𝑆))
174173oveq1d 7411 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → ((𝐴𝑘) · (𝑘 𝑥)) = ((0g𝑆) · (𝑘 𝑥)))
175136ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → 𝑆 ∈ Ring)
176175, 145syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → (mulGrp‘𝑆) ∈ Mnd)
177 simplr 768 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈))))
178177eldifad 3958 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → 𝑘 ∈ ℕ0)
179 simpr 486 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → 𝑥𝐾)
180144, 124, 176, 178, 179mulgnn0cld 18960 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → (𝑘 𝑥) ∈ 𝐾)
18117, 106, 168ringlz 20088 . . . . . . . . . . 11 ((𝑆 ∈ Ring ∧ (𝑘 𝑥) ∈ 𝐾) → ((0g𝑆) · (𝑘 𝑥)) = (0g𝑆))
182175, 180, 181syl2anc 585 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → ((0g𝑆) · (𝑘 𝑥)) = (0g𝑆))
183174, 182eqtrd 2773 . . . . . . . . 9 (((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) ∧ 𝑥𝐾) → ((𝐴𝑘) · (𝑘 𝑥)) = (0g𝑆))
184183mpteq2dva 5244 . . . . . . . 8 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))) = (𝑥𝐾 ↦ (0g𝑆)))
185 fconstmpt 5733 . . . . . . . 8 (𝐾 × {(0g𝑆)}) = (𝑥𝐾 ↦ (0g𝑆))
186184, 185eqtr4di 2791 . . . . . . 7 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))) = (𝐾 × {(0g𝑆)}))
187137cmnmndd 19656 . . . . . . . . 9 (𝜑𝑆 ∈ Mnd)
18819, 168pws0g 18648 . . . . . . . . 9 ((𝑆 ∈ Mnd ∧ 𝐾 ∈ V) → (𝐾 × {(0g𝑆)}) = (0g‘(𝑆s 𝐾)))
189187, 133, 188syl2anc 585 . . . . . . . 8 (𝜑 → (𝐾 × {(0g𝑆)}) = (0g‘(𝑆s 𝐾)))
190189adantr 482 . . . . . . 7 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → (𝐾 × {(0g𝑆)}) = (0g‘(𝑆s 𝐾)))
191186, 190eqtrd 2773 . . . . . 6 ((𝜑𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g𝑈)))) → (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))) = (0g‘(𝑆s 𝐾)))
192191, 135suppss2 8172 . . . . 5 (𝜑 → ((𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))) supp (0g‘(𝑆s 𝐾))) ⊆ (𝐴 supp (0g𝑈)))
193 suppssfifsupp 9366 . . . . 5 ((((𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))) ∧ (0g‘(𝑆s 𝐾)) ∈ V) ∧ ((𝐴 supp (0g𝑈)) ∈ Fin ∧ ((𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))) supp (0g‘(𝑆s 𝐾))) ⊆ (𝐴 supp (0g𝑈)))) → (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))) finSupp (0g‘(𝑆s 𝐾)))
194153, 155, 156, 159, 192, 193syl32anc 1379 . . . 4 (𝜑 → (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥)))) finSupp (0g‘(𝑆s 𝐾)))
19519, 17, 132, 133, 135, 137, 152, 194pwsgsum 19833 . . 3 (𝜑 → ((𝑆s 𝐾) Σg (𝑘 ∈ ℕ0 ↦ (𝑥𝐾 ↦ ((𝐴𝑘) · (𝑘 𝑥))))) = (𝑥𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑘 𝑥))))))
19678, 131, 1953eqtrd 2777 . 2 (𝜑 → (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘)( ·𝑠𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1𝑈)))))) = (𝑥𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑘 𝑥))))))
19715, 196eqtrd 2773 1 (𝜑 → (𝑄𝑀) = (𝑥𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑘 𝑥))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wral 3062  wrex 3071  Vcvv 3475  cdif 3943  wss 3946  {csn 4624   class class class wbr 5144  cmpt 5227   × cxp 5670  Fun wfun 6529   Fn wfn 6530  wf 6531  cfv 6535  (class class class)co 7396  f cof 7655   supp csupp 8133  Fincfn 8927   finSupp cfsupp 9349   < clt 11235  0cn0 12459  Basecbs 17131  s cress 17160  .rcmulr 17185  Scalarcsca 17187   ·𝑠 cvsca 17188  0gc0g 17372   Σg cgsu 17373  s cpws 17379  Mndcmnd 18612  .gcmg 18935  mulGrpcmgp 19970  Ringcrg 20038  CRingccrg 20039   RingHom crh 20226  SubRingcsubrg 20336  LModclmod 20448  AssAlgcasa 21378  algSccascl 21380  var1cv1 21669  Poly1cpl1 21670  coe1cco1 21671   evalSub1 ces1 21801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712  ax-cnex 11153  ax-resscn 11154  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-mulcom 11161  ax-addass 11162  ax-mulass 11163  ax-distr 11164  ax-i2m1 11165  ax-1ne0 11166  ax-1rid 11167  ax-rnegex 11168  ax-rrecex 11169  ax-cnre 11170  ax-pre-lttri 11171  ax-pre-lttrn 11172  ax-pre-ltadd 11173  ax-pre-mulgt0 11174
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4905  df-int 4947  df-iun 4995  df-iin 4996  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7657  df-ofr 7658  df-om 7843  df-1st 7962  df-2nd 7963  df-supp 8134  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-1o 8453  df-er 8691  df-map 8810  df-pm 8811  df-ixp 8880  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fsupp 9350  df-sup 9424  df-oi 9492  df-card 9921  df-pnf 11237  df-mnf 11238  df-xr 11239  df-ltxr 11240  df-le 11241  df-sub 11433  df-neg 11434  df-nn 12200  df-2 12262  df-3 12263  df-4 12264  df-5 12265  df-6 12266  df-7 12267  df-8 12268  df-9 12269  df-n0 12460  df-z 12546  df-dec 12665  df-uz 12810  df-fz 13472  df-fzo 13615  df-seq 13954  df-hash 14278  df-struct 17067  df-sets 17084  df-slot 17102  df-ndx 17114  df-base 17132  df-ress 17161  df-plusg 17197  df-mulr 17198  df-sca 17200  df-vsca 17201  df-ip 17202  df-tset 17203  df-ple 17204  df-ds 17206  df-hom 17208  df-cco 17209  df-0g 17374  df-gsum 17375  df-prds 17380  df-pws 17382  df-mre 17517  df-mrc 17518  df-acs 17520  df-mgm 18548  df-sgrp 18597  df-mnd 18613  df-mhm 18658  df-submnd 18659  df-grp 18809  df-minusg 18810  df-sbg 18811  df-mulg 18936  df-subg 18988  df-ghm 19075  df-cntz 19166  df-cmn 19634  df-abl 19635  df-mgp 19971  df-ur 19988  df-srg 19992  df-ring 20040  df-cring 20041  df-rnghom 20229  df-subrg 20338  df-lmod 20450  df-lss 20520  df-lsp 20560  df-assa 21381  df-asp 21382  df-ascl 21383  df-psr 21433  df-mvr 21434  df-mpl 21435  df-opsr 21437  df-evls 21604  df-evl 21605  df-psr1 21673  df-vr1 21674  df-ply1 21675  df-coe1 21676  df-evls1 21803  df-evl1 21804
This theorem is referenced by:  ressply1evl  32590
  Copyright terms: Public domain W3C validator