m2cpminv - Metamath Proof Explorer

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

Theorem m2cpminv 22817

Description: The inverse matrix transformation is a 1-1 function from the constant polynomial matrices onto the matrices over the base ring of the polynomials. (Contributed by AV, 27-Nov-2019.) (Revised by AV, 15-Dec-2019.)

**Hypotheses**
Ref	Expression
m2cpminv.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
m2cpminv.k	⊢ 𝐾 = (Base‘𝐴)
m2cpminv.s	⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)
m2cpminv.i	⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅)
m2cpminv.t	⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)

**Assertion**
Ref	Expression
m2cpminv	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼:𝑆–1-1-onto→𝐾 ∧ ^◡𝐼 = 𝑇))

Proof of Theorem m2cpminv Dummy variables 𝑘 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		m2cpminv.a	. . . 4 ⊢ 𝐴 = (𝑁 Mat 𝑅)
2		m2cpminv.k	. . . 4 ⊢ 𝐾 = (Base‘𝐴)
3		m2cpminv.s	. . . 4 ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)
4		m2cpminv.i	. . . 4 ⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅)
5	1, 2, 3, 4	cpm2mf 22809	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐼:𝑆⟶𝐾)
6		m2cpminv.t	. . . 4 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
7	3, 6, 1, 2	m2cpmf 22799	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐾⟶𝑆)
8	3, 4, 6	m2cpminvid2 22812	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ 𝑆) → (𝑇‘(𝐼‘𝑠)) = 𝑠)
9	8	3expa 1131	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑠 ∈ 𝑆) → (𝑇‘(𝐼‘𝑠)) = 𝑠)
10	9	ralrimiva 3154	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑠 ∈ 𝑆 (𝑇‘(𝐼‘𝑠)) = 𝑠)
11	4, 1, 2, 6	m2cpminvid 22810	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐾) → (𝐼‘(𝑇‘𝑘)) = 𝑘)
12	11	3expa 1131	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ 𝐾) → (𝐼‘(𝑇‘𝑘)) = 𝑘)
13	12	ralrimiva 3154	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑘 ∈ 𝐾 (𝐼‘(𝑇‘𝑘)) = 𝑘)
14	5, 7, 10, 13	2fvidf1od 7282	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐼:𝑆–1-1-onto→𝐾)
15	5, 7, 10, 13	2fvidinvd 7283	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ^◡𝐼 = 𝑇)
16	14, 15	jca 519	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼:𝑆–1-1-onto→𝐾 ∧ ^◡𝐼 = 𝑇))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1560 ∈ wcel 2142 ^◡ccnv 5646 –1-1-onto→wf1o 6520 ‘cfv 6521 (class class class)co 7396 Fincfn 8927 Basecbs 17245 Ringcrg 20279 Mat cmat 22464 ConstPolyMat ccpmat 22760 matToPolyMat cmat2pmat 22761 cPolyMatToMat ccpmat2mat 22762

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-ot 4591 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-ofr 7661 df-om 7847 df-1st 7970 df-2nd 7971 df-supp 8141 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8678 df-map 8810 df-pm 8811 df-ixp 8880 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fsupp 9308 df-sup 9388 df-oi 9458 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-dec 12689 df-uz 12840 df-fz 13513 df-fzo 13660 df-seq 14015 df-hash 14344 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-sca 17302 df-vsca 17303 df-ip 17304 df-tset 17305 df-ple 17306 df-ds 17308 df-hom 17310 df-cco 17311 df-0g 17470 df-gsum 17471 df-prds 17476 df-pws 17478 df-mre 17614 df-mrc 17615 df-acs 17617 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-mhm 18817 df-submnd 18818 df-grp 18978 df-minusg 18979 df-sbg 18980 df-mulg 19110 df-subg 19165 df-ghm 19254 df-cntz 19357 df-cmn 19822 df-abl 19823 df-mgp 20187 df-rng 20199 df-ur 20228 df-srg 20233 df-ring 20281 df-subrng 20592 df-subrg 20616 df-lmod 20926 df-lss 20996 df-sra 21237 df-rgmod 21238 df-dsmm 21781 df-frlm 21796 df-ascl 21904 df-psr 21958 df-mvr 21959 df-mpl 21960 df-opsr 21962 df-psr1 22239 df-vr1 22240 df-ply1 22241 df-coe1 22242 df-mat 22465 df-cpmat 22763 df-mat2pmat 22764 df-cpmat2mat 22765

This theorem is referenced by: (None)

W3C validator