Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cpmidpmatlem2 | Structured version Visualization version GIF version |
Description: Lemma 2 for cpmidpmat 22003. (Contributed by AV, 14-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) |
Ref | Expression |
---|---|
cpmidgsum.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
cpmidgsum.b | ⊢ 𝐵 = (Base‘𝐴) |
cpmidgsum.p | ⊢ 𝑃 = (Poly1‘𝑅) |
cpmidgsum.y | ⊢ 𝑌 = (𝑁 Mat 𝑃) |
cpmidgsum.x | ⊢ 𝑋 = (var1‘𝑅) |
cpmidgsum.e | ⊢ ↑ = (.g‘(mulGrp‘𝑃)) |
cpmidgsum.m | ⊢ · = ( ·𝑠 ‘𝑌) |
cpmidgsum.1 | ⊢ 1 = (1r‘𝑌) |
cpmidgsum.u | ⊢ 𝑈 = (algSc‘𝑃) |
cpmidgsum.c | ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
cpmidgsum.k | ⊢ 𝐾 = (𝐶‘𝑀) |
cpmidgsum.h | ⊢ 𝐻 = (𝐾 · 1 ) |
cpmidgsumm2pm.o | ⊢ 𝑂 = (1r‘𝐴) |
cpmidgsumm2pm.m | ⊢ ∗ = ( ·𝑠 ‘𝐴) |
cpmidgsumm2pm.t | ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
cpmidpmat.g | ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑘) ∗ 𝑂)) |
Ref | Expression |
---|---|
cpmidpmatlem2 | ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ (𝐵 ↑m ℕ0)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1189 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈ Fin) | |
2 | crngring 19776 | . . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
3 | 2 | 3ad2ant2 1132 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
4 | 3 | adantr 480 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
5 | cpmidgsum.k | . . . . . 6 ⊢ 𝐾 = (𝐶‘𝑀) | |
6 | cpmidgsum.c | . . . . . . 7 ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) | |
7 | cpmidgsum.a | . . . . . . 7 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
8 | cpmidgsum.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝐴) | |
9 | cpmidgsum.p | . . . . . . 7 ⊢ 𝑃 = (Poly1‘𝑅) | |
10 | eqid 2739 | . . . . . . 7 ⊢ (Base‘𝑃) = (Base‘𝑃) | |
11 | 6, 7, 8, 9, 10 | chpmatply1 21962 | . . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) ∈ (Base‘𝑃)) |
12 | 5, 11 | eqeltrid 2844 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐾 ∈ (Base‘𝑃)) |
13 | eqid 2739 | . . . . . 6 ⊢ (coe1‘𝐾) = (coe1‘𝐾) | |
14 | eqid 2739 | . . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
15 | 13, 10, 9, 14 | coe1fvalcl 21364 | . . . . 5 ⊢ ((𝐾 ∈ (Base‘𝑃) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝐾)‘𝑘) ∈ (Base‘𝑅)) |
16 | 12, 15 | sylan 579 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝐾)‘𝑘) ∈ (Base‘𝑅)) |
17 | 2 | anim2i 616 | . . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
18 | 7 | matring 21573 | . . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
19 | cpmidgsumm2pm.o | . . . . . . . 8 ⊢ 𝑂 = (1r‘𝐴) | |
20 | 8, 19 | ringidcl 19788 | . . . . . . 7 ⊢ (𝐴 ∈ Ring → 𝑂 ∈ 𝐵) |
21 | 17, 18, 20 | 3syl 18 | . . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑂 ∈ 𝐵) |
22 | 21 | 3adant3 1130 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑂 ∈ 𝐵) |
23 | 22 | adantr 480 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑂 ∈ 𝐵) |
24 | cpmidgsumm2pm.m | . . . . 5 ⊢ ∗ = ( ·𝑠 ‘𝐴) | |
25 | 14, 7, 8, 24 | matvscl 21561 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (((coe1‘𝐾)‘𝑘) ∈ (Base‘𝑅) ∧ 𝑂 ∈ 𝐵)) → (((coe1‘𝐾)‘𝑘) ∗ 𝑂) ∈ 𝐵) |
26 | 1, 4, 16, 23, 25 | syl22anc 835 | . . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝐾)‘𝑘) ∗ 𝑂) ∈ 𝐵) |
27 | cpmidpmat.g | . . 3 ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑘) ∗ 𝑂)) | |
28 | 26, 27 | fmptd 6982 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐺:ℕ0⟶𝐵) |
29 | 8 | fvexi 6782 | . . . 4 ⊢ 𝐵 ∈ V |
30 | nn0ex 12222 | . . . 4 ⊢ ℕ0 ∈ V | |
31 | 29, 30 | pm3.2i 470 | . . 3 ⊢ (𝐵 ∈ V ∧ ℕ0 ∈ V) |
32 | elmapg 8602 | . . 3 ⊢ ((𝐵 ∈ V ∧ ℕ0 ∈ V) → (𝐺 ∈ (𝐵 ↑m ℕ0) ↔ 𝐺:ℕ0⟶𝐵)) | |
33 | 31, 32 | mp1i 13 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐺 ∈ (𝐵 ↑m ℕ0) ↔ 𝐺:ℕ0⟶𝐵)) |
34 | 28, 33 | mpbird 256 | 1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ (𝐵 ↑m ℕ0)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1541 ∈ wcel 2109 Vcvv 3430 ↦ cmpt 5161 ⟶wf 6426 ‘cfv 6430 (class class class)co 7268 ↑m cmap 8589 Fincfn 8707 ℕ0cn0 12216 Basecbs 16893 ·𝑠 cvsca 16947 .gcmg 18681 mulGrpcmgp 19701 1rcur 19718 Ringcrg 19764 CRingccrg 19765 algSccascl 21040 var1cv1 21328 Poly1cpl1 21329 coe1cco1 21330 Mat cmat 21535 matToPolyMat cmat2pmat 21834 CharPlyMat cchpmat 21956 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-rep 5213 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7579 ax-cnex 10911 ax-resscn 10912 ax-1cn 10913 ax-icn 10914 ax-addcl 10915 ax-addrcl 10916 ax-mulcl 10917 ax-mulrcl 10918 ax-mulcom 10919 ax-addass 10920 ax-mulass 10921 ax-distr 10922 ax-i2m1 10923 ax-1ne0 10924 ax-1rid 10925 ax-rnegex 10926 ax-rrecex 10927 ax-cnre 10928 ax-pre-lttri 10929 ax-pre-lttrn 10930 ax-pre-ltadd 10931 ax-pre-mulgt0 10932 ax-addf 10934 ax-mulf 10935 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-xor 1506 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3072 df-rmo 3073 df-rab 3074 df-v 3432 df-sbc 3720 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-ot 4575 df-uni 4845 df-int 4885 df-iun 4931 df-iin 4932 df-br 5079 df-opab 5141 df-mpt 5162 df-tr 5196 df-id 5488 df-eprel 5494 df-po 5502 df-so 5503 df-fr 5543 df-se 5544 df-we 5545 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-res 5600 df-ima 5601 df-pred 6199 df-ord 6266 df-on 6267 df-lim 6268 df-suc 6269 df-iota 6388 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435 df-fo 6436 df-f1o 6437 df-fv 6438 df-isom 6439 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-of 7524 df-ofr 7525 df-om 7701 df-1st 7817 df-2nd 7818 df-supp 7962 df-tpos 8026 df-frecs 8081 df-wrecs 8112 df-recs 8186 df-rdg 8225 df-1o 8281 df-2o 8282 df-er 8472 df-map 8591 df-pm 8592 df-ixp 8660 df-en 8708 df-dom 8709 df-sdom 8710 df-fin 8711 df-fsupp 9090 df-sup 9162 df-oi 9230 df-card 9681 df-pnf 10995 df-mnf 10996 df-xr 10997 df-ltxr 10998 df-le 10999 df-sub 11190 df-neg 11191 df-div 11616 df-nn 11957 df-2 12019 df-3 12020 df-4 12021 df-5 12022 df-6 12023 df-7 12024 df-8 12025 df-9 12026 df-n0 12217 df-xnn0 12289 df-z 12303 df-dec 12420 df-uz 12565 df-rp 12713 df-fz 13222 df-fzo 13365 df-seq 13703 df-exp 13764 df-hash 14026 df-word 14199 df-lsw 14247 df-concat 14255 df-s1 14282 df-substr 14335 df-pfx 14365 df-splice 14444 df-reverse 14453 df-s2 14542 df-struct 16829 df-sets 16846 df-slot 16864 df-ndx 16876 df-base 16894 df-ress 16923 df-plusg 16956 df-mulr 16957 df-starv 16958 df-sca 16959 df-vsca 16960 df-ip 16961 df-tset 16962 df-ple 16963 df-ds 16965 df-unif 16966 df-hom 16967 df-cco 16968 df-0g 17133 df-gsum 17134 df-prds 17139 df-pws 17141 df-mre 17276 df-mrc 17277 df-acs 17279 df-mgm 18307 df-sgrp 18356 df-mnd 18367 df-mhm 18411 df-submnd 18412 df-efmnd 18489 df-grp 18561 df-minusg 18562 df-sbg 18563 df-mulg 18682 df-subg 18733 df-ghm 18813 df-gim 18856 df-cntz 18904 df-oppg 18931 df-symg 18956 df-pmtr 19031 df-psgn 19080 df-cmn 19369 df-abl 19370 df-mgp 19702 df-ur 19719 df-ring 19766 df-cring 19767 df-oppr 19843 df-dvdsr 19864 df-unit 19865 df-invr 19895 df-dvr 19906 df-rnghom 19940 df-drng 19974 df-subrg 20003 df-lmod 20106 df-lss 20175 df-sra 20415 df-rgmod 20416 df-cnfld 20579 df-zring 20652 df-zrh 20686 df-dsmm 20920 df-frlm 20935 df-ascl 21043 df-psr 21093 df-mvr 21094 df-mpl 21095 df-opsr 21097 df-psr1 21332 df-vr1 21333 df-ply1 21334 df-coe1 21335 df-mamu 21514 df-mat 21536 df-mdet 21715 df-mat2pmat 21837 df-chpmat 21957 |
This theorem is referenced by: cpmidpmat 22003 |
Copyright terms: Public domain | W3C validator |