Theorem cramer

Description: 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 [unique 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." If it is assumed that a (unique) solution exists, it can be obtained by Cramer's rule (see also cramerimp ). On the other hand, if a vector can be constructed by Cramer's rule, it is a solution of the system of linear equations, so at least one solution exists. The uniqueness is ensured by considering only systems of linear equations whose matrix has a unit (of the underlying ring) as determinant, see matunit or slesolinv . For fields as underlying rings, this requirement is equivalent to the determinant not being 0. Theorem 4.4 in Lang p. 513. This is Metamath 100 proof #97. (Contributed by Alexander van der Vekens, 21-Feb-2019) (Revised by Alexander van der Vekens, 1-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		cramer.a	|- A = ( N Mat R )
2		cramer.b	|- B = ( Base ` A )
3		cramer.v	|- V = ( ( Base ` R ) ^m N )
4		cramer.d	|- D = ( N maDet R )
5		cramer.x	|- .x. = ( R maVecMul <. N , N >. )
6		cramer.q	|- ./ = ( /r ` R )
7		pm3.22	|- ( ( R e. CRing /\ N =/= (/) ) -> ( N =/= (/) /\ R e. CRing ) )
8	1 2 3 4 5 6	cramerlem3	|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) )
9	7 8	syl3an1	|- ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) )
10		simpl1l	|- ( ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> R e. CRing )
11		simpl2	|- ( ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> ( X e. B /\ Y e. V ) )
12		simpl3	|- ( ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> ( D ` X ) e. ( Unit ` R ) )
13		crngring	|- ( R e. CRing -> R e. Ring )
14	13	anim1ci	|- ( ( R e. CRing /\ N =/= (/) ) -> ( N =/= (/) /\ R e. Ring ) )
15	14	anim1i	|- ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) ) -> ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) )
16	15	3adant3	|- ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) )
17	1 2 3 5	slesolvec	|- ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )
18	17	imp	|- ( ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) /\ ( X .x. Z ) = Y ) -> Z e. V )
19	16 18	sylan	|- ( ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> Z e. V )
20		simpr	|- ( ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> ( X .x. Z ) = Y )
21	1 2 3 4 5 6	cramerlem1	|- ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) )
22	10 11 12 19 20 21	syl113anc	|- ( ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) )
23	22	ex	|- ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( X .x. Z ) = Y -> Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )
24	9 23	impbid	|- ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) <-> ( X .x. Z ) = Y ) )