Metamath Proof Explorer

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)

Ref Expression
`|- A = ( N Mat R )`
`|- J = ( N maAdju R )`
`|- B = ( Base ` A )`
`|- ( R e. CRing -> J : B --> B )`

Proof

Step Hyp Ref Expression
` |-  A = ( N Mat R )`
` |-  J = ( N maAdju R )`
` |-  B = ( Base ` A )`
4 eqid
` |-  ( Base ` R ) = ( Base ` R )`
5 1 3 matrcl
` |-  ( m e. B -> ( N e. Fin /\ R e. _V ) )`
` |-  ( ( R e. CRing /\ m e. B ) -> ( N e. Fin /\ R e. _V ) )`
7 6 simpld
` |-  ( ( R e. CRing /\ m e. B ) -> N e. Fin )`
8 simpl
` |-  ( ( R e. CRing /\ m e. B ) -> R e. CRing )`
9 eqid
` |-  ( N maDet R ) = ( N maDet R )`
10 9 1 3 4 mdetf
` |-  ( R e. CRing -> ( N maDet R ) : B --> ( Base ` R ) )`
` |-  ( ( R e. CRing /\ m e. B ) -> ( N maDet R ) : B --> ( Base ` R ) )`
` |-  ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) -> ( N maDet R ) : B --> ( Base ` R ) )`
` |-  ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) -> N e. Fin )`
14 simp1l
` |-  ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) -> R e. CRing )`
15 simp11l
` |-  ( ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) /\ k e. N /\ l e. N ) -> R e. CRing )`
16 crngring
` |-  ( R e. CRing -> R e. Ring )`
17 eqid
` |-  ( 1r ` R ) = ( 1r ` R )`
18 4 17 ringidcl
` |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )`
19 eqid
` |-  ( 0g ` R ) = ( 0g ` R )`
20 4 19 ring0cl
` |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )`
21 18 20 ifcld
` |-  ( R e. Ring -> if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )`
22 15 16 21 3syl
` |-  ( ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) /\ k e. N /\ l e. N ) -> if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )`
23 simp2
` |-  ( ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) /\ k e. N /\ l e. N ) -> k e. N )`
24 simp3
` |-  ( ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) /\ k e. N /\ l e. N ) -> l e. N )`
25 simp11r
` |-  ( ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) /\ k e. N /\ l e. N ) -> m e. B )`
26 1 4 3 23 24 25 matecld
` |-  ( ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) /\ k e. N /\ l e. N ) -> ( k m l ) e. ( Base ` R ) )`
27 22 26 ifcld
` |-  ( ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) /\ k e. N /\ l e. N ) -> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) e. ( Base ` R ) )`
28 1 4 3 13 14 27 matbas2d
` |-  ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) -> ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) e. B )`
29 12 28 ffvelrnd
` |-  ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) -> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) e. ( Base ` R ) )`
30 1 4 3 7 8 29 matbas2d
` |-  ( ( R e. CRing /\ m e. B ) -> ( i e. N , j e. N |-> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) ) e. B )`
31 1 9 2 3 17 19 madufval
` |-  J = ( m e. B |-> ( i e. N , j e. N |-> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) ) )`
32 30 31 fmptd
` |-  ( R e. CRing -> J : B --> B )`