# Metamath Proof Explorer

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}\mathrm{Mat}{R}$
maduf.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
maduf.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion madutpos ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}\left(tpos{M}\right)=tpos{J}\left({M}\right)$

### Proof

Step Hyp Ref Expression
1 maduf.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 maduf.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
3 maduf.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 eqid ${⊢}\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)=\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)$
5 4 tposmpo ${⊢}tpos\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)=\left({c}\in {N},{d}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)$
6 orcom ${⊢}\left({d}={a}\vee {c}={b}\right)↔\left({c}={b}\vee {d}={a}\right)$
7 6 a1i ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to \left(\left({d}={a}\vee {c}={b}\right)↔\left({c}={b}\vee {d}={a}\right)\right)$
8 ancom ${⊢}\left({c}={b}\wedge {d}={a}\right)↔\left({d}={a}\wedge {c}={b}\right)$
9 8 a1i ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to \left(\left({c}={b}\wedge {d}={a}\right)↔\left({d}={a}\wedge {c}={b}\right)\right)$
10 9 ifbid ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right)=if\left(\left({d}={a}\wedge {c}={b}\right),{1}_{{R}},{0}_{{R}}\right)$
11 ovtpos ${⊢}{c}tpos{M}{d}={d}{M}{c}$
12 11 eqcomi ${⊢}{d}{M}{c}={c}tpos{M}{d}$
13 12 a1i ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {d}{M}{c}={c}tpos{M}{d}$
14 7 10 13 ifbieq12d ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)=if\left(\left({c}={b}\vee {d}={a}\right),if\left(\left({d}={a}\wedge {c}={b}\right),{1}_{{R}},{0}_{{R}}\right),{c}tpos{M}{d}\right)$
15 14 mpoeq3dv ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to \left({c}\in {N},{d}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)=\left({c}\in {N},{d}\in {N}⟼if\left(\left({c}={b}\vee {d}={a}\right),if\left(\left({d}={a}\wedge {c}={b}\right),{1}_{{R}},{0}_{{R}}\right),{c}tpos{M}{d}\right)\right)$
16 5 15 syl5eq ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to tpos\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)=\left({c}\in {N},{d}\in {N}⟼if\left(\left({c}={b}\vee {d}={a}\right),if\left(\left({d}={a}\wedge {c}={b}\right),{1}_{{R}},{0}_{{R}}\right),{c}tpos{M}{d}\right)\right)$
17 16 fveq2d ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to \left({N}\mathrm{maDet}{R}\right)\left(tpos\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\right)=\left({N}\mathrm{maDet}{R}\right)\left(\left({c}\in {N},{d}\in {N}⟼if\left(\left({c}={b}\vee {d}={a}\right),if\left(\left({d}={a}\wedge {c}={b}\right),{1}_{{R}},{0}_{{R}}\right),{c}tpos{M}{d}\right)\right)\right)$
18 simpll ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {R}\in \mathrm{CRing}$
19 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
20 1 3 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
21 20 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
22 21 ad2antlr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {N}\in \mathrm{Fin}$
23 simp1ll ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\wedge {d}\in {N}\wedge {c}\in {N}\right)\to {R}\in \mathrm{CRing}$
24 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
25 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
26 19 25 ringidcl ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {\mathrm{Base}}_{{R}}$
27 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
28 19 27 ring0cl ${⊢}{R}\in \mathrm{Ring}\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
29 26 28 ifcld ${⊢}{R}\in \mathrm{Ring}\to if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
30 23 24 29 3syl ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\wedge {d}\in {N}\wedge {c}\in {N}\right)\to if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
31 1 19 3 matbas2i ${⊢}{M}\in {B}\to {M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
32 elmapi ${⊢}{M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
33 31 32 syl ${⊢}{M}\in {B}\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
34 33 ad2antlr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
35 34 fovrnda ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\wedge \left({d}\in {N}\wedge {c}\in {N}\right)\right)\to {d}{M}{c}\in {\mathrm{Base}}_{{R}}$
36 35 3impb ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\wedge {d}\in {N}\wedge {c}\in {N}\right)\to {d}{M}{c}\in {\mathrm{Base}}_{{R}}$
37 30 36 ifcld ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\wedge {d}\in {N}\wedge {c}\in {N}\right)\to if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\in {\mathrm{Base}}_{{R}}$
38 1 19 3 22 18 37 matbas2d ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to \left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\in {B}$
39 eqid ${⊢}{N}\mathrm{maDet}{R}={N}\mathrm{maDet}{R}$
40 39 1 3 mdettpos ${⊢}\left({R}\in \mathrm{CRing}\wedge \left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\in {B}\right)\to \left({N}\mathrm{maDet}{R}\right)\left(tpos\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\right)=\left({N}\mathrm{maDet}{R}\right)\left(\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\right)$
41 18 38 40 syl2anc ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to \left({N}\mathrm{maDet}{R}\right)\left(tpos\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\right)=\left({N}\mathrm{maDet}{R}\right)\left(\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\right)$
42 17 41 eqtr3d ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to \left({N}\mathrm{maDet}{R}\right)\left(\left({c}\in {N},{d}\in {N}⟼if\left(\left({c}={b}\vee {d}={a}\right),if\left(\left({d}={a}\wedge {c}={b}\right),{1}_{{R}},{0}_{{R}}\right),{c}tpos{M}{d}\right)\right)\right)=\left({N}\mathrm{maDet}{R}\right)\left(\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\right)$
43 1 3 mattposcl ${⊢}{M}\in {B}\to tpos{M}\in {B}$
44 43 adantl ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to tpos{M}\in {B}$
45 44 adantr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to tpos{M}\in {B}$
46 simprl ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}\in {N}$
47 simprr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {b}\in {N}$
48 1 39 2 3 25 27 maducoeval2 ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge tpos{M}\in {B}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {a}{J}\left(tpos{M}\right){b}=\left({N}\mathrm{maDet}{R}\right)\left(\left({c}\in {N},{d}\in {N}⟼if\left(\left({c}={b}\vee {d}={a}\right),if\left(\left({d}={a}\wedge {c}={b}\right),{1}_{{R}},{0}_{{R}}\right),{c}tpos{M}{d}\right)\right)\right)$
49 18 45 46 47 48 syl211anc ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}{J}\left(tpos{M}\right){b}=\left({N}\mathrm{maDet}{R}\right)\left(\left({c}\in {N},{d}\in {N}⟼if\left(\left({c}={b}\vee {d}={a}\right),if\left(\left({d}={a}\wedge {c}={b}\right),{1}_{{R}},{0}_{{R}}\right),{c}tpos{M}{d}\right)\right)\right)$
50 simplr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {M}\in {B}$
51 1 39 2 3 25 27 maducoeval2 ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {b}\in {N}\wedge {a}\in {N}\right)\to {b}{J}\left({M}\right){a}=\left({N}\mathrm{maDet}{R}\right)\left(\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\right)$
52 18 50 47 46 51 syl211anc ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {b}{J}\left({M}\right){a}=\left({N}\mathrm{maDet}{R}\right)\left(\left({d}\in {N},{c}\in {N}⟼if\left(\left({d}={a}\vee {c}={b}\right),if\left(\left({c}={b}\wedge {d}={a}\right),{1}_{{R}},{0}_{{R}}\right),{d}{M}{c}\right)\right)\right)$
53 42 49 52 3eqtr4d ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}{J}\left(tpos{M}\right){b}={b}{J}\left({M}\right){a}$
54 ovtpos ${⊢}{a}tpos{J}\left({M}\right){b}={b}{J}\left({M}\right){a}$
55 53 54 syl6eqr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}{J}\left(tpos{M}\right){b}={a}tpos{J}\left({M}\right){b}$
56 55 ralrimivva ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{a}{J}\left(tpos{M}\right){b}={a}tpos{J}\left({M}\right){b}$
57 1 2 3 maduf ${⊢}{R}\in \mathrm{CRing}\to {J}:{B}⟶{B}$
58 57 adantr ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}:{B}⟶{B}$
59 58 44 ffvelrnd ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}\left(tpos{M}\right)\in {B}$
60 1 19 3 matbas2i ${⊢}{J}\left(tpos{M}\right)\in {B}\to {J}\left(tpos{M}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
61 59 60 syl ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}\left(tpos{M}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
62 elmapi ${⊢}{J}\left(tpos{M}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {J}\left(tpos{M}\right):{N}×{N}⟶{\mathrm{Base}}_{{R}}$
63 ffn ${⊢}{J}\left(tpos{M}\right):{N}×{N}⟶{\mathrm{Base}}_{{R}}\to {J}\left(tpos{M}\right)Fn\left({N}×{N}\right)$
64 61 62 63 3syl ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}\left(tpos{M}\right)Fn\left({N}×{N}\right)$
65 57 ffvelrnda ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}\left({M}\right)\in {B}$
66 1 3 mattposcl ${⊢}{J}\left({M}\right)\in {B}\to tpos{J}\left({M}\right)\in {B}$
67 1 19 3 matbas2i ${⊢}tpos{J}\left({M}\right)\in {B}\to tpos{J}\left({M}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
68 65 66 67 3syl ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to tpos{J}\left({M}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
69 elmapi ${⊢}tpos{J}\left({M}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to tpos{J}\left({M}\right):{N}×{N}⟶{\mathrm{Base}}_{{R}}$
70 ffn ${⊢}tpos{J}\left({M}\right):{N}×{N}⟶{\mathrm{Base}}_{{R}}\to tpos{J}\left({M}\right)Fn\left({N}×{N}\right)$
71 68 69 70 3syl ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to tpos{J}\left({M}\right)Fn\left({N}×{N}\right)$
72 eqfnov2 ${⊢}\left({J}\left(tpos{M}\right)Fn\left({N}×{N}\right)\wedge tpos{J}\left({M}\right)Fn\left({N}×{N}\right)\right)\to \left({J}\left(tpos{M}\right)=tpos{J}\left({M}\right)↔\forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{a}{J}\left(tpos{M}\right){b}={a}tpos{J}\left({M}\right){b}\right)$
73 64 71 72 syl2anc ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to \left({J}\left(tpos{M}\right)=tpos{J}\left({M}\right)↔\forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{a}{J}\left(tpos{M}\right){b}={a}tpos{J}\left({M}\right){b}\right)$
74 56 73 mpbird ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}\left(tpos{M}\right)=tpos{J}\left({M}\right)$