MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lply1binomsc Structured version   Visualization version   GIF version

Theorem lply1binomsc 21588
Description: The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings, expressed by an element of this ring: (𝑋 + 𝐴)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝑋𝑘)). (Contributed by AV, 25-Aug-2019.)
Hypotheses
Ref Expression
cply1binom.p 𝑃 = (Poly1𝑅)
cply1binom.x 𝑋 = (var1𝑅)
cply1binom.a + = (+g𝑃)
cply1binom.m × = (.r𝑃)
cply1binom.t · = (.g𝑃)
cply1binom.g 𝐺 = (mulGrp‘𝑃)
cply1binom.e = (.g𝐺)
lply1binomsc.k 𝐾 = (Base‘𝑅)
lply1binomsc.s 𝑆 = (algSc‘𝑃)
lply1binomsc.h 𝐻 = (mulGrp‘𝑅)
lply1binomsc.e 𝐸 = (.g𝐻)
Assertion
Ref Expression
lply1binomsc ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (𝑁 (𝑋 + (𝑆𝐴))) = (𝑃 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((𝑆‘((𝑁𝑘)𝐸𝐴)) × (𝑘 𝑋))))))
Distinct variable groups:   𝐴,𝑘   𝑘,𝐾   𝑘,𝑁   𝑃,𝑘   𝑅,𝑘   𝑘,𝑋   × ,𝑘   · ,𝑘   ,𝑘   + ,𝑘   𝑆,𝑘
Allowed substitution hints:   𝐸(𝑘)   𝐺(𝑘)   𝐻(𝑘)

Proof of Theorem lply1binomsc
StepHypRef Expression
1 lply1binomsc.s . . . . . 6 𝑆 = (algSc‘𝑃)
2 eqid 2737 . . . . . 6 (Scalar‘𝑃) = (Scalar‘𝑃)
3 crngring 19894 . . . . . . . 8 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
4 cply1binom.p . . . . . . . . 9 𝑃 = (Poly1𝑅)
54ply1ring 21529 . . . . . . . 8 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
63, 5syl 17 . . . . . . 7 (𝑅 ∈ CRing → 𝑃 ∈ Ring)
763ad2ant1 1133 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝑃 ∈ Ring)
84ply1lmod 21533 . . . . . . . 8 (𝑅 ∈ Ring → 𝑃 ∈ LMod)
93, 8syl 17 . . . . . . 7 (𝑅 ∈ CRing → 𝑃 ∈ LMod)
1093ad2ant1 1133 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝑃 ∈ LMod)
11 eqid 2737 . . . . . 6 (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
12 eqid 2737 . . . . . 6 (Base‘𝑃) = (Base‘𝑃)
131, 2, 7, 10, 11, 12asclf 21196 . . . . 5 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝑆:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃))
14 lply1binomsc.k . . . . . . 7 𝐾 = (Base‘𝑅)
154ply1sca 21534 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃))
16153ad2ant1 1133 . . . . . . . 8 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝑅 = (Scalar‘𝑃))
1716fveq2d 6838 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
1814, 17eqtrid 2789 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝐾 = (Base‘(Scalar‘𝑃)))
1918feq2d 6646 . . . . 5 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (𝑆:𝐾⟶(Base‘𝑃) ↔ 𝑆:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃)))
2013, 19mpbird 257 . . . 4 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝑆:𝐾⟶(Base‘𝑃))
21 simp3 1138 . . . 4 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝐴𝐾)
2220, 21ffvelcdmd 7027 . . 3 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (𝑆𝐴) ∈ (Base‘𝑃))
23 cply1binom.x . . . 4 𝑋 = (var1𝑅)
24 cply1binom.a . . . 4 + = (+g𝑃)
25 cply1binom.m . . . 4 × = (.r𝑃)
26 cply1binom.t . . . 4 · = (.g𝑃)
27 cply1binom.g . . . 4 𝐺 = (mulGrp‘𝑃)
28 cply1binom.e . . . 4 = (.g𝐺)
294, 23, 24, 25, 26, 27, 28, 12lply1binom 21587 . . 3 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ (𝑆𝐴) ∈ (Base‘𝑃)) → (𝑁 (𝑋 + (𝑆𝐴))) = (𝑃 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) (𝑆𝐴)) × (𝑘 𝑋))))))
3022, 29syld3an3 1409 . 2 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (𝑁 (𝑋 + (𝑆𝐴))) = (𝑃 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) (𝑆𝐴)) × (𝑘 𝑋))))))
314ply1assa 21480 . . . . . . . . . . 11 (𝑅 ∈ CRing → 𝑃 ∈ AssAlg)
32313ad2ant1 1133 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝑃 ∈ AssAlg)
3332adantr 482 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → 𝑃 ∈ AssAlg)
34 fznn0sub 13398 . . . . . . . . . 10 (𝑘 ∈ (0...𝑁) → (𝑁𝑘) ∈ ℕ0)
3534adantl 483 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (𝑁𝑘) ∈ ℕ0)
3615fveq2d 6838 . . . . . . . . . . . . . 14 (𝑅 ∈ CRing → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
3714, 36eqtrid 2789 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → 𝐾 = (Base‘(Scalar‘𝑃)))
3837eleq2d 2823 . . . . . . . . . . . 12 (𝑅 ∈ CRing → (𝐴𝐾𝐴 ∈ (Base‘(Scalar‘𝑃))))
3938biimpa 478 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ 𝐴𝐾) → 𝐴 ∈ (Base‘(Scalar‘𝑃)))
40393adant2 1131 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝐴 ∈ (Base‘(Scalar‘𝑃)))
4140adantr 482 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ (Base‘(Scalar‘𝑃)))
42 eqid 2737 . . . . . . . . . . . . 13 (1r𝑃) = (1r𝑃)
4312, 42ringidcl 19906 . . . . . . . . . . . 12 (𝑃 ∈ Ring → (1r𝑃) ∈ (Base‘𝑃))
446, 43syl 17 . . . . . . . . . . 11 (𝑅 ∈ CRing → (1r𝑃) ∈ (Base‘𝑃))
45443ad2ant1 1133 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (1r𝑃) ∈ (Base‘𝑃))
4645adantr 482 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (1r𝑃) ∈ (Base‘𝑃))
47 eqid 2737 . . . . . . . . . 10 ( ·𝑠𝑃) = ( ·𝑠𝑃)
48 eqid 2737 . . . . . . . . . 10 (mulGrp‘(Scalar‘𝑃)) = (mulGrp‘(Scalar‘𝑃))
49 eqid 2737 . . . . . . . . . 10 (.g‘(mulGrp‘(Scalar‘𝑃))) = (.g‘(mulGrp‘(Scalar‘𝑃)))
5012, 2, 11, 47, 48, 49, 27, 28assamulgscm 21215 . . . . . . . . 9 ((𝑃 ∈ AssAlg ∧ ((𝑁𝑘) ∈ ℕ0𝐴 ∈ (Base‘(Scalar‘𝑃)) ∧ (1r𝑃) ∈ (Base‘𝑃))) → ((𝑁𝑘) (𝐴( ·𝑠𝑃)(1r𝑃))) = (((𝑁𝑘)(.g‘(mulGrp‘(Scalar‘𝑃)))𝐴)( ·𝑠𝑃)((𝑁𝑘) (1r𝑃))))
5133, 35, 41, 46, 50syl13anc 1372 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁𝑘) (𝐴( ·𝑠𝑃)(1r𝑃))) = (((𝑁𝑘)(.g‘(mulGrp‘(Scalar‘𝑃)))𝐴)( ·𝑠𝑃)((𝑁𝑘) (1r𝑃))))
52 lply1binomsc.e . . . . . . . . . . . . . 14 𝐸 = (.g𝐻)
53 lply1binomsc.h . . . . . . . . . . . . . . . 16 𝐻 = (mulGrp‘𝑅)
5415fveq2d 6838 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → (mulGrp‘𝑅) = (mulGrp‘(Scalar‘𝑃)))
5553, 54eqtrid 2789 . . . . . . . . . . . . . . 15 (𝑅 ∈ CRing → 𝐻 = (mulGrp‘(Scalar‘𝑃)))
5655fveq2d 6838 . . . . . . . . . . . . . 14 (𝑅 ∈ CRing → (.g𝐻) = (.g‘(mulGrp‘(Scalar‘𝑃))))
5752, 56eqtrid 2789 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → 𝐸 = (.g‘(mulGrp‘(Scalar‘𝑃))))
58573ad2ant1 1133 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝐸 = (.g‘(mulGrp‘(Scalar‘𝑃))))
5958adantr 482 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → 𝐸 = (.g‘(mulGrp‘(Scalar‘𝑃))))
6059eqcomd 2743 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (.g‘(mulGrp‘(Scalar‘𝑃))) = 𝐸)
6160oveqd 7363 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁𝑘)(.g‘(mulGrp‘(Scalar‘𝑃)))𝐴) = ((𝑁𝑘)𝐸𝐴))
6227ringmgp 19888 . . . . . . . . . . . 12 (𝑃 ∈ Ring → 𝐺 ∈ Mnd)
636, 62syl 17 . . . . . . . . . . 11 (𝑅 ∈ CRing → 𝐺 ∈ Mnd)
64633ad2ant1 1133 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝐺 ∈ Mnd)
6527, 12mgpbas 19825 . . . . . . . . . . 11 (Base‘𝑃) = (Base‘𝐺)
6627, 42ringidval 19838 . . . . . . . . . . 11 (1r𝑃) = (0g𝐺)
6765, 28, 66mulgnn0z 18831 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑁𝑘) ∈ ℕ0) → ((𝑁𝑘) (1r𝑃)) = (1r𝑃))
6864, 34, 67syl2an 597 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁𝑘) (1r𝑃)) = (1r𝑃))
6961, 68oveq12d 7364 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁𝑘)(.g‘(mulGrp‘(Scalar‘𝑃)))𝐴)( ·𝑠𝑃)((𝑁𝑘) (1r𝑃))) = (((𝑁𝑘)𝐸𝐴)( ·𝑠𝑃)(1r𝑃)))
7051, 69eqtrd 2777 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁𝑘) (𝐴( ·𝑠𝑃)(1r𝑃))) = (((𝑁𝑘)𝐸𝐴)( ·𝑠𝑃)(1r𝑃)))
711, 2, 11, 47, 42asclval 21194 . . . . . . . . 9 (𝐴 ∈ (Base‘(Scalar‘𝑃)) → (𝑆𝐴) = (𝐴( ·𝑠𝑃)(1r𝑃)))
7241, 71syl 17 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (𝑆𝐴) = (𝐴( ·𝑠𝑃)(1r𝑃)))
7372oveq2d 7362 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁𝑘) (𝑆𝐴)) = ((𝑁𝑘) (𝐴( ·𝑠𝑃)(1r𝑃))))
7453ringmgp 19888 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → 𝐻 ∈ Mnd)
753, 74syl 17 . . . . . . . . . . . 12 (𝑅 ∈ CRing → 𝐻 ∈ Mnd)
76753ad2ant1 1133 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝐻 ∈ Mnd)
7776adantr 482 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → 𝐻 ∈ Mnd)
78 simpr 486 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ 𝐴𝐾) → 𝐴𝐾)
7953, 14mgpbas 19825 . . . . . . . . . . . . 13 𝐾 = (Base‘𝐻)
8078, 79eleqtrdi 2848 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝐴𝐾) → 𝐴 ∈ (Base‘𝐻))
81803adant2 1131 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → 𝐴 ∈ (Base‘𝐻))
8281adantr 482 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ (Base‘𝐻))
83 eqid 2737 . . . . . . . . . . 11 (Base‘𝐻) = (Base‘𝐻)
8483, 52mulgnn0cl 18821 . . . . . . . . . 10 ((𝐻 ∈ Mnd ∧ (𝑁𝑘) ∈ ℕ0𝐴 ∈ (Base‘𝐻)) → ((𝑁𝑘)𝐸𝐴) ∈ (Base‘𝐻))
8577, 35, 82, 84syl3anc 1371 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁𝑘)𝐸𝐴) ∈ (Base‘𝐻))
8616adantr 482 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → 𝑅 = (Scalar‘𝑃))
8786eqcomd 2743 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (Scalar‘𝑃) = 𝑅)
8887fveq2d 6838 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
89 eqid 2737 . . . . . . . . . . 11 (Base‘𝑅) = (Base‘𝑅)
9053, 89mgpbas 19825 . . . . . . . . . 10 (Base‘𝑅) = (Base‘𝐻)
9188, 90eqtrdi 2793 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (Base‘(Scalar‘𝑃)) = (Base‘𝐻))
9285, 91eleqtrrd 2841 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁𝑘)𝐸𝐴) ∈ (Base‘(Scalar‘𝑃)))
931, 2, 11, 47, 42asclval 21194 . . . . . . . 8 (((𝑁𝑘)𝐸𝐴) ∈ (Base‘(Scalar‘𝑃)) → (𝑆‘((𝑁𝑘)𝐸𝐴)) = (((𝑁𝑘)𝐸𝐴)( ·𝑠𝑃)(1r𝑃)))
9492, 93syl 17 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (𝑆‘((𝑁𝑘)𝐸𝐴)) = (((𝑁𝑘)𝐸𝐴)( ·𝑠𝑃)(1r𝑃)))
9570, 73, 943eqtr4d 2787 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁𝑘) (𝑆𝐴)) = (𝑆‘((𝑁𝑘)𝐸𝐴)))
9695oveq1d 7361 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁𝑘) (𝑆𝐴)) × (𝑘 𝑋)) = ((𝑆‘((𝑁𝑘)𝐸𝐴)) × (𝑘 𝑋)))
9796oveq2d 7362 . . . 4 (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁𝑘) (𝑆𝐴)) × (𝑘 𝑋))) = ((𝑁C𝑘) · ((𝑆‘((𝑁𝑘)𝐸𝐴)) × (𝑘 𝑋))))
9897mpteq2dva 5200 . . 3 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) (𝑆𝐴)) × (𝑘 𝑋)))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((𝑆‘((𝑁𝑘)𝐸𝐴)) × (𝑘 𝑋)))))
9998oveq2d 7362 . 2 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (𝑃 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) (𝑆𝐴)) × (𝑘 𝑋))))) = (𝑃 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((𝑆‘((𝑁𝑘)𝐸𝐴)) × (𝑘 𝑋))))))
10030, 99eqtrd 2777 1 ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0𝐴𝐾) → (𝑁 (𝑋 + (𝑆𝐴))) = (𝑃 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((𝑆‘((𝑁𝑘)𝐸𝐴)) × (𝑘 𝑋))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1087   = wceq 1541  wcel 2106  cmpt 5183  wf 6484  cfv 6488  (class class class)co 7346  0cc0 10981  cmin 11315  0cn0 12343  ...cfz 13349  Ccbc 14126  Basecbs 17014  +gcplusg 17064  .rcmulr 17065  Scalarcsca 17067   ·𝑠 cvsca 17068   Σg cgsu 17253  Mndcmnd 18487  .gcmg 18801  mulGrpcmgp 19819  1rcur 19836  Ringcrg 19882  CRingccrg 19883  LModclmod 20233  AssAlgcasa 21167  algSccascl 21169  var1cv1 21457  Poly1cpl1 21458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5237  ax-sep 5251  ax-nul 5258  ax-pow 5315  ax-pr 5379  ax-un 7659  ax-cnex 11037  ax-resscn 11038  ax-1cn 11039  ax-icn 11040  ax-addcl 11041  ax-addrcl 11042  ax-mulcl 11043  ax-mulrcl 11044  ax-mulcom 11045  ax-addass 11046  ax-mulass 11047  ax-distr 11048  ax-i2m1 11049  ax-1ne0 11050  ax-1rid 11051  ax-rnegex 11052  ax-rrecex 11053  ax-cnre 11054  ax-pre-lttri 11055  ax-pre-lttrn 11056  ax-pre-ltadd 11057  ax-pre-mulgt0 11058
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3924  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4861  df-int 4903  df-iun 4951  df-iin 4952  df-br 5101  df-opab 5163  df-mpt 5184  df-tr 5218  df-id 5525  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5582  df-se 5583  df-we 5584  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-pred 6246  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-isom 6497  df-riota 7302  df-ov 7349  df-oprab 7350  df-mpo 7351  df-of 7604  df-ofr 7605  df-om 7790  df-1st 7908  df-2nd 7909  df-supp 8057  df-frecs 8176  df-wrecs 8207  df-recs 8281  df-rdg 8320  df-1o 8376  df-er 8578  df-map 8697  df-pm 8698  df-ixp 8766  df-en 8814  df-dom 8815  df-sdom 8816  df-fin 8817  df-fsupp 9236  df-oi 9376  df-card 9805  df-pnf 11121  df-mnf 11122  df-xr 11123  df-ltxr 11124  df-le 11125  df-sub 11317  df-neg 11318  df-div 11743  df-nn 12084  df-2 12146  df-3 12147  df-4 12148  df-5 12149  df-6 12150  df-7 12151  df-8 12152  df-9 12153  df-n0 12344  df-z 12430  df-dec 12548  df-uz 12693  df-rp 12841  df-fz 13350  df-fzo 13493  df-seq 13832  df-fac 14098  df-bc 14127  df-hash 14155  df-struct 16950  df-sets 16967  df-slot 16985  df-ndx 16997  df-base 17015  df-ress 17044  df-plusg 17077  df-mulr 17078  df-sca 17080  df-vsca 17081  df-tset 17083  df-ple 17084  df-0g 17254  df-gsum 17255  df-mre 17397  df-mrc 17398  df-acs 17400  df-mgm 18428  df-sgrp 18477  df-mnd 18488  df-mhm 18532  df-submnd 18533  df-grp 18681  df-minusg 18682  df-sbg 18683  df-mulg 18802  df-subg 18853  df-ghm 18933  df-cntz 19024  df-cmn 19488  df-abl 19489  df-mgp 19820  df-ur 19837  df-srg 19841  df-ring 19884  df-cring 19885  df-subrg 20131  df-lmod 20235  df-lss 20304  df-assa 21170  df-ascl 21172  df-psr 21222  df-mvr 21223  df-mpl 21224  df-opsr 21226  df-psr1 21461  df-vr1 21462  df-ply1 21463
This theorem is referenced by:  chpscmatgsumbin  22103
  Copyright terms: Public domain W3C validator