Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  madutpos Structured version   Unicode version

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

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2420 . . . . . . . . 9
21tposmpt2 7009 . . . . . . . 8 tpos
3 orcom 388 . . . . . . . . . . 11
43a1i 11 . . . . . . . . . 10
5 ancom 451 . . . . . . . . . . . 12
65a1i 11 . . . . . . . . . . 11
76ifbid 3928 . . . . . . . . . 10
8 ovtpos 6987 . . . . . . . . . . . 12 tpos
98eqcomi 2433 . . . . . . . . . . 11 tpos
109a1i 11 . . . . . . . . . 10 tpos
114, 7, 10ifbieq12d 3933 . . . . . . . . 9 tpos
1211mpt2eq3dv 6362 . . . . . . . 8 tpos
132, 12syl5eq 2473 . . . . . . 7 tpos tpos
1413fveq2d 5876 . . . . . 6 maDet tpos maDet tpos
15 simpll 758 . . . . . . 7
16 maduf.a . . . . . . . 8 Mat
17 eqid 2420 . . . . . . . 8
18 maduf.b . . . . . . . 8
1916, 18matrcl 19361 . . . . . . . . . 10
2019simpld 460 . . . . . . . . 9
2120ad2antlr 731 . . . . . . . 8
22 simp1ll 1068 . . . . . . . . . 10
23 crngring 17719 . . . . . . . . . 10
24 eqid 2420 . . . . . . . . . . . 12
2517, 24ringidcl 17729 . . . . . . . . . . 11
26 eqid 2420 . . . . . . . . . . . 12
2717, 26ring0cl 17730 . . . . . . . . . . 11
2825, 27ifcld 3949 . . . . . . . . . 10
2922, 23, 283syl 18 . . . . . . . . 9
3016, 17, 18matbas2i 19371 . . . . . . . . . . . . 13
31 elmapi 7492 . . . . . . . . . . . . 13
3230, 31syl 17 . . . . . . . . . . . 12
3332ad2antlr 731 . . . . . . . . . . 11
3433fovrnda 6445 . . . . . . . . . 10
35343impb 1201 . . . . . . . . 9
3629, 35ifcld 3949 . . . . . . . 8
3716, 17, 18, 21, 15, 36matbas2d 19372 . . . . . . 7
38 eqid 2420 . . . . . . . 8 maDet maDet
3938, 16, 18mdettpos 19560 . . . . . . 7 maDet tpos maDet
4015, 37, 39syl2anc 665 . . . . . 6 maDet tpos maDet
4216, 18mattposcl 19402 . . . . . . . 8 tpos
4342adantl 467 . . . . . . 7 tpos
4443adantr 466 . . . . . 6 tpos
45 simprl 762 . . . . . 6
46 simprr 764 . . . . . 6
4816, 38, 47, 18, 24, 26maducoeval2 19589 . . . . . 6 tpos tpos maDet tpos
4915, 44, 45, 46, 48syl211anc 1270 . . . . 5 tpos maDet tpos
50 simplr 760 . . . . . 6
5116, 38, 47, 18, 24, 26maducoeval2 19589 . . . . . 6 maDet
5215, 50, 46, 45, 51syl211anc 1270 . . . . 5 maDet
5341, 49, 523eqtr4d 2471 . . . 4 tpos
54 ovtpos 6987 . . . 4 tpos
5553, 54syl6eqr 2479 . . 3 tpos tpos
5655ralrimivva 2844 . 2 tpos tpos
5716, 47, 18maduf 19590 . . . . . . 7
5857adantr 466 . . . . . 6
5958, 43ffvelrnd 6029 . . . . 5 tpos
6016, 17, 18matbas2i 19371 . . . . 5 tpos tpos
6159, 60syl 17 . . . 4 tpos
62 elmapi 7492 . . . 4 tpos tpos
63 ffn 5737 . . . 4 tpos tpos
6461, 62, 633syl 18 . . 3 tpos
6557ffvelrnda 6028 . . . . 5
6616, 18mattposcl 19402 . . . . 5 tpos
6716, 17, 18matbas2i 19371 . . . . 5 tpos tpos
6865, 66, 673syl 18 . . . 4 tpos
69 elmapi 7492 . . . 4 tpos tpos
70 ffn 5737 . . . 4 tpos tpos
7168, 69, 703syl 18 . . 3 tpos
72 eqfnov2 6408 . . 3 tpos tpos tpos tpos tpos tpos
7364, 71, 72syl2anc 665 . 2 tpos tpos tpos tpos
7456, 73mpbird 235 1 tpos tpos