Metamath Proof Explorer

Theorem madutpos

Description: The adjuct of a transposed matrix is the transposition of the adjunct of the matrix. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses maduf.a 
|- A = ( N Mat R )
maduf.j 
|- J = ( N maAdju R )
maduf.b 
|- B = ( Base ` A )
Assertion madutpos 
|- ( ( R e. CRing /\ M e. B ) -> ( J ` tpos M ) = tpos ( J ` M ) )

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 
 |-  ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) = ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) )
5 4 tposmpo 
 |-  tpos ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) = ( c e. N , d e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) )
6 orcom 
 |-  ( ( d = a \/ c = b ) <-> ( c = b \/ d = a ) )
7 6 a1i 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( ( d = a \/ c = b ) <-> ( c = b \/ d = a ) ) )
8 ancom 
 |-  ( ( c = b /\ d = a ) <-> ( d = a /\ c = b ) )
9 8 a1i 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( ( c = b /\ d = a ) <-> ( d = a /\ c = b ) ) )
10 9 ifbid 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( d = a /\ c = b ) , ( 1r ` R ) , ( 0g ` R ) ) )
11 ovtpos 
 |-  ( c tpos M d ) = ( d M c )
12 11 eqcomi 
 |-  ( d M c ) = ( c tpos M d )
13 12 a1i 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( d M c ) = ( c tpos M d ) )
14 7 10 13 ifbieq12d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) = if ( ( c = b \/ d = a ) , if ( ( d = a /\ c = b ) , ( 1r ` R ) , ( 0g ` R ) ) , ( c tpos M d ) ) )
15 14 mpoeq3dv 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( c e. N , d e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) = ( c e. N , d e. N |-> if ( ( c = b \/ d = a ) , if ( ( d = a /\ c = b ) , ( 1r ` R ) , ( 0g ` R ) ) , ( c tpos M d ) ) ) )
16 5 15 syl5eq 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> tpos ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) = ( c e. N , d e. N |-> if ( ( c = b \/ d = a ) , if ( ( d = a /\ c = b ) , ( 1r ` R ) , ( 0g ` R ) ) , ( c tpos M d ) ) ) )
17 16 fveq2d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( ( N maDet R ) ` tpos ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) ) = ( ( N maDet R ) ` ( c e. N , d e. N |-> if ( ( c = b \/ d = a ) , if ( ( d = a /\ c = b ) , ( 1r ` R ) , ( 0g ` R ) ) , ( c tpos M d ) ) ) ) )
18 simpll 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> R e. CRing )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 1 3 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
21 20 simpld 
 |-  ( M e. B -> N e. Fin )
22 21 ad2antlr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> N e. Fin )
23 simp1ll 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ d e. N /\ c e. N ) -> R e. CRing )
24 crngring 
 |-  ( R e. CRing -> R e. Ring )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 19 25 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
27 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
28 19 27 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
29 26 28 ifcld 
 |-  ( R e. Ring -> if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
30 23 24 29 3syl 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ d e. N /\ c e. N ) -> if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
31 1 19 3 matbas2i 
 |-  ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
32 elmapi 
 |-  ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
33 31 32 syl 
 |-  ( M e. B -> M : ( N X. N ) --> ( Base ` R ) )
34 33 ad2antlr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
35 34 fovrnda 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ ( d e. N /\ c e. N ) ) -> ( d M c ) e. ( Base ` R ) )
36 35 3impb 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ d e. N /\ c e. N ) -> ( d M c ) e. ( Base ` R ) )
37 30 36 ifcld 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ d e. N /\ c e. N ) -> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) e. ( Base ` R ) )
38 1 19 3 22 18 37 matbas2d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) e. B )
39 eqid 
 |-  ( N maDet R ) = ( N maDet R )
40 39 1 3 mdettpos 
 |-  ( ( R e. CRing /\ ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) e. B ) -> ( ( N maDet R ) ` tpos ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) ) = ( ( N maDet R ) ` ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) ) )
41 18 38 40 syl2anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( ( N maDet R ) ` tpos ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) ) = ( ( N maDet R ) ` ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) ) )
42 17 41 eqtr3d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( ( N maDet R ) ` ( c e. N , d e. N |-> if ( ( c = b \/ d = a ) , if ( ( d = a /\ c = b ) , ( 1r ` R ) , ( 0g ` R ) ) , ( c tpos M d ) ) ) ) = ( ( N maDet R ) ` ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) ) )
43 1 3 mattposcl 
 |-  ( M e. B -> tpos M e. B )
44 43 adantl 
 |-  ( ( R e. CRing /\ M e. B ) -> tpos M e. B )
45 44 adantr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> tpos M e. B )
46 simprl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
47 simprr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
48 1 39 2 3 25 27 maducoeval2 
 |-  ( ( ( R e. CRing /\ tpos M e. B ) /\ a e. N /\ b e. N ) -> ( a ( J ` tpos M ) b ) = ( ( N maDet R ) ` ( c e. N , d e. N |-> if ( ( c = b \/ d = a ) , if ( ( d = a /\ c = b ) , ( 1r ` R ) , ( 0g ` R ) ) , ( c tpos M d ) ) ) ) )
49 18 45 46 47 48 syl211anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a ( J ` tpos M ) b ) = ( ( N maDet R ) ` ( c e. N , d e. N |-> if ( ( c = b \/ d = a ) , if ( ( d = a /\ c = b ) , ( 1r ` R ) , ( 0g ` R ) ) , ( c tpos M d ) ) ) ) )
50 simplr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> M e. B )
51 1 39 2 3 25 27 maducoeval2 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ b e. N /\ a e. N ) -> ( b ( J ` M ) a ) = ( ( N maDet R ) ` ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) ) )
52 18 50 47 46 51 syl211anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( b ( J ` M ) a ) = ( ( N maDet R ) ` ( d e. N , c e. N |-> if ( ( d = a \/ c = b ) , if ( ( c = b /\ d = a ) , ( 1r ` R ) , ( 0g ` R ) ) , ( d M c ) ) ) ) )
53 42 49 52 3eqtr4d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a ( J ` tpos M ) b ) = ( b ( J ` M ) a ) )
54 ovtpos 
 |-  ( a tpos ( J ` M ) b ) = ( b ( J ` M ) a )
55 53 54 eqtr4di 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a ( J ` tpos M ) b ) = ( a tpos ( J ` M ) b ) )
56 55 ralrimivva 
 |-  ( ( R e. CRing /\ M e. B ) -> A. a e. N A. b e. N ( a ( J ` tpos M ) b ) = ( a tpos ( J ` M ) b ) )
57 1 2 3 maduf 
 |-  ( R e. CRing -> J : B --> B )
58 57 adantr 
 |-  ( ( R e. CRing /\ M e. B ) -> J : B --> B )
59 58 44 ffvelrnd 
 |-  ( ( R e. CRing /\ M e. B ) -> ( J ` tpos M ) e. B )
60 1 19 3 matbas2i 
 |-  ( ( J ` tpos M ) e. B -> ( J ` tpos M ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
61 59 60 syl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( J ` tpos M ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
62 elmapi 
 |-  ( ( J ` tpos M ) e. ( ( Base ` R ) ^m ( N X. N ) ) -> ( J ` tpos M ) : ( N X. N ) --> ( Base ` R ) )
63 ffn 
 |-  ( ( J ` tpos M ) : ( N X. N ) --> ( Base ` R ) -> ( J ` tpos M ) Fn ( N X. N ) )
64 61 62 63 3syl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( J ` tpos M ) Fn ( N X. N ) )
65 57 ffvelrnda 
 |-  ( ( R e. CRing /\ M e. B ) -> ( J ` M ) e. B )
66 1 3 mattposcl 
 |-  ( ( J ` M ) e. B -> tpos ( J ` M ) e. B )
67 1 19 3 matbas2i 
 |-  ( tpos ( J ` M ) e. B -> tpos ( J ` M ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
68 65 66 67 3syl 
 |-  ( ( R e. CRing /\ M e. B ) -> tpos ( J ` M ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
69 elmapi 
 |-  ( tpos ( J ` M ) e. ( ( Base ` R ) ^m ( N X. N ) ) -> tpos ( J ` M ) : ( N X. N ) --> ( Base ` R ) )
70 ffn 
 |-  ( tpos ( J ` M ) : ( N X. N ) --> ( Base ` R ) -> tpos ( J ` M ) Fn ( N X. N ) )
71 68 69 70 3syl 
 |-  ( ( R e. CRing /\ M e. B ) -> tpos ( J ` M ) Fn ( N X. N ) )
72 eqfnov2 
 |-  ( ( ( J ` tpos M ) Fn ( N X. N ) /\ tpos ( J ` M ) Fn ( N X. N ) ) -> ( ( J ` tpos M ) = tpos ( J ` M ) <-> A. a e. N A. b e. N ( a ( J ` tpos M ) b ) = ( a tpos ( J ` M ) b ) ) )
73 64 71 72 syl2anc 
 |-  ( ( R e. CRing /\ M e. B ) -> ( ( J ` tpos M ) = tpos ( J ` M ) <-> A. a e. N A. b e. N ( a ( J ` tpos M ) b ) = ( a tpos ( J ` M ) b ) ) )
74 56 73 mpbird 
 |-  ( ( R e. CRing /\ M e. B ) -> ( J ` tpos M ) = tpos ( J ` M ) )