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