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

Theorem pmatcollpw3fi1lem1 22018
Description: Lemma 1 for pmatcollpw3fi1 22020. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.)
Hypotheses
Ref Expression
pmatcollpw.p 𝑃 = (Poly1𝑅)
pmatcollpw.c 𝐶 = (𝑁 Mat 𝑃)
pmatcollpw.b 𝐵 = (Base‘𝐶)
pmatcollpw.m = ( ·𝑠𝐶)
pmatcollpw.e = (.g‘(mulGrp‘𝑃))
pmatcollpw.x 𝑋 = (var1𝑅)
pmatcollpw.t 𝑇 = (𝑁 matToPolyMat 𝑅)
pmatcollpw3.a 𝐴 = (𝑁 Mat 𝑅)
pmatcollpw3.d 𝐷 = (Base‘𝐴)
pmatcollpw3fi1lem1.0 0 = (0g𝐴)
pmatcollpw3fi1lem1.h 𝐻 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝐺‘0), 0 ))
Assertion
Ref Expression
pmatcollpw3fi1lem1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))))
Distinct variable groups:   𝐵,𝑛   𝑛,𝑀   𝑛,𝑁   𝑃,𝑛   𝑅,𝑛   𝑛,𝑋   ,𝑛   𝐶,𝑛   𝐵,𝑙   𝑀,𝑙   𝑁,𝑙   𝑅,𝑙   𝐷,𝑙,𝑛   𝐴,𝑙   𝐺,𝑙,𝑛
Allowed substitution hints:   𝐴(𝑛)   𝐶(𝑙)   𝑃(𝑙)   𝑇(𝑛,𝑙)   (𝑙)   𝐻(𝑛,𝑙)   (𝑛,𝑙)   𝑋(𝑙)   0 (𝑛,𝑙)

Proof of Theorem pmatcollpw3fi1lem1
StepHypRef Expression
1 simpr 485 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛))))))
2 pmatcollpw.p . . . . . . . . . . 11 𝑃 = (Poly1𝑅)
3 pmatcollpw.c . . . . . . . . . . 11 𝐶 = (𝑁 Mat 𝑃)
42, 3pmatring 21924 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
5 ringmnd 19868 . . . . . . . . . 10 (𝐶 ∈ Ring → 𝐶 ∈ Mnd)
64, 5syl 17 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Mnd)
76adantr 481 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → 𝐶 ∈ Mnd)
8 pmatcollpw.b . . . . . . . . 9 𝐵 = (Base‘𝐶)
9 ringcmn 19895 . . . . . . . . . . 11 (𝐶 ∈ Ring → 𝐶 ∈ CMnd)
104, 9syl 17 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ CMnd)
1110adantr 481 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → 𝐶 ∈ CMnd)
12 snfi 8888 . . . . . . . . . 10 {0} ∈ Fin
1312a1i 11 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → {0} ∈ Fin)
14 simplll 772 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → 𝑁 ∈ Fin)
15 simpllr 773 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → 𝑅 ∈ Ring)
16 elmapi 8687 . . . . . . . . . . . . 13 (𝐺 ∈ (𝐷m {0}) → 𝐺:{0}⟶𝐷)
1716adantl 482 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → 𝐺:{0}⟶𝐷)
1817ffvelcdmda 7001 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → (𝐺𝑛) ∈ 𝐷)
19 elsni 4588 . . . . . . . . . . . . 13 (𝑛 ∈ {0} → 𝑛 = 0)
20 0nn0 12328 . . . . . . . . . . . . 13 0 ∈ ℕ0
2119, 20eqeltrdi 2846 . . . . . . . . . . . 12 (𝑛 ∈ {0} → 𝑛 ∈ ℕ0)
2221adantl 482 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → 𝑛 ∈ ℕ0)
23 pmatcollpw3.a . . . . . . . . . . . 12 𝐴 = (𝑁 Mat 𝑅)
24 pmatcollpw3.d . . . . . . . . . . . 12 𝐷 = (Base‘𝐴)
25 pmatcollpw.t . . . . . . . . . . . 12 𝑇 = (𝑁 matToPolyMat 𝑅)
26 pmatcollpw.m . . . . . . . . . . . 12 = ( ·𝑠𝐶)
27 pmatcollpw.e . . . . . . . . . . . 12 = (.g‘(mulGrp‘𝑃))
28 pmatcollpw.x . . . . . . . . . . . 12 𝑋 = (var1𝑅)
2923, 24, 25, 2, 3, 8, 26, 27, 28mat2pmatscmxcl 21972 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐺𝑛) ∈ 𝐷𝑛 ∈ ℕ0)) → ((𝑛 𝑋) (𝑇‘(𝐺𝑛))) ∈ 𝐵)
3014, 15, 18, 22, 29syl22anc 836 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → ((𝑛 𝑋) (𝑇‘(𝐺𝑛))) ∈ 𝐵)
3130ralrimiva 3140 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → ∀𝑛 ∈ {0} ((𝑛 𝑋) (𝑇‘(𝐺𝑛))) ∈ 𝐵)
328, 11, 13, 31gsummptcl 19643 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛))))) ∈ 𝐵)
33 eqid 2737 . . . . . . . . 9 (+g𝐶) = (+g𝐶)
34 eqid 2737 . . . . . . . . 9 (0g𝐶) = (0g𝐶)
358, 33, 34mndrid 18483 . . . . . . . 8 ((𝐶 ∈ Mnd ∧ (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛))))) ∈ 𝐵) → ((𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))(+g𝐶)(0g𝐶)) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛))))))
367, 32, 35syl2anc 584 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → ((𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))(+g𝐶)(0g𝐶)) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛))))))
37 fz0sn 13436 . . . . . . . . . . . 12 (0...0) = {0}
3837eqcomi 2746 . . . . . . . . . . 11 {0} = (0...0)
3938a1i 11 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → {0} = (0...0))
40 pmatcollpw3fi1lem1.h . . . . . . . . . . . . . 14 𝐻 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝐺‘0), 0 ))
41 simpr 485 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑙 = 𝑛)
4219ad2antlr 724 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑛 = 0)
4341, 42eqtrd 2777 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑙 = 0)
4443iftrued 4479 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (𝐺‘0))
45 fveq2 6812 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → (𝐺𝑛) = (𝐺‘0))
4645eqcomd 2743 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → (𝐺‘0) = (𝐺𝑛))
4719, 46syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ {0} → (𝐺‘0) = (𝐺𝑛))
4847ad2antlr 724 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → (𝐺‘0) = (𝐺𝑛))
4944, 48eqtrd 2777 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (𝐺𝑛))
50 1nn0 12329 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℕ0
5150a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 0 → 1 ∈ ℕ0)
52 nn0uz 12700 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
5351, 52eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → 1 ∈ (ℤ‘0))
54 eluzfz1 13343 . . . . . . . . . . . . . . . . . 18 (1 ∈ (ℤ‘0) → 0 ∈ (0...1))
5553, 54syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → 0 ∈ (0...1))
56 eleq1 2825 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → (𝑛 ∈ (0...1) ↔ 0 ∈ (0...1)))
5755, 56mpbird 256 . . . . . . . . . . . . . . . 16 (𝑛 = 0 → 𝑛 ∈ (0...1))
5819, 57syl 17 . . . . . . . . . . . . . . 15 (𝑛 ∈ {0} → 𝑛 ∈ (0...1))
5958adantl 482 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → 𝑛 ∈ (0...1))
60 ffvelcdm 6999 . . . . . . . . . . . . . . . . . 18 ((𝐺:{0}⟶𝐷𝑛 ∈ {0}) → (𝐺𝑛) ∈ 𝐷)
6160ex 413 . . . . . . . . . . . . . . . . 17 (𝐺:{0}⟶𝐷 → (𝑛 ∈ {0} → (𝐺𝑛) ∈ 𝐷))
6216, 61syl 17 . . . . . . . . . . . . . . . 16 (𝐺 ∈ (𝐷m {0}) → (𝑛 ∈ {0} → (𝐺𝑛) ∈ 𝐷))
6362adantl 482 . . . . . . . . . . . . . . 15 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (𝑛 ∈ {0} → (𝐺𝑛) ∈ 𝐷))
6463imp 407 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → (𝐺𝑛) ∈ 𝐷)
6540, 49, 59, 64fvmptd2 6923 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → (𝐻𝑛) = (𝐺𝑛))
6665eqcomd 2743 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → (𝐺𝑛) = (𝐻𝑛))
6766fveq2d 6816 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → (𝑇‘(𝐺𝑛)) = (𝑇‘(𝐻𝑛)))
6867oveq2d 7333 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ {0}) → ((𝑛 𝑋) (𝑇‘(𝐺𝑛))) = ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))
6939, 68mpteq12dva 5176 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))) = (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))
7069oveq2d 7333 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))))
71 ovexd 7352 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (0 + 1) ∈ V)
728, 34mndidcl 18477 . . . . . . . . . . . 12 (𝐶 ∈ Mnd → (0g𝐶) ∈ 𝐵)
736, 72syl 17 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g𝐶) ∈ 𝐵)
7473adantr 481 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (0g𝐶) ∈ 𝐵)
75 0p1e1 12175 . . . . . . . . . . . . . . . . . . . . 21 (0 + 1) = 1
7675eqeq2i 2750 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = (0 + 1) ↔ 𝑛 = 1)
77 ax-1ne0 11020 . . . . . . . . . . . . . . . . . . . . . 22 1 ≠ 0
7877neii 2943 . . . . . . . . . . . . . . . . . . . . 21 ¬ 1 = 0
79 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 1 → (𝑛 = 0 ↔ 1 = 0))
8078, 79mtbiri 326 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → ¬ 𝑛 = 0)
8176, 80sylbi 216 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (0 + 1) → ¬ 𝑛 = 0)
8281ad2antlr 724 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → ¬ 𝑛 = 0)
83 eqeq1 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0))
8483notbid 317 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑛 → (¬ 𝑙 = 0 ↔ ¬ 𝑛 = 0))
8584adantl 482 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → (¬ 𝑙 = 0 ↔ ¬ 𝑛 = 0))
8682, 85mpbird 256 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → ¬ 𝑙 = 0)
8786iffalsed 4482 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = 0 )
88 pmatcollpw3fi1lem1.0 . . . . . . . . . . . . . . . 16 0 = (0g𝐴)
8987, 88eqtrdi 2793 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (0g𝐴))
9050a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → 1 ∈ ℕ0)
9190, 52eleqtrdi 2848 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → 1 ∈ (ℤ‘0))
92 eluzfz2 13344 . . . . . . . . . . . . . . . . . . 19 (1 ∈ (ℤ‘0) → 1 ∈ (0...1))
9391, 92syl 17 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → 1 ∈ (0...1))
94 eleq1 2825 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (𝑛 ∈ (0...1) ↔ 1 ∈ (0...1)))
9593, 94mpbird 256 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → 𝑛 ∈ (0...1))
9676, 95sylbi 216 . . . . . . . . . . . . . . . 16 (𝑛 = (0 + 1) → 𝑛 ∈ (0...1))
9796adantl 482 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → 𝑛 ∈ (0...1))
98 fvexd 6827 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → (0g𝐴) ∈ V)
9940, 89, 97, 98fvmptd2 6923 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → (𝐻𝑛) = (0g𝐴))
10099fveq2d 6816 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → (𝑇‘(𝐻𝑛)) = (𝑇‘(0g𝐴)))
10123fveq2i 6815 . . . . . . . . . . . . . . . 16 (0g𝐴) = (0g‘(𝑁 Mat 𝑅))
1023fveq2i 6815 . . . . . . . . . . . . . . . 16 (0g𝐶) = (0g‘(𝑁 Mat 𝑃))
10325, 2, 101, 1020mat2pmat 21968 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → (𝑇‘(0g𝐴)) = (0g𝐶))
104103ancoms 459 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(0g𝐴)) = (0g𝐶))
105104ad2antrr 723 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → (𝑇‘(0g𝐴)) = (0g𝐶))
106100, 105eqtrd 2777 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → (𝑇‘(𝐻𝑛)) = (0g𝐶))
107106oveq2d 7333 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → ((𝑛 𝑋) (𝑇‘(𝐻𝑛))) = ((𝑛 𝑋) (0g𝐶)))
1082, 3pmatlmod 21925 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod)
109108ad2antrr 723 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → 𝐶 ∈ LMod)
110 simpllr 773 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → 𝑅 ∈ Ring)
111 eleq1 2825 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (𝑛 ∈ ℕ0 ↔ 1 ∈ ℕ0))
11290, 111mpbird 256 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → 𝑛 ∈ ℕ0)
11376, 112sylbi 216 . . . . . . . . . . . . . . 15 (𝑛 = (0 + 1) → 𝑛 ∈ ℕ0)
114113adantl 482 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → 𝑛 ∈ ℕ0)
115 eqid 2737 . . . . . . . . . . . . . . 15 (mulGrp‘𝑃) = (mulGrp‘𝑃)
116 eqid 2737 . . . . . . . . . . . . . . 15 (Base‘𝑃) = (Base‘𝑃)
1172, 28, 115, 27, 116ply1moncl 21525 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0) → (𝑛 𝑋) ∈ (Base‘𝑃))
118110, 114, 117syl2anc 584 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → (𝑛 𝑋) ∈ (Base‘𝑃))
1192ply1ring 21502 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
1203matsca2 21652 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝑃 = (Scalar‘𝐶))
121119, 120sylan2 593 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑃 = (Scalar‘𝐶))
122121eqcomd 2743 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Scalar‘𝐶) = 𝑃)
123122fveq2d 6816 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(Scalar‘𝐶)) = (Base‘𝑃))
124123eleq2d 2823 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑛 𝑋) ∈ (Base‘(Scalar‘𝐶)) ↔ (𝑛 𝑋) ∈ (Base‘𝑃)))
125124ad2antrr 723 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → ((𝑛 𝑋) ∈ (Base‘(Scalar‘𝐶)) ↔ (𝑛 𝑋) ∈ (Base‘𝑃)))
126118, 125mpbird 256 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → (𝑛 𝑋) ∈ (Base‘(Scalar‘𝐶)))
127 eqid 2737 . . . . . . . . . . . . 13 (Scalar‘𝐶) = (Scalar‘𝐶)
128 eqid 2737 . . . . . . . . . . . . 13 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
129127, 26, 128, 34lmodvs0 20240 . . . . . . . . . . . 12 ((𝐶 ∈ LMod ∧ (𝑛 𝑋) ∈ (Base‘(Scalar‘𝐶))) → ((𝑛 𝑋) (0g𝐶)) = (0g𝐶))
130109, 126, 129syl2anc 584 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → ((𝑛 𝑋) (0g𝐶)) = (0g𝐶))
131107, 130eqtrd 2777 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 = (0 + 1)) → ((𝑛 𝑋) (𝑇‘(𝐻𝑛))) = (0g𝐶))
1328, 7, 71, 74, 131gsumsnd 19628 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))) = (0g𝐶))
133132eqcomd 2743 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (0g𝐶) = (𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))))
13470, 133oveq12d 7335 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → ((𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))(+g𝐶)(0g𝐶)) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))(+g𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))))
13536, 134eqtr3d 2779 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))(+g𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))))
136135adantr 481 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))) → (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))(+g𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))))
1371, 136eqtrd 2777 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))) → 𝑀 = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))(+g𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))))
1381373impa 1109 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))) → 𝑀 = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))(+g𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))))
13920a1i 11 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → 0 ∈ ℕ0)
140 simplll 772 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) → 𝑁 ∈ Fin)
141 simpllr 773 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) → 𝑅 ∈ Ring)
142 id 22 . . . . . . . . . . . . 13 (𝐺:{0}⟶𝐷𝐺:{0}⟶𝐷)
143 c0ex 11049 . . . . . . . . . . . . . . 15 0 ∈ V
144143snid 4607 . . . . . . . . . . . . . 14 0 ∈ {0}
145144a1i 11 . . . . . . . . . . . . 13 (𝐺:{0}⟶𝐷 → 0 ∈ {0})
146142, 145ffvelcdmd 7002 . . . . . . . . . . . 12 (𝐺:{0}⟶𝐷 → (𝐺‘0) ∈ 𝐷)
14716, 146syl 17 . . . . . . . . . . 11 (𝐺 ∈ (𝐷m {0}) → (𝐺‘0) ∈ 𝐷)
148147ad2antlr 724 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑙 ∈ (0...1)) → (𝐺‘0) ∈ 𝐷)
14923matring 21675 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
15024, 88ring0cl 19883 . . . . . . . . . . . 12 (𝐴 ∈ Ring → 0𝐷)
151149, 150syl 17 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0𝐷)
152151ad2antrr 723 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑙 ∈ (0...1)) → 0𝐷)
153148, 152ifcld 4517 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑙 ∈ (0...1)) → if(𝑙 = 0, (𝐺‘0), 0 ) ∈ 𝐷)
154153, 40fmptd 7028 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → 𝐻:(0...1)⟶𝐷)
15575oveq2i 7328 . . . . . . . . 9 (0...(0 + 1)) = (0...1)
156155feq2i 6630 . . . . . . . 8 (𝐻:(0...(0 + 1))⟶𝐷𝐻:(0...1)⟶𝐷)
157154, 156sylibr 233 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → 𝐻:(0...(0 + 1))⟶𝐷)
158157ffvelcdmda 7001 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) → (𝐻𝑛) ∈ 𝐷)
159 elfznn0 13429 . . . . . . 7 (𝑛 ∈ (0...(0 + 1)) → 𝑛 ∈ ℕ0)
160159adantl 482 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) → 𝑛 ∈ ℕ0)
16123, 24, 25, 2, 3, 8, 26, 27, 28mat2pmatscmxcl 21972 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐻𝑛) ∈ 𝐷𝑛 ∈ ℕ0)) → ((𝑛 𝑋) (𝑇‘(𝐻𝑛))) ∈ 𝐵)
162140, 141, 158, 160, 161syl22anc 836 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) → ((𝑛 𝑋) (𝑇‘(𝐻𝑛))) ∈ 𝐵)
1638, 33, 11, 139, 162gsummptfzsplit 19608 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0})) → (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))(+g𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))))
1641633adant3 1131 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))) → (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))(+g𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))))
165138, 164eqtr4d 2780 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))))
166155mpteq1i 5183 . . 3 (𝑛 ∈ (0...(0 + 1)) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))) = (𝑛 ∈ (0...1) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))
167166oveq2i 7328 . 2 (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛)))))
168165, 167eqtrdi 2793 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 𝑋) (𝑇‘(𝐺𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 𝑋) (𝑇‘(𝐻𝑛))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  Vcvv 3441  ifcif 4471  {csn 4571  cmpt 5170  wf 6462  cfv 6466  (class class class)co 7317  m cmap 8665  Fincfn 8783  0cc0 10951  1c1 10952   + caddc 10954  0cn0 12313  cuz 12662  ...cfz 13319  Basecbs 16989  +gcplusg 17039  Scalarcsca 17042   ·𝑠 cvsca 17043  0gc0g 17227   Σg cgsu 17228  Mndcmnd 18462  .gcmg 18776  CMndccmn 19461  mulGrpcmgp 19795  Ringcrg 19858  LModclmod 20206  var1cv1 21430  Poly1cpl1 21431   Mat cmat 21637   matToPolyMat cmat2pmat 21936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  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 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-ot 4580  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-se 5564  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-isom 6475  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-of 7575  df-ofr 7576  df-om 7760  df-1st 7878  df-2nd 7879  df-supp 8027  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-er 8548  df-map 8667  df-pm 8668  df-ixp 8736  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-fsupp 9206  df-sup 9278  df-oi 9346  df-card 9775  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-nn 12054  df-2 12116  df-3 12117  df-4 12118  df-5 12119  df-6 12120  df-7 12121  df-8 12122  df-9 12123  df-n0 12314  df-z 12400  df-dec 12518  df-uz 12663  df-fz 13320  df-fzo 13463  df-seq 13802  df-hash 14125  df-struct 16925  df-sets 16942  df-slot 16960  df-ndx 16972  df-base 16990  df-ress 17019  df-plusg 17052  df-mulr 17053  df-sca 17055  df-vsca 17056  df-ip 17057  df-tset 17058  df-ple 17059  df-ds 17061  df-hom 17063  df-cco 17064  df-0g 17229  df-gsum 17230  df-prds 17235  df-pws 17237  df-mre 17372  df-mrc 17373  df-acs 17375  df-mgm 18403  df-sgrp 18452  df-mnd 18463  df-mhm 18507  df-submnd 18508  df-grp 18656  df-minusg 18657  df-sbg 18658  df-mulg 18777  df-subg 18828  df-ghm 18908  df-cntz 18999  df-cmn 19463  df-abl 19464  df-mgp 19796  df-ur 19813  df-ring 19860  df-subrg 20104  df-lmod 20208  df-lss 20277  df-sra 20517  df-rgmod 20518  df-dsmm 21022  df-frlm 21037  df-ascl 21145  df-psr 21195  df-mvr 21196  df-mpl 21197  df-opsr 21199  df-psr1 21434  df-vr1 21435  df-ply1 21436  df-mamu 21616  df-mat 21638  df-mat2pmat 21939
This theorem is referenced by:  pmatcollpw3fi1lem2  22019
  Copyright terms: Public domain W3C validator