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

Theorem maduf 21562
Description: Creating the adjunct of matrices is a function from the set of matrices into the set of matrices. (Contributed by Stefan O'Rear, 11-Jul-2018.)
Hypotheses
Ref Expression
maduf.a 𝐴 = (𝑁 Mat 𝑅)
maduf.j 𝐽 = (𝑁 maAdju 𝑅)
maduf.b 𝐵 = (Base‘𝐴)
Assertion
Ref Expression
maduf (𝑅 ∈ CRing → 𝐽:𝐵𝐵)

Proof of Theorem maduf
Dummy variables 𝑖 𝑗 𝑘 𝑙 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 maduf.a . . 3 𝐴 = (𝑁 Mat 𝑅)
2 eqid 2738 . . 3 (Base‘𝑅) = (Base‘𝑅)
3 maduf.b . . 3 𝐵 = (Base‘𝐴)
41, 3matrcl 21333 . . . . 5 (𝑚𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
54adantl 485 . . . 4 ((𝑅 ∈ CRing ∧ 𝑚𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
65simpld 498 . . 3 ((𝑅 ∈ CRing ∧ 𝑚𝐵) → 𝑁 ∈ Fin)
7 simpl 486 . . 3 ((𝑅 ∈ CRing ∧ 𝑚𝐵) → 𝑅 ∈ CRing)
8 eqid 2738 . . . . . . 7 (𝑁 maDet 𝑅) = (𝑁 maDet 𝑅)
98, 1, 3, 2mdetf 21516 . . . . . 6 (𝑅 ∈ CRing → (𝑁 maDet 𝑅):𝐵⟶(Base‘𝑅))
109adantr 484 . . . . 5 ((𝑅 ∈ CRing ∧ 𝑚𝐵) → (𝑁 maDet 𝑅):𝐵⟶(Base‘𝑅))
11103ad2ant1 1135 . . . 4 (((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) → (𝑁 maDet 𝑅):𝐵⟶(Base‘𝑅))
1263ad2ant1 1135 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) → 𝑁 ∈ Fin)
13 simp1l 1199 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) → 𝑅 ∈ CRing)
14 simp11l 1286 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) ∧ 𝑘𝑁𝑙𝑁) → 𝑅 ∈ CRing)
15 crngring 19598 . . . . . . 7 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
16 eqid 2738 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
172, 16ringidcl 19610 . . . . . . . 8 (𝑅 ∈ Ring → (1r𝑅) ∈ (Base‘𝑅))
18 eqid 2738 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
192, 18ring0cl 19611 . . . . . . . 8 (𝑅 ∈ Ring → (0g𝑅) ∈ (Base‘𝑅))
2017, 19ifcld 4499 . . . . . . 7 (𝑅 ∈ Ring → if(𝑙 = 𝑖, (1r𝑅), (0g𝑅)) ∈ (Base‘𝑅))
2114, 15, 203syl 18 . . . . . 6 ((((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) ∧ 𝑘𝑁𝑙𝑁) → if(𝑙 = 𝑖, (1r𝑅), (0g𝑅)) ∈ (Base‘𝑅))
22 simp2 1139 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) ∧ 𝑘𝑁𝑙𝑁) → 𝑘𝑁)
23 simp3 1140 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) ∧ 𝑘𝑁𝑙𝑁) → 𝑙𝑁)
24 simp11r 1287 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) ∧ 𝑘𝑁𝑙𝑁) → 𝑚𝐵)
251, 2, 3, 22, 23, 24matecld 21347 . . . . . 6 ((((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) ∧ 𝑘𝑁𝑙𝑁) → (𝑘𝑚𝑙) ∈ (Base‘𝑅))
2621, 25ifcld 4499 . . . . 5 ((((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) ∧ 𝑘𝑁𝑙𝑁) → if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑅), (0g𝑅)), (𝑘𝑚𝑙)) ∈ (Base‘𝑅))
271, 2, 3, 12, 13, 26matbas2d 21344 . . . 4 (((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) → (𝑘𝑁, 𝑙𝑁 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑅), (0g𝑅)), (𝑘𝑚𝑙))) ∈ 𝐵)
2811, 27ffvelrnd 6923 . . 3 (((𝑅 ∈ CRing ∧ 𝑚𝐵) ∧ 𝑖𝑁𝑗𝑁) → ((𝑁 maDet 𝑅)‘(𝑘𝑁, 𝑙𝑁 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑅), (0g𝑅)), (𝑘𝑚𝑙)))) ∈ (Base‘𝑅))
291, 2, 3, 6, 7, 28matbas2d 21344 . 2 ((𝑅 ∈ CRing ∧ 𝑚𝐵) → (𝑖𝑁, 𝑗𝑁 ↦ ((𝑁 maDet 𝑅)‘(𝑘𝑁, 𝑙𝑁 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑅), (0g𝑅)), (𝑘𝑚𝑙))))) ∈ 𝐵)
30 maduf.j . . 3 𝐽 = (𝑁 maAdju 𝑅)
311, 8, 30, 3, 16, 18madufval 21558 . 2 𝐽 = (𝑚𝐵 ↦ (𝑖𝑁, 𝑗𝑁 ↦ ((𝑁 maDet 𝑅)‘(𝑘𝑁, 𝑙𝑁 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑅), (0g𝑅)), (𝑘𝑚𝑙))))))
3229, 31fmptd 6949 1 (𝑅 ∈ CRing → 𝐽:𝐵𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2111  Vcvv 3420  ifcif 4453  wf 6393  cfv 6397  (class class class)co 7231  cmpo 7233  Fincfn 8646  Basecbs 16784  0gc0g 16968  1rcur 19540  Ringcrg 19586  CRingccrg 19587   Mat cmat 21328   maDet cmdat 21505   maAdju cmadu 21553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830  ax-addf 10832  ax-mulf 10833
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-xor 1508  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-ot 4564  df-uni 4834  df-int 4874  df-iun 4920  df-iin 4921  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-se 5524  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-isom 6406  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-om 7663  df-1st 7779  df-2nd 7780  df-supp 7924  df-tpos 7988  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-1o 8222  df-2o 8223  df-er 8411  df-map 8530  df-pm 8531  df-ixp 8599  df-en 8647  df-dom 8648  df-sdom 8649  df-fin 8650  df-fsupp 9010  df-sup 9082  df-oi 9150  df-card 9579  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-div 11514  df-nn 11855  df-2 11917  df-3 11918  df-4 11919  df-5 11920  df-6 11921  df-7 11922  df-8 11923  df-9 11924  df-n0 12115  df-xnn0 12187  df-z 12201  df-dec 12318  df-uz 12463  df-rp 12611  df-fz 13120  df-fzo 13263  df-seq 13599  df-exp 13660  df-hash 13921  df-word 14094  df-lsw 14142  df-concat 14150  df-s1 14177  df-substr 14230  df-pfx 14260  df-splice 14339  df-reverse 14348  df-s2 14437  df-struct 16724  df-sets 16741  df-slot 16759  df-ndx 16769  df-base 16785  df-ress 16809  df-plusg 16839  df-mulr 16840  df-starv 16841  df-sca 16842  df-vsca 16843  df-ip 16844  df-tset 16845  df-ple 16846  df-ds 16848  df-unif 16849  df-hom 16850  df-cco 16851  df-0g 16970  df-gsum 16971  df-prds 16976  df-pws 16978  df-mre 17113  df-mrc 17114  df-acs 17116  df-mgm 18138  df-sgrp 18187  df-mnd 18198  df-mhm 18242  df-submnd 18243  df-efmnd 18320  df-grp 18392  df-minusg 18393  df-mulg 18513  df-subg 18564  df-ghm 18644  df-gim 18687  df-cntz 18735  df-oppg 18762  df-symg 18784  df-pmtr 18858  df-psgn 18907  df-cmn 19196  df-abl 19197  df-mgp 19529  df-ur 19541  df-ring 19588  df-cring 19589  df-oppr 19665  df-dvdsr 19683  df-unit 19684  df-invr 19714  df-dvr 19725  df-rnghom 19759  df-drng 19793  df-subrg 19822  df-sra 20233  df-rgmod 20234  df-cnfld 20388  df-zring 20460  df-zrh 20494  df-dsmm 20718  df-frlm 20733  df-mat 21329  df-mdet 21506  df-madu 21555
This theorem is referenced by:  madutpos  21563  madugsum  21564  madurid  21565  madulid  21566  matinv  21598  cpmadugsumfi  21798
  Copyright terms: Public domain W3C validator