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 eqtrid ⊢ 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 eqtr4di ⊢ 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