Metamath Proof Explorer

Theorem maduf

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
Hypotheses maduf.a 
|- A = ( N Mat R )
maduf.j 
|- J = ( N maAdju R )
maduf.b 
|- B = ( Base ` A )
Assertion maduf 
|- ( R e. CRing -> J : B --> B )

Proof

Step Hyp Ref Expression
1 maduf.a 
 |-  A = ( N Mat R )
2 maduf.j 
 |-  J = ( N maAdju R )
3 maduf.b 
 |-  B = ( Base ` A )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 1 3 matrcl 
 |-  ( m e. B -> ( N e. Fin /\ R e. _V ) )
6 5 adantl 
 |-  ( ( 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 ) )
11 10 adantr 
 |-  ( ( R e. CRing /\ m e. B ) -> ( N maDet R ) : B --> ( Base ` R ) )
12 11 3ad2ant1 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ i e. N /\ j e. N ) -> ( N maDet R ) : B --> ( Base ` R ) )
13 7 3ad2ant1 
 |-  ( ( ( 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 )