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

 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
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 maduf.a . . 3 Mat
2 eqid 2467 . . 3
41, 3matrcl 18783 . . . . 5
54adantl 466 . . . 4
65simpld 459 . . 3
7 simpl 457 . . 3
8 eqid 2467 . . . . . . 7 maDet maDet
98, 1, 3, 2mdetf 18966 . . . . . 6 maDet
1263ad2ant1 1017 . . . . 5
13 simp1l 1020 . . . . 5
14 simp11l 1107 . . . . . . 7
15 crngring 17081 . . . . . . 7
16 eqid 2467 . . . . . . . . 9
172, 16ringidcl 17091 . . . . . . . 8
18 eqid 2467 . . . . . . . . 9
192, 18ring0cl 17092 . . . . . . . 8
20 ifcl 3987 . . . . . . . 8
2117, 19, 20syl2anc 661 . . . . . . 7
2214, 15, 213syl 20 . . . . . 6
23 simp11r 1108 . . . . . . . 8
241, 2, 3matbas2i 18793 . . . . . . . 8
25 elmapi 7452 . . . . . . . 8
2623, 24, 253syl 20 . . . . . . 7
27 simp2 997 . . . . . . 7
28 simp3 998 . . . . . . 7
2926, 27, 28fovrnd 6442 . . . . . 6
30 ifcl 3987 . . . . . 6
3122, 29, 30syl2anc 661 . . . . 5
321, 2, 3, 12, 13, 31matbas2d 18794 . . . 4
3311, 32ffvelrnd 6033 . . 3 maDet
341, 2, 3, 6, 7, 33matbas2d 18794 . 2 maDet