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

 Description: Multiplying a matrix with its adjunct results in the identity matrix multiplied with the determinant of the matrix. See Proposition 4.16 in [Lang] p. 518. (Contributed by Stefan O'Rear, 16-Jul-2018.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2451 . . 3 maMul maMul
2 eqid 2451 . . 3
3 eqid 2451 . . 3
4 simpr 463 . . 3
5 madurid.a . . . . . 6 Mat
6 madurid.b . . . . . 6
75, 6matrcl 19437 . . . . 5
87simpld 461 . . . 4
105, 2, 6matbas2i 19447 . . . 4
135, 12, 6maduf 19666 . . . . . 6
1413adantl 468 . . . . 5
15 simpl 459 . . . . 5
1614, 15ffvelrnd 6023 . . . 4
175, 2, 6matbas2i 19447 . . . 4
1816, 17syl 17 . . 3
191, 2, 3, 4, 9, 9, 9, 11, 18mamuval 19411 . 2 maMul g
205, 1matmulr 19463 . . . . 5 maMul
218, 20sylan 474 . . . 4 maMul
22 madurid.t . . . 4
2321, 22syl6eqr 2503 . . 3 maMul
2423oveqd 6307 . 2 maMul
26 simp1l 1032 . . . . . 6
27 simp1r 1033 . . . . . 6
28 elmapi 7493 . . . . . . . . . 10
2911, 28syl 17 . . . . . . . . 9
30293ad2ant1 1029 . . . . . . . 8
3130adantr 467 . . . . . . 7
32 simpl2 1012 . . . . . . 7
33 simpr 463 . . . . . . 7
3431, 32, 33fovrnd 6441 . . . . . 6
35 simp3 1010 . . . . . 6
365, 12, 6, 25, 3, 2, 26, 27, 34, 35madugsum 19668 . . . . 5 g
37 iftrue 3887 . . . . . . . . 9
3837adantl 468 . . . . . . . 8
39 ffn 5728 . . . . . . . . . . . . 13
4029, 39syl 17 . . . . . . . . . . . 12
41 fnov 6404 . . . . . . . . . . . 12
4240, 41sylib 200 . . . . . . . . . . 11
4342adantr 467 . . . . . . . . . 10
44 equtr2 1869 . . . . . . . . . . . . . . 15
4544oveq1d 6305 . . . . . . . . . . . . . 14
4645ifeq1da 3911 . . . . . . . . . . . . 13
47 ifid 3918 . . . . . . . . . . . . 13
4846, 47syl6eq 2501 . . . . . . . . . . . 12
4948adantl 468 . . . . . . . . . . 11
5049mpt2eq3dv 6357 . . . . . . . . . 10
5143, 50eqtr4d 2488 . . . . . . . . 9
5251fveq2d 5869 . . . . . . . 8
5338, 52eqtr2d 2486 . . . . . . 7
54533ad2antl1 1170 . . . . . 6
55 eqid 2451 . . . . . . . 8
56 simpl1r 1060 . . . . . . . 8
5793ad2ant1 1029 . . . . . . . . 9
5857adantr 467 . . . . . . . 8
5930ad2antrr 732 . . . . . . . . 9
60 simpll2 1048 . . . . . . . . 9
61 simpr 463 . . . . . . . . 9
6259, 60, 61fovrnd 6441 . . . . . . . 8
6330adantr 467 . . . . . . . . . 10
6463fovrnda 6440 . . . . . . . . 9
65643impb 1204 . . . . . . . 8
66 simpl3 1013 . . . . . . . 8
67 simpl2 1012 . . . . . . . 8
68 df-ne 2624 . . . . . . . . . . 11
6968biimpri 210 . . . . . . . . . 10
7069necomd 2679 . . . . . . . . 9
7170adantl 468 . . . . . . . 8
7225, 2, 55, 56, 58, 62, 65, 66, 67, 71mdetralt2 19634 . . . . . . 7
73 ifid 3918 . . . . . . . . . . 11
74 oveq1 6297 . . . . . . . . . . . . 13
7574adantl 468 . . . . . . . . . . . 12
7675ifeq1da 3911 . . . . . . . . . . 11
7773, 76syl5eqr 2499 . . . . . . . . . 10
7877ifeq2d 3900 . . . . . . . . 9
7978mpt2eq3dv 6357 . . . . . . . 8
8079fveq2d 5869 . . . . . . 7
81 iffalse 3890 . . . . . . . 8
8281adantl 468 . . . . . . 7
8372, 80, 823eqtr4d 2495 . . . . . 6
8454, 83pm2.61dan 800 . . . . 5
8536, 84eqtrd 2485 . . . 4 g
8685mpt2eq3dva 6355 . . 3 g
87 madurid.i . . . . 5
8887oveq2i 6301 . . . 4
89 crngring 17791 . . . . . 6
9089adantl 468 . . . . 5
9125, 5, 6, 2mdetf 19620 . . . . . . 7
9291adantl 468 . . . . . 6
9392, 15ffvelrnd 6023 . . . . 5
94 madurid.s . . . . . 6
955, 2, 94, 55matsc 19475 . . . . 5
969, 90, 93, 95syl3anc 1268 . . . 4
9788, 96syl5eq 2497 . . 3
9886, 97eqtr4d 2488 . 2 g
9919, 24, 983eqtr3d 2493 1