Theorem cramerlem2

Description: Lemma 2 for cramer . (Contributed by AV, 21-Feb-2019) (Revised by AV, 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	cramerlem2	|- ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )

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		simpll1	|- ( ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ z e. V ) /\ ( X .x. z ) = Y ) -> R e. CRing )
8		simpll2	|- ( ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ z e. V ) /\ ( X .x. z ) = Y ) -> ( X e. B /\ Y e. V ) )
9		simpll3	|- ( ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ z e. V ) /\ ( X .x. z ) = Y ) -> ( D ` X ) e. ( Unit ` R ) )
10		simplr	|- ( ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ z e. V ) /\ ( X .x. z ) = Y ) -> z e. V )
11		simpr	|- ( ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ z e. V ) /\ ( X .x. z ) = Y ) -> ( X .x. z ) = Y )
12	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 ) ) ) )
13	7 8 9 10 11 12	syl113anc	|- ( ( ( ( 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 ) ) ) )
14	13	ex	|- ( ( ( 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 ) ) ) ) )
15	14	ralrimiva	|- ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )