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

Theorem chfacfisf 20640
 Description: The "characteristic factor function" is a function from the nonnegative integers to polynomial matrices. (Contributed by AV, 8-Nov-2019.)
Hypotheses
Ref Expression
chfacfisf.a 𝐴 = (𝑁 Mat 𝑅)
chfacfisf.b 𝐵 = (Base‘𝐴)
chfacfisf.p 𝑃 = (Poly1𝑅)
chfacfisf.y 𝑌 = (𝑁 Mat 𝑃)
chfacfisf.r × = (.r𝑌)
chfacfisf.s = (-g𝑌)
chfacfisf.0 0 = (0g𝑌)
chfacfisf.t 𝑇 = (𝑁 matToPolyMat 𝑅)
chfacfisf.g 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
Assertion
Ref Expression
chfacfisf (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))
Distinct variable groups:   𝐵,𝑛   𝑛,𝑀   𝑛,𝑁   𝑅,𝑛   𝑛,𝑌   𝑛,𝑏   𝑛,𝑠
Allowed substitution hints:   𝐴(𝑛,𝑠,𝑏)   𝐵(𝑠,𝑏)   𝑃(𝑛,𝑠,𝑏)   𝑅(𝑠,𝑏)   𝑇(𝑛,𝑠,𝑏)   × (𝑛,𝑠,𝑏)   𝐺(𝑛,𝑠,𝑏)   𝑀(𝑠,𝑏)   (𝑛,𝑠,𝑏)   𝑁(𝑠,𝑏)   𝑌(𝑠,𝑏)   0 (𝑛,𝑠,𝑏)

Proof of Theorem chfacfisf
StepHypRef Expression
1 chfacfisf.p . . . . . . . . 9 𝑃 = (Poly1𝑅)
2 chfacfisf.y . . . . . . . . 9 𝑌 = (𝑁 Mat 𝑃)
31, 2pmatring 20479 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
433adant3 1079 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
5 ringgrp 18533 . . . . . . 7 (𝑌 ∈ Ring → 𝑌 ∈ Grp)
64, 5syl 17 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → 𝑌 ∈ Grp)
76adantr 481 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑌 ∈ Grp)
8 eqid 2620 . . . . . . . 8 (Base‘𝑌) = (Base‘𝑌)
9 chfacfisf.0 . . . . . . . 8 0 = (0g𝑌)
108, 9ring0cl 18550 . . . . . . 7 (𝑌 ∈ Ring → 0 ∈ (Base‘𝑌))
114, 10syl 17 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → 0 ∈ (Base‘𝑌))
1211adantr 481 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 0 ∈ (Base‘𝑌))
134adantr 481 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑌 ∈ Ring)
14 chfacfisf.t . . . . . . . 8 𝑇 = (𝑁 matToPolyMat 𝑅)
15 chfacfisf.a . . . . . . . 8 𝐴 = (𝑁 Mat 𝑅)
16 chfacfisf.b . . . . . . . 8 𝐵 = (Base‘𝐴)
1714, 15, 16, 1, 2mat2pmatbas 20512 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
1817adantr 481 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑇𝑀) ∈ (Base‘𝑌))
19 3simpa 1056 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
20 elmapi 7864 . . . . . . . . . . 11 (𝑏 ∈ (𝐵𝑚 (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
2120adantl 482 . . . . . . . . . 10 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵)
22 nnnn0 11284 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → 𝑠 ∈ ℕ0)
23 nn0uz 11707 . . . . . . . . . . . . 13 0 = (ℤ‘0)
2422, 23syl6eleq 2709 . . . . . . . . . . . 12 (𝑠 ∈ ℕ → 𝑠 ∈ (ℤ‘0))
25 eluzfz1 12333 . . . . . . . . . . . 12 (𝑠 ∈ (ℤ‘0) → 0 ∈ (0...𝑠))
2624, 25syl 17 . . . . . . . . . . 11 (𝑠 ∈ ℕ → 0 ∈ (0...𝑠))
2726adantr 481 . . . . . . . . . 10 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 0 ∈ (0...𝑠))
2821, 27ffvelrnd 6346 . . . . . . . . 9 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑏‘0) ∈ 𝐵)
2919, 28anim12i 589 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘0) ∈ 𝐵))
30 df-3an 1038 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘0) ∈ 𝐵))
3129, 30sylibr 224 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵))
3214, 15, 16, 1, 2mat2pmatbas 20512 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
3331, 32syl 17 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
34 chfacfisf.r . . . . . . 7 × = (.r𝑌)
358, 34ringcl 18542 . . . . . 6 ((𝑌 ∈ Ring ∧ (𝑇𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
3613, 18, 33, 35syl3anc 1324 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
37 chfacfisf.s . . . . . 6 = (-g𝑌)
388, 37grpsubcl 17476 . . . . 5 ((𝑌 ∈ Grp ∧ 0 ∈ (Base‘𝑌) ∧ ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌))
397, 12, 36, 38syl3anc 1324 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌))
4039ad2antrr 761 . . 3 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌))
4122adantr 481 . . . . . . . . 9 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑠 ∈ ℕ0)
4219, 41anim12i 589 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑠 ∈ ℕ0))
43 df-3an 1038 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑠 ∈ ℕ0))
4442, 43sylibr 224 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0))
45 eluzfz2 12334 . . . . . . . . . . 11 (𝑠 ∈ (ℤ‘0) → 𝑠 ∈ (0...𝑠))
4624, 45syl 17 . . . . . . . . . 10 (𝑠 ∈ ℕ → 𝑠 ∈ (0...𝑠))
4746anim1i 591 . . . . . . . . 9 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑠 ∈ (0...𝑠) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))))
4847ancomd 467 . . . . . . . 8 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑏 ∈ (𝐵𝑚 (0...𝑠)) ∧ 𝑠 ∈ (0...𝑠)))
4948adantl 482 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑏 ∈ (𝐵𝑚 (0...𝑠)) ∧ 𝑠 ∈ (0...𝑠)))
5015, 16, 1, 2, 14m2pmfzmap 20533 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0) ∧ (𝑏 ∈ (𝐵𝑚 (0...𝑠)) ∧ 𝑠 ∈ (0...𝑠))) → (𝑇‘(𝑏𝑠)) ∈ (Base‘𝑌))
5144, 49, 50syl2anc 692 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑇‘(𝑏𝑠)) ∈ (Base‘𝑌))
5251adantr 481 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑏𝑠)) ∈ (Base‘𝑌))
5352ad2antrr 761 . . . 4 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 = (𝑠 + 1)) → (𝑇‘(𝑏𝑠)) ∈ (Base‘𝑌))
5412ad4antr 767 . . . . 5 (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ (𝑠 + 1) < 𝑛) → 0 ∈ (Base‘𝑌))
55 nn0re 11286 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
5655adantl 482 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℝ)
57 peano2nn 11017 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ℕ → (𝑠 + 1) ∈ ℕ)
5857nnred 11020 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℕ → (𝑠 + 1) ∈ ℝ)
5958adantr 481 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑠 + 1) ∈ ℝ)
6056, 59lenltd 10168 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑛 ≤ (𝑠 + 1) ↔ ¬ (𝑠 + 1) < 𝑛))
61 nesym 2847 . . . . . . . . . . . . . . . 16 ((𝑠 + 1) ≠ 𝑛 ↔ ¬ 𝑛 = (𝑠 + 1))
62 ltlen 10123 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ) → (𝑛 < (𝑠 + 1) ↔ (𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛)))
6355, 58, 62syl2anr 495 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑛 < (𝑠 + 1) ↔ (𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛)))
6463biimprd 238 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → ((𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛) → 𝑛 < (𝑠 + 1)))
6564expcomd 454 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → ((𝑠 + 1) ≠ 𝑛 → (𝑛 ≤ (𝑠 + 1) → 𝑛 < (𝑠 + 1))))
6661, 65syl5bir 233 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = (𝑠 + 1) → (𝑛 ≤ (𝑠 + 1) → 𝑛 < (𝑠 + 1))))
6766com23 86 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑛 ≤ (𝑠 + 1) → (¬ 𝑛 = (𝑠 + 1) → 𝑛 < (𝑠 + 1))))
6860, 67sylbird 250 . . . . . . . . . . . . 13 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (¬ (𝑠 + 1) < 𝑛 → (¬ 𝑛 = (𝑠 + 1) → 𝑛 < (𝑠 + 1))))
6968com23 86 . . . . . . . . . . . 12 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = (𝑠 + 1) → (¬ (𝑠 + 1) < 𝑛𝑛 < (𝑠 + 1))))
7069impd 447 . . . . . . . . . . 11 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1)))
7170ex 450 . . . . . . . . . 10 (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0 → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1))))
7271ad2antrl 763 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑛 ∈ ℕ0 → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1))))
7372imp 445 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1)))
7473adantr 481 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1)))
753, 5syl 17 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Grp)
76753adant3 1079 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → 𝑌 ∈ Grp)
7776ad4antr 767 . . . . . . . . 9 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑌 ∈ Grp)
7819ad4antr 767 . . . . . . . . . . 11 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
7921ad4antlr 768 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑏:(0...𝑠)⟶𝐵)
80 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 0 → 𝑛 = 0)
8180necon3bi 2817 . . . . . . . . . . . . . . . . . 18 𝑛 = 0 → 𝑛 ≠ 0)
8281anim2i 592 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0) → (𝑛 ∈ ℕ0𝑛 ≠ 0))
83 elnnne0 11291 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ0𝑛 ≠ 0))
8482, 83sylibr 224 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
85 nnm1nn0 11319 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
8684, 85syl 17 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0) → (𝑛 − 1) ∈ ℕ0)
8786adantll 749 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑛 − 1) ∈ ℕ0)
8887adantr 481 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ∈ ℕ0)
8941ad4antlr 768 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℕ0)
9063simprbda 652 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ≤ (𝑠 + 1))
9156adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ ℝ)
92 1red 10040 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 1 ∈ ℝ)
93 nnre 11012 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℕ → 𝑠 ∈ ℝ)
9493ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℝ)
9591, 92, 94lesubaddd 10609 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑛 − 1) ≤ 𝑠𝑛 ≤ (𝑠 + 1)))
9690, 95mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ≤ 𝑠)
9796exp31 629 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠)))
9897ad2antrl 763 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠)))
9998imp 445 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠))
10099adantr 481 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠))
101100imp 445 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ≤ 𝑠)
102 elfz2nn0 12415 . . . . . . . . . . . . 13 ((𝑛 − 1) ∈ (0...𝑠) ↔ ((𝑛 − 1) ∈ ℕ0𝑠 ∈ ℕ0 ∧ (𝑛 − 1) ≤ 𝑠))
10388, 89, 101, 102syl3anbrc 1244 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ∈ (0...𝑠))
10479, 103ffvelrnd 6346 . . . . . . . . . . 11 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑏‘(𝑛 − 1)) ∈ 𝐵)
105 df-3an 1038 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵))
10678, 104, 105sylanbrc 697 . . . . . . . . . 10 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵))
10714, 15, 16, 1, 2mat2pmatbas 20512 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵) → (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌))
108106, 107syl 17 . . . . . . . . 9 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌))
10913ad2antrr 761 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑌 ∈ Ring)
11018ad2antrr 761 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇𝑀) ∈ (Base‘𝑌))
11144ad2antrr 761 . . . . . . . . . . . 12 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0))
112 simprr 795 . . . . . . . . . . . . 13 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑏 ∈ (𝐵𝑚 (0...𝑠)))
113112ad2antrr 761 . . . . . . . . . . . 12 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑏 ∈ (𝐵𝑚 (0...𝑠)))
114 simplr 791 . . . . . . . . . . . . . . . 16 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ ℕ0)
11522ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℕ0)
116 nn0z 11385 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
117 nnz 11384 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ℕ → 𝑠 ∈ ℤ)
118 zleltp1 11413 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑛𝑠𝑛 < (𝑠 + 1)))
119116, 117, 118syl2anr 495 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑛𝑠𝑛 < (𝑠 + 1)))
120119biimpar 502 . . . . . . . . . . . . . . . 16 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛𝑠)
121 elfz2nn0 12415 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (0...𝑠) ↔ (𝑛 ∈ ℕ0𝑠 ∈ ℕ0𝑛𝑠))
122114, 115, 120, 121syl3anbrc 1244 . . . . . . . . . . . . . . 15 (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ (0...𝑠))
123122exp31 629 . . . . . . . . . . . . . 14 (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → 𝑛 ∈ (0...𝑠))))
124123ad2antrl 763 . . . . . . . . . . . . 13 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → 𝑛 ∈ (0...𝑠))))
125124imp31 448 . . . . . . . . . . . 12 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ (0...𝑠))
12615, 16, 1, 2, 14m2pmfzmap 20533 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0) ∧ (𝑏 ∈ (𝐵𝑚 (0...𝑠)) ∧ 𝑛 ∈ (0...𝑠))) → (𝑇‘(𝑏𝑛)) ∈ (Base‘𝑌))
127111, 113, 125, 126syl12anc 1322 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇‘(𝑏𝑛)) ∈ (Base‘𝑌))
1288, 34ringcl 18542 . . . . . . . . . . 11 ((𝑌 ∈ Ring ∧ (𝑇𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏𝑛)) ∈ (Base‘𝑌)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑛))) ∈ (Base‘𝑌))
129109, 110, 127, 128syl3anc 1324 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑛))) ∈ (Base‘𝑌))
130129adantlr 750 . . . . . . . . 9 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑛))) ∈ (Base‘𝑌))
1318, 37grpsubcl 17476 . . . . . . . . 9 ((𝑌 ∈ Grp ∧ (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌) ∧ ((𝑇𝑀) × (𝑇‘(𝑏𝑛))) ∈ (Base‘𝑌)) → ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))) ∈ (Base‘𝑌))
13277, 108, 130, 131syl3anc 1324 . . . . . . . 8 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))) ∈ (Base‘𝑌))
133132ex 450 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑛 < (𝑠 + 1) → ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))) ∈ (Base‘𝑌)))
13474, 133syld 47 . . . . . 6 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))) ∈ (Base‘𝑌)))
135134impl 649 . . . . 5 (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))) ∈ (Base‘𝑌))
13654, 135ifclda 4111 . . . 4 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))) ∈ (Base‘𝑌))
13753, 136ifclda 4111 . . 3 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))))) ∈ (Base‘𝑌))
13840, 137ifclda 4111 . 2 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))) ∈ (Base‘𝑌))
139 chfacfisf.g . 2 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
140138, 139fmptd 6371 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1481   ∈ wcel 1988   ≠ wne 2791  ifcif 4077   class class class wbr 4644   ↦ cmpt 4720  ⟶wf 5872  ‘cfv 5876  (class class class)co 6635   ↑𝑚 cmap 7842  Fincfn 7940  ℝcr 9920  0cc0 9921  1c1 9922   + caddc 9924   < clt 10059   ≤ cle 10060   − cmin 10251  ℕcn 11005  ℕ0cn0 11277  ℤcz 11362  ℤ≥cuz 11672  ...cfz 12311  Basecbs 15838  .rcmulr 15923  0gc0g 16081  Grpcgrp 17403  -gcsg 17405  Ringcrg 18528  Poly1cpl1 19528   Mat cmat 20194   matToPolyMat cmat2pmat 20490 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-ot 4177  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-ofr 6883  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-ixp 7894  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-sup 8333  df-oi 8400  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-fz 12312  df-fzo 12450  df-seq 12785  df-hash 13101  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-sets 15845  df-ress 15846  df-plusg 15935  df-mulr 15936  df-sca 15938  df-vsca 15939  df-ip 15940  df-tset 15941  df-ple 15942  df-ds 15945  df-hom 15947  df-cco 15948  df-0g 16083  df-gsum 16084  df-prds 16089  df-pws 16091  df-mre 16227  df-mrc 16228  df-acs 16230  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-mhm 17316  df-submnd 17317  df-grp 17406  df-minusg 17407  df-sbg 17408  df-mulg 17522  df-subg 17572  df-ghm 17639  df-cntz 17731  df-cmn 18176  df-abl 18177  df-mgp 18471  df-ur 18483  df-ring 18530  df-subrg 18759  df-lmod 18846  df-lss 18914  df-sra 19153  df-rgmod 19154  df-ascl 19295  df-psr 19337  df-mpl 19339  df-opsr 19341  df-psr1 19531  df-ply1 19533  df-dsmm 20057  df-frlm 20072  df-mamu 20171  df-mat 20195  df-mat2pmat 20493 This theorem is referenced by:  chfacfscmulcl  20643  chfacfscmulgsum  20646  chfacfpmmulcl  20647  chfacfpmmulgsum  20650
 Copyright terms: Public domain W3C validator