Metamath Proof Explorer

Theorem cramerimp

Description: One direction of Cramer's rule (according to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule : "[Cramer's rule] ... expresses the solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations."): The ith component of the solution vector of a system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the righthand side vector of the system of linear equations divided by the determinant of the matrix of the system of linear equations. (Contributed by AV, 19-Feb-2019) (Revised by AV, 1-Mar-2019)

Ref Expression
Hypotheses cramerimp.a 
|- A = ( N Mat R )
cramerimp.b 
|- B = ( Base ` A )
cramerimp.v 
|- V = ( ( Base ` R ) ^m N )
cramerimp.e 
|- E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )
cramerimp.h 
|- H = ( ( X ( N matRepV R ) Y ) ` I )
cramerimp.x 
|- .x. = ( R maVecMul <. N , N >. )
cramerimp.d 
|- D = ( N maDet R )
cramerimp.q 
|- ./ = ( /r ` R )
Assertion cramerimp 
|- ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( Z ` I ) = ( ( D ` H ) ./ ( D ` X ) ) )

Proof

Step Hyp Ref Expression
1 cramerimp.a 
 |-  A = ( N Mat R )
2 cramerimp.b 
 |-  B = ( Base ` A )
3 cramerimp.v 
 |-  V = ( ( Base ` R ) ^m N )
4 cramerimp.e 
 |-  E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )
5 cramerimp.h 
 |-  H = ( ( X ( N matRepV R ) Y ) ` I )
6 cramerimp.x 
 |-  .x. = ( R maVecMul <. N , N >. )
7 cramerimp.d 
 |-  D = ( N maDet R )
8 cramerimp.q 
 |-  ./ = ( /r ` R )
9 crngring 
 |-  ( R e. CRing -> R e. Ring )
10 9 adantr 
 |-  ( ( R e. CRing /\ I e. N ) -> R e. Ring )
11 10 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> R e. Ring )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 7 1 2 12 mdetf 
 |-  ( R e. CRing -> D : B --> ( Base ` R ) )
14 13 adantr 
 |-  ( ( R e. CRing /\ I e. N ) -> D : B --> ( Base ` R ) )
15 14 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> D : B --> ( Base ` R ) )
16 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
17 16 simpld 
 |-  ( X e. B -> N e. Fin )
18 17 adantr 
 |-  ( ( X e. B /\ Y e. V ) -> N e. Fin )
19 10 18 anim12i 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> ( R e. Ring /\ N e. Fin ) )
20 19 3adant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( R e. Ring /\ N e. Fin ) )
21 ne0i 
 |-  ( I e. N -> N =/= (/) )
22 9 21 anim12ci 
 |-  ( ( R e. CRing /\ I e. N ) -> ( N =/= (/) /\ R e. Ring ) )
23 22 anim1i 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) )
24 23 3adant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) )
25 simpl 
 |-  ( ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) -> ( X .x. Z ) = Y )
26 25 3ad2ant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( X .x. Z ) = Y )
27 1 2 3 6 slesolvec 
 |-  ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )
28 24 26 27 sylc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> Z e. V )
29 simpr 
 |-  ( ( R e. CRing /\ I e. N ) -> I e. N )
30 29 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> I e. N )
31 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
32 1 2 3 31 ma1repvcl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( Z e. V /\ I e. N ) ) -> ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I ) e. B )
33 20 28 30 32 syl12anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I ) e. B )
34 4 33 eqeltrid 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> E e. B )
35 15 34 ffvelrnd 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( D ` E ) e. ( Base ` R ) )
36 simpr 
 |-  ( ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) -> ( D ` X ) e. ( Unit ` R ) )
37 36 3ad2ant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( D ` X ) e. ( Unit ` R ) )
38 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
39 eqid 
 |-  ( .r ` R ) = ( .r ` R )
40 12 38 8 39 dvrcan3 
 |-  ( ( R e. Ring /\ ( D ` E ) e. ( Base ` R ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( ( D ` E ) ( .r ` R ) ( D ` X ) ) ./ ( D ` X ) ) = ( D ` E ) )
41 11 35 37 40 syl3anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( ( D ` E ) ( .r ` R ) ( D ` X ) ) ./ ( D ` X ) ) = ( D ` E ) )
42 simpl 
 |-  ( ( R e. CRing /\ I e. N ) -> R e. CRing )
43 42 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> R e. CRing )
44 12 38 unitcl 
 |-  ( ( D ` X ) e. ( Unit ` R ) -> ( D ` X ) e. ( Base ` R ) )
45 44 adantl 
 |-  ( ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) -> ( D ` X ) e. ( Base ` R ) )
46 45 3ad2ant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( D ` X ) e. ( Base ` R ) )
47 12 39 crngcom 
 |-  ( ( R e. CRing /\ ( D ` E ) e. ( Base ` R ) /\ ( D ` X ) e. ( Base ` R ) ) -> ( ( D ` E ) ( .r ` R ) ( D ` X ) ) = ( ( D ` X ) ( .r ` R ) ( D ` E ) ) )
48 43 35 46 47 syl3anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( D ` E ) ( .r ` R ) ( D ` X ) ) = ( ( D ` X ) ( .r ` R ) ( D ` E ) ) )
49 48 oveq1d 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( ( D ` E ) ( .r ` R ) ( D ` X ) ) ./ ( D ` X ) ) = ( ( ( D ` X ) ( .r ` R ) ( D ` E ) ) ./ ( D ` X ) ) )
50 18 adantl 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> N e. Fin )
51 42 adantr 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> R e. CRing )
52 29 adantr 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> I e. N )
53 50 51 52 3jca 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> ( N e. Fin /\ R e. CRing /\ I e. N ) )
54 53 3adant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( N e. Fin /\ R e. CRing /\ I e. N ) )
55 1 3 4 7 cramerimplem1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ I e. N ) /\ Z e. V ) -> ( D ` E ) = ( Z ` I ) )
56 54 28 55 syl2anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( D ` E ) = ( Z ` I ) )
57 41 49 56 3eqtr3rd 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( Z ` I ) = ( ( ( D ` X ) ( .r ` R ) ( D ` E ) ) ./ ( D ` X ) ) )
58 1 2 3 4 5 6 7 39 cramerimplem3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( ( D ` X ) ( .r ` R ) ( D ` E ) ) = ( D ` H ) )
59 58 3adant3r 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( D ` X ) ( .r ` R ) ( D ` E ) ) = ( D ` H ) )
60 59 oveq1d 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( ( D ` X ) ( .r ` R ) ( D ` E ) ) ./ ( D ` X ) ) = ( ( D ` H ) ./ ( D ` X ) ) )
61 57 60 eqtrd 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( Z ` I ) = ( ( D ` H ) ./ ( D ` X ) ) )