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

Theorem monmatcollpw 21469
 Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix having scaled monomials with the same power as entries is the matrix of the coefficients of the monomials or a zero matrix. Generalization of decpmatid 21460 (but requires 𝑅 to be commutative!). (Contributed by AV, 11-Nov-2019.) (Revised by AV, 4-Dec-2019.)
Hypotheses
Ref Expression
monmatcollpw.p 𝑃 = (Poly1𝑅)
monmatcollpw.c 𝐶 = (𝑁 Mat 𝑃)
monmatcollpw.a 𝐴 = (𝑁 Mat 𝑅)
monmatcollpw.k 𝐾 = (Base‘𝐴)
monmatcollpw.0 0 = (0g𝐴)
monmatcollpw.e = (.g‘(mulGrp‘𝑃))
monmatcollpw.x 𝑋 = (var1𝑅)
monmatcollpw.m · = ( ·𝑠𝐶)
monmatcollpw.t 𝑇 = (𝑁 matToPolyMat 𝑅)
Assertion
Ref Expression
monmatcollpw (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (((𝐿 𝑋) · (𝑇𝑀)) decompPMat 𝐼) = if(𝐼 = 𝐿, 𝑀, 0 ))

Proof of Theorem monmatcollpw
Dummy variables 𝑖 𝑗 𝑙 𝑥 𝑦 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 767 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 𝑁 ∈ Fin)
2 crngring 19367 . . . . . 6 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
3 monmatcollpw.p . . . . . . 7 𝑃 = (Poly1𝑅)
43ply1ring 20962 . . . . . 6 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
52, 4syl 17 . . . . 5 (𝑅 ∈ CRing → 𝑃 ∈ Ring)
65ad2antlr 727 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 𝑃 ∈ Ring)
72adantl 486 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring)
8 simp2 1135 . . . . . 6 ((𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0) → 𝐿 ∈ ℕ0)
9 monmatcollpw.x . . . . . . 7 𝑋 = (var1𝑅)
10 eqid 2759 . . . . . . 7 (mulGrp‘𝑃) = (mulGrp‘𝑃)
11 monmatcollpw.e . . . . . . 7 = (.g‘(mulGrp‘𝑃))
12 eqid 2759 . . . . . . 7 (Base‘𝑃) = (Base‘𝑃)
133, 9, 10, 11, 12ply1moncl 20985 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝐿 ∈ ℕ0) → (𝐿 𝑋) ∈ (Base‘𝑃))
147, 8, 13syl2an 599 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (𝐿 𝑋) ∈ (Base‘𝑃))
152anim2i 620 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
16 simp1 1134 . . . . . . . 8 ((𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0) → 𝑀𝐾)
1715, 16anim12i 616 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑀𝐾))
18 df-3an 1087 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐾) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑀𝐾))
1917, 18sylibr 237 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐾))
20 monmatcollpw.t . . . . . . 7 𝑇 = (𝑁 matToPolyMat 𝑅)
21 monmatcollpw.a . . . . . . 7 𝐴 = (𝑁 Mat 𝑅)
22 monmatcollpw.k . . . . . . 7 𝐾 = (Base‘𝐴)
23 monmatcollpw.c . . . . . . 7 𝐶 = (𝑁 Mat 𝑃)
2420, 21, 22, 3, 23mat2pmatbas 21416 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐾) → (𝑇𝑀) ∈ (Base‘𝐶))
2519, 24syl 17 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (𝑇𝑀) ∈ (Base‘𝐶))
2614, 25jca 516 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → ((𝐿 𝑋) ∈ (Base‘𝑃) ∧ (𝑇𝑀) ∈ (Base‘𝐶)))
27 eqid 2759 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
28 monmatcollpw.m . . . . 5 · = ( ·𝑠𝐶)
2912, 23, 27, 28matvscl 21121 . . . 4 (((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ ((𝐿 𝑋) ∈ (Base‘𝑃) ∧ (𝑇𝑀) ∈ (Base‘𝐶))) → ((𝐿 𝑋) · (𝑇𝑀)) ∈ (Base‘𝐶))
301, 6, 26, 29syl21anc 837 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → ((𝐿 𝑋) · (𝑇𝑀)) ∈ (Base‘𝐶))
31 simpr3 1194 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 𝐼 ∈ ℕ0)
3223, 27decpmatval 21455 . . 3 ((((𝐿 𝑋) · (𝑇𝑀)) ∈ (Base‘𝐶) ∧ 𝐼 ∈ ℕ0) → (((𝐿 𝑋) · (𝑇𝑀)) decompPMat 𝐼) = (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖((𝐿 𝑋) · (𝑇𝑀))𝑗))‘𝐼)))
3330, 31, 32syl2anc 588 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (((𝐿 𝑋) · (𝑇𝑀)) decompPMat 𝐼) = (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖((𝐿 𝑋) · (𝑇𝑀))𝑗))‘𝐼)))
3463ad2ant1 1131 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → 𝑃 ∈ Ring)
35263ad2ant1 1131 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((𝐿 𝑋) ∈ (Base‘𝑃) ∧ (𝑇𝑀) ∈ (Base‘𝐶)))
36 3simpc 1148 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (𝑖𝑁𝑗𝑁))
37 eqid 2759 . . . . . . . 8 (.r𝑃) = (.r𝑃)
3823, 27, 12, 28, 37matvscacell 21126 . . . . . . 7 ((𝑃 ∈ Ring ∧ ((𝐿 𝑋) ∈ (Base‘𝑃) ∧ (𝑇𝑀) ∈ (Base‘𝐶)) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖((𝐿 𝑋) · (𝑇𝑀))𝑗) = ((𝐿 𝑋)(.r𝑃)(𝑖(𝑇𝑀)𝑗)))
3934, 35, 36, 38syl3anc 1369 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (𝑖((𝐿 𝑋) · (𝑇𝑀))𝑗) = ((𝐿 𝑋)(.r𝑃)(𝑖(𝑇𝑀)𝑗)))
4039fveq2d 6660 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (coe1‘(𝑖((𝐿 𝑋) · (𝑇𝑀))𝑗)) = (coe1‘((𝐿 𝑋)(.r𝑃)(𝑖(𝑇𝑀)𝑗))))
4140fveq1d 6658 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((coe1‘(𝑖((𝐿 𝑋) · (𝑇𝑀))𝑗))‘𝐼) = ((coe1‘((𝐿 𝑋)(.r𝑃)(𝑖(𝑇𝑀)𝑗)))‘𝐼))
4216anim2i 620 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀𝐾))
43 df-3an 1087 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐾) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀𝐾))
4442, 43sylibr 237 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐾))
45443ad2ant1 1131 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐾))
46 eqid 2759 . . . . . . . . . 10 (algSc‘𝑃) = (algSc‘𝑃)
4720, 21, 22, 3, 46mat2pmatvalel 21415 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐾) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖(𝑇𝑀)𝑗) = ((algSc‘𝑃)‘(𝑖𝑀𝑗)))
4845, 36, 47syl2anc 588 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (𝑖(𝑇𝑀)𝑗) = ((algSc‘𝑃)‘(𝑖𝑀𝑗)))
4948oveq2d 7164 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((𝐿 𝑋)(.r𝑃)(𝑖(𝑇𝑀)𝑗)) = ((𝐿 𝑋)(.r𝑃)((algSc‘𝑃)‘(𝑖𝑀𝑗))))
503ply1assa 20913 . . . . . . . . . 10 (𝑅 ∈ CRing → 𝑃 ∈ AssAlg)
5150ad2antlr 727 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 𝑃 ∈ AssAlg)
52513ad2ant1 1131 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → 𝑃 ∈ AssAlg)
53 eqid 2759 . . . . . . . . . 10 (Base‘𝑅) = (Base‘𝑅)
54 eqid 2759 . . . . . . . . . 10 (Base‘𝐴) = (Base‘𝐴)
55 simp2 1135 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → 𝑖𝑁)
56 simp3 1136 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → 𝑗𝑁)
5722eleq2i 2844 . . . . . . . . . . . . . 14 (𝑀𝐾𝑀 ∈ (Base‘𝐴))
5857biimpi 219 . . . . . . . . . . . . 13 (𝑀𝐾𝑀 ∈ (Base‘𝐴))
59583ad2ant1 1131 . . . . . . . . . . . 12 ((𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0) → 𝑀 ∈ (Base‘𝐴))
6059adantl 486 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 𝑀 ∈ (Base‘𝐴))
61603ad2ant1 1131 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → 𝑀 ∈ (Base‘𝐴))
6221, 53, 54, 55, 56, 61matecld 21116 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (𝑖𝑀𝑗) ∈ (Base‘𝑅))
633ply1sca 20967 . . . . . . . . . . . . . 14 (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃))
6463adantl 486 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝑃))
6564eqcomd 2765 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (Scalar‘𝑃) = 𝑅)
6665fveq2d 6660 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
6766adantr 485 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
68673ad2ant1 1131 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
6962, 68eleqtrrd 2856 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (𝑖𝑀𝑗) ∈ (Base‘(Scalar‘𝑃)))
70143ad2ant1 1131 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (𝐿 𝑋) ∈ (Base‘𝑃))
71 eqid 2759 . . . . . . . . 9 (Scalar‘𝑃) = (Scalar‘𝑃)
72 eqid 2759 . . . . . . . . 9 (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
73 eqid 2759 . . . . . . . . 9 ( ·𝑠𝑃) = ( ·𝑠𝑃)
7446, 71, 72, 12, 37, 73asclmul2 20639 . . . . . . . 8 ((𝑃 ∈ AssAlg ∧ (𝑖𝑀𝑗) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝐿 𝑋) ∈ (Base‘𝑃)) → ((𝐿 𝑋)(.r𝑃)((algSc‘𝑃)‘(𝑖𝑀𝑗))) = ((𝑖𝑀𝑗)( ·𝑠𝑃)(𝐿 𝑋)))
7552, 69, 70, 74syl3anc 1369 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((𝐿 𝑋)(.r𝑃)((algSc‘𝑃)‘(𝑖𝑀𝑗))) = ((𝑖𝑀𝑗)( ·𝑠𝑃)(𝐿 𝑋)))
7649, 75eqtrd 2794 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((𝐿 𝑋)(.r𝑃)(𝑖(𝑇𝑀)𝑗)) = ((𝑖𝑀𝑗)( ·𝑠𝑃)(𝐿 𝑋)))
7776fveq2d 6660 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (coe1‘((𝐿 𝑋)(.r𝑃)(𝑖(𝑇𝑀)𝑗))) = (coe1‘((𝑖𝑀𝑗)( ·𝑠𝑃)(𝐿 𝑋))))
7877fveq1d 6658 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((coe1‘((𝐿 𝑋)(.r𝑃)(𝑖(𝑇𝑀)𝑗)))‘𝐼) = ((coe1‘((𝑖𝑀𝑗)( ·𝑠𝑃)(𝐿 𝑋)))‘𝐼))
792ad2antlr 727 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 𝑅 ∈ Ring)
80793ad2ant1 1131 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → 𝑅 ∈ Ring)
81 simp1r2 1268 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → 𝐿 ∈ ℕ0)
82 eqid 2759 . . . . . . 7 (0g𝑅) = (0g𝑅)
8382, 53, 3, 9, 73, 10, 11coe1tm 20987 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑖𝑀𝑗) ∈ (Base‘𝑅) ∧ 𝐿 ∈ ℕ0) → (coe1‘((𝑖𝑀𝑗)( ·𝑠𝑃)(𝐿 𝑋))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅))))
8480, 62, 81, 83syl3anc 1369 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (coe1‘((𝑖𝑀𝑗)( ·𝑠𝑃)(𝐿 𝑋))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅))))
8584fveq1d 6658 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((coe1‘((𝑖𝑀𝑗)( ·𝑠𝑃)(𝐿 𝑋)))‘𝐼) = ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼))
8641, 78, 853eqtrd 2798 . . 3 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((coe1‘(𝑖((𝐿 𝑋) · (𝑇𝑀))𝑗))‘𝐼) = ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼))
8786mpoeq3dva 7223 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖((𝐿 𝑋) · (𝑇𝑀))𝑗))‘𝐼)) = (𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼)))
88 monmatcollpw.0 . . . . . . . . 9 0 = (0g𝐴)
8915adantr 485 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
9089adantr 485 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
9121, 82mat0op 21109 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g𝐴) = (𝑧𝑁, 𝑤𝑁 ↦ (0g𝑅)))
9290, 91syl 17 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (0g𝐴) = (𝑧𝑁, 𝑤𝑁 ↦ (0g𝑅)))
9388, 92syl5eq 2806 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → 0 = (𝑧𝑁, 𝑤𝑁 ↦ (0g𝑅)))
94 eqidd 2760 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) ∧ (𝑧 = 𝑥𝑤 = 𝑦)) → (0g𝑅) = (0g𝑅))
95 simprl 771 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → 𝑥𝑁)
96 simprr 773 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → 𝑦𝑁)
97 fvexd 6671 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (0g𝑅) ∈ V)
9893, 94, 95, 96, 97ovmpod 7295 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (𝑥 0 𝑦) = (0g𝑅))
9998eqcomd 2765 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (0g𝑅) = (𝑥 0 𝑦))
10099ifeq2d 4438 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → if(𝐼 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)) = if(𝐼 = 𝐿, (𝑥𝑀𝑦), (𝑥 0 𝑦)))
101 eqidd 2760 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼)) = (𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼)))
102 oveq12 7157 . . . . . . . . . 10 ((𝑖 = 𝑥𝑗 = 𝑦) → (𝑖𝑀𝑗) = (𝑥𝑀𝑦))
103102ifeq1d 4437 . . . . . . . . 9 ((𝑖 = 𝑥𝑗 = 𝑦) → if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)) = if(𝑙 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)))
104103mpteq2dv 5126 . . . . . . . 8 ((𝑖 = 𝑥𝑗 = 𝑦) → (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑥𝑀𝑦), (0g𝑅))))
105104fveq1d 6658 . . . . . . 7 ((𝑖 = 𝑥𝑗 = 𝑦) → ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼) = ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)))‘𝐼))
106 eqidd 2760 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑥𝑀𝑦), (0g𝑅))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑥𝑀𝑦), (0g𝑅))))
107 eqeq1 2763 . . . . . . . . . 10 (𝑙 = 𝐼 → (𝑙 = 𝐿𝐼 = 𝐿))
108107ifbid 4441 . . . . . . . . 9 (𝑙 = 𝐼 → if(𝑙 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)) = if(𝐼 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)))
109108adantl 486 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑙 = 𝐼) → if(𝑙 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)) = if(𝐼 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)))
11031adantr 485 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → 𝐼 ∈ ℕ0)
111 ovex 7181 . . . . . . . . . 10 (𝑥𝑀𝑦) ∈ V
112 fvex 6669 . . . . . . . . . 10 (0g𝑅) ∈ V
113111, 112ifex 4468 . . . . . . . . 9 if(𝐼 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)) ∈ V
114113a1i 11 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → if(𝐼 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)) ∈ V)
115106, 109, 110, 114fvmptd 6764 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)))‘𝐼) = if(𝐼 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)))
116105, 115sylan9eqr 2816 . . . . . 6 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) ∧ (𝑖 = 𝑥𝑗 = 𝑦)) → ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼) = if(𝐼 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)))
117101, 116, 95, 96, 114ovmpod 7295 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (𝑥(𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼))𝑦) = if(𝐼 = 𝐿, (𝑥𝑀𝑦), (0g𝑅)))
118 ifov 7246 . . . . . 6 (𝑥if(𝐼 = 𝐿, 𝑀, 0 )𝑦) = if(𝐼 = 𝐿, (𝑥𝑀𝑦), (𝑥 0 𝑦))
119118a1i 11 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (𝑥if(𝐼 = 𝐿, 𝑀, 0 )𝑦) = if(𝐼 = 𝐿, (𝑥𝑀𝑦), (𝑥 0 𝑦)))
120100, 117, 1193eqtr4d 2804 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ (𝑥𝑁𝑦𝑁)) → (𝑥(𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼))𝑦) = (𝑥if(𝐼 = 𝐿, 𝑀, 0 )𝑦))
121120ralrimivva 3121 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → ∀𝑥𝑁𝑦𝑁 (𝑥(𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼))𝑦) = (𝑥if(𝐼 = 𝐿, 𝑀, 0 )𝑦))
122 simplr 769 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 𝑅 ∈ CRing)
123 eqidd 2760 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅))))
124107ifbid 4441 . . . . . . . 8 (𝑙 = 𝐼 → if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)) = if(𝐼 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))
125124adantl 486 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) ∧ 𝑙 = 𝐼) → if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)) = if(𝐼 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))
126313ad2ant1 1131 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → 𝐼 ∈ ℕ0)
12753, 82ring0cl 19380 . . . . . . . . . . 11 (𝑅 ∈ Ring → (0g𝑅) ∈ (Base‘𝑅))
1287, 127syl 17 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (0g𝑅) ∈ (Base‘𝑅))
129128adantr 485 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (0g𝑅) ∈ (Base‘𝑅))
1301293ad2ant1 1131 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → (0g𝑅) ∈ (Base‘𝑅))
13162, 130ifcld 4464 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → if(𝐼 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)) ∈ (Base‘𝑅))
132123, 125, 126, 131fvmptd 6764 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼) = if(𝐼 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))
133132, 131eqeltrd 2853 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) ∧ 𝑖𝑁𝑗𝑁) → ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼) ∈ (Base‘𝑅))
13421, 53, 22, 1, 122, 133matbas2d 21113 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼)) ∈ 𝐾)
13560, 57sylibr 237 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 𝑀𝐾)
13621matring 21133 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
13722, 88ring0cl 19380 . . . . . . 7 (𝐴 ∈ Ring → 0𝐾)
13815, 136, 1373syl 18 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 0𝐾)
139138adantr 485 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → 0𝐾)
140135, 139ifcld 4464 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → if(𝐼 = 𝐿, 𝑀, 0 ) ∈ 𝐾)
14121, 22eqmat 21114 . . . 4 (((𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼)) ∈ 𝐾 ∧ if(𝐼 = 𝐿, 𝑀, 0 ) ∈ 𝐾) → ((𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼)) = if(𝐼 = 𝐿, 𝑀, 0 ) ↔ ∀𝑥𝑁𝑦𝑁 (𝑥(𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼))𝑦) = (𝑥if(𝐼 = 𝐿, 𝑀, 0 )𝑦)))
142134, 140, 141syl2anc 588 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → ((𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼)) = if(𝐼 = 𝐿, 𝑀, 0 ) ↔ ∀𝑥𝑁𝑦𝑁 (𝑥(𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼))𝑦) = (𝑥if(𝐼 = 𝐿, 𝑀, 0 )𝑦)))
143121, 142mpbird 260 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (𝑖𝑁, 𝑗𝑁 ↦ ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝐿, (𝑖𝑀𝑗), (0g𝑅)))‘𝐼)) = if(𝐼 = 𝐿, 𝑀, 0 ))
14433, 87, 1433eqtrd 2798 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀𝐾𝐿 ∈ ℕ0𝐼 ∈ ℕ0)) → (((𝐿 𝑋) · (𝑇𝑀)) decompPMat 𝐼) = if(𝐼 = 𝐿, 𝑀, 0 ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∀wral 3071  Vcvv 3410  ifcif 4418   ↦ cmpt 5110  ‘cfv 6333  (class class class)co 7148   ∈ cmpo 7150  Fincfn 8525  ℕ0cn0 11924  Basecbs 16531  .rcmulr 16614  Scalarcsca 16616   ·𝑠 cvsca 16617  0gc0g 16761  .gcmg 18281  mulGrpcmgp 19297  Ringcrg 19355  CRingccrg 19356  AssAlgcasa 20605  algSccascl 20607  var1cv1 20890  Poly1cpl1 20891  coe1cco1 20892   Mat cmat 21097   matToPolyMat cmat2pmat 21394   decompPMat cdecpmat 21452 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-pre-mulgt0 10642 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-ot 4529  df-uni 4797  df-int 4837  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-se 5482  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-isom 6342  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7403  df-ofr 7404  df-om 7578  df-1st 7691  df-2nd 7692  df-supp 7834  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-1o 8110  df-2o 8111  df-oadd 8114  df-er 8297  df-map 8416  df-pm 8417  df-ixp 8478  df-en 8526  df-dom 8527  df-sdom 8528  df-fin 8529  df-fsupp 8857  df-sup 8929  df-oi 8997  df-card 9391  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-sub 10900  df-neg 10901  df-nn 11665  df-2 11727  df-3 11728  df-4 11729  df-5 11730  df-6 11731  df-7 11732  df-8 11733  df-9 11734  df-n0 11925  df-z 12011  df-dec 12128  df-uz 12273  df-fz 12930  df-fzo 13073  df-seq 13409  df-hash 13731  df-struct 16533  df-ndx 16534  df-slot 16535  df-base 16537  df-sets 16538  df-ress 16539  df-plusg 16626  df-mulr 16627  df-sca 16629  df-vsca 16630  df-ip 16631  df-tset 16632  df-ple 16633  df-ds 16635  df-hom 16637  df-cco 16638  df-0g 16763  df-gsum 16764  df-prds 16769  df-pws 16771  df-mre 16905  df-mrc 16906  df-acs 16908  df-mgm 17908  df-sgrp 17957  df-mnd 17968  df-mhm 18012  df-submnd 18013  df-grp 18162  df-minusg 18163  df-sbg 18164  df-mulg 18282  df-subg 18333  df-ghm 18413  df-cntz 18504  df-cmn 18965  df-abl 18966  df-mgp 19298  df-ur 19310  df-ring 19357  df-cring 19358  df-subrg 19591  df-lmod 19694  df-lss 19762  df-sra 20002  df-rgmod 20003  df-dsmm 20487  df-frlm 20502  df-assa 20608  df-ascl 20610  df-psr 20661  df-mvr 20662  df-mpl 20663  df-opsr 20665  df-psr1 20894  df-vr1 20895  df-ply1 20896  df-coe1 20897  df-mamu 21076  df-mat 21098  df-mat2pmat 21397  df-decpmat 21453 This theorem is referenced by:  monmat2matmon  21514
 Copyright terms: Public domain W3C validator