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 22779

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 22771	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐼:𝑆⟶𝐾)
6		m2cpminv.t	. . . 4 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
7	3, 6, 1, 2	m2cpmf 22761	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐾⟶𝑆)
8	3, 4, 6	m2cpminvid2 22774	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ 𝑆) → (𝑇‘(𝐼‘𝑠)) = 𝑠)
9	8	3expa 1118	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑠 ∈ 𝑆) → (𝑇‘(𝐼‘𝑠)) = 𝑠)
10	9	ralrimiva 3152	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑠 ∈ 𝑆 (𝑇‘(𝐼‘𝑠)) = 𝑠)
11	4, 1, 2, 6	m2cpminvid 22772	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐾) → (𝐼‘(𝑇‘𝑘)) = 𝑘)
12	11	3expa 1118	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ 𝐾) → (𝐼‘(𝑇‘𝑘)) = 𝑘)
13	12	ralrimiva 3152	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑘 ∈ 𝐾 (𝐼‘(𝑇‘𝑘)) = 𝑘)
14	5, 7, 10, 13	2fvidf1od 7329	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐼:𝑆–1-1-onto→𝐾)
15	5, 7, 10, 13	2fvidinvd 7330	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ^◡𝐼 = 𝑇)
16	14, 15	jca 511	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼:𝑆–1-1-onto→𝐾 ∧ ^◡𝐼 = 𝑇))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2108 ^◡ccnv 5694 –1-1-onto→wf1o 6567 ‘cfv 6568 (class class class)co 7443 Fincfn 8997 Basecbs 17252 Ringcrg 20254 Mat cmat 22424 ConstPolyMat ccpmat 22722 matToPolyMat cmat2pmat 22723 cPolyMatToMat ccpmat2mat 22724

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7764 ax-cnex 11234 ax-resscn 11235 ax-1cn 11236 ax-icn 11237 ax-addcl 11238 ax-addrcl 11239 ax-mulcl 11240 ax-mulrcl 11241 ax-mulcom 11242 ax-addass 11243 ax-mulass 11244 ax-distr 11245 ax-i2m1 11246 ax-1ne0 11247 ax-1rid 11248 ax-rnegex 11249 ax-rrecex 11250 ax-cnre 11251 ax-pre-lttri 11252 ax-pre-lttrn 11253 ax-pre-ltadd 11254 ax-pre-mulgt0 11255

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-ot 4657 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5650 df-se 5651 df-we 5652 df-xp 5701 df-rel 5702 df-cnv 5703 df-co 5704 df-dm 5705 df-rn 5706 df-res 5707 df-ima 5708 df-pred 6327 df-ord 6393 df-on 6394 df-lim 6395 df-suc 6396 df-iota 6520 df-fun 6570 df-fn 6571 df-f 6572 df-f1 6573 df-fo 6574 df-f1o 6575 df-fv 6576 df-isom 6577 df-riota 7399 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7708 df-ofr 7709 df-om 7898 df-1st 8024 df-2nd 8025 df-supp 8196 df-frecs 8316 df-wrecs 8347 df-recs 8421 df-rdg 8460 df-1o 8516 df-2o 8517 df-er 8757 df-map 8880 df-pm 8881 df-ixp 8950 df-en 8998 df-dom 8999 df-sdom 9000 df-fin 9001 df-fsupp 9426 df-sup 9505 df-oi 9573 df-card 10002 df-pnf 11320 df-mnf 11321 df-xr 11322 df-ltxr 11323 df-le 11324 df-sub 11516 df-neg 11517 df-nn 12288 df-2 12350 df-3 12351 df-4 12352 df-5 12353 df-6 12354 df-7 12355 df-8 12356 df-9 12357 df-n0 12548 df-z 12634 df-dec 12753 df-uz 12898 df-fz 13562 df-fzo 13706 df-seq 14047 df-hash 14374 df-struct 17188 df-sets 17205 df-slot 17223 df-ndx 17235 df-base 17253 df-ress 17282 df-plusg 17318 df-mulr 17319 df-sca 17321 df-vsca 17322 df-ip 17323 df-tset 17324 df-ple 17325 df-ds 17327 df-hom 17329 df-cco 17330 df-0g 17495 df-gsum 17496 df-prds 17501 df-pws 17503 df-mre 17638 df-mrc 17639 df-acs 17641 df-mgm 18672 df-sgrp 18751 df-mnd 18767 df-mhm 18812 df-submnd 18813 df-grp 18970 df-minusg 18971 df-sbg 18972 df-mulg 19102 df-subg 19157 df-ghm 19247 df-cntz 19351 df-cmn 19818 df-abl 19819 df-mgp 20156 df-rng 20174 df-ur 20203 df-srg 20208 df-ring 20256 df-subrng 20566 df-subrg 20591 df-lmod 20876 df-lss 20947 df-sra 21189 df-rgmod 21190 df-dsmm 21769 df-frlm 21784 df-ascl 21892 df-psr 21945 df-mvr 21946 df-mpl 21947 df-opsr 21949 df-psr1 22194 df-vr1 22195 df-ply1 22196 df-coe1 22197 df-mat 22425 df-cpmat 22725 df-mat2pmat 22726 df-cpmat2mat 22727

This theorem is referenced by: (None)

W3C validator