Metamath Proof Explorer

Theorem slesolvec

Description: Every solution of a system of linear equations represented by a matrix and a vector is a vector. (Contributed by AV, 10-Feb-2019) (Revised by AV, 27-Feb-2019)

Ref Expression
Hypotheses slesolex.a 
|- A = ( N Mat R )
slesolex.b 
|- B = ( Base ` A )
slesolex.v 
|- V = ( ( Base ` R ) ^m N )
slesolex.x 
|- .x. = ( R maVecMul <. N , N >. )
Assertion slesolvec 
|- ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )

Proof

Step Hyp Ref Expression
1 slesolex.a 
 |-  A = ( N Mat R )
2 slesolex.b 
 |-  B = ( Base ` A )
3 slesolex.v 
 |-  V = ( ( Base ` R ) ^m N )
4 slesolex.x 
 |-  .x. = ( R maVecMul <. N , N >. )
5 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
6 5 simpld 
 |-  ( X e. B -> N e. Fin )
7 simpr 
 |-  ( ( N =/= (/) /\ N e. Fin ) -> N e. Fin )
8 simpl 
 |-  ( ( N =/= (/) /\ N e. Fin ) -> N =/= (/) )
9 7 7 8 3jca 
 |-  ( ( N =/= (/) /\ N e. Fin ) -> ( N e. Fin /\ N e. Fin /\ N =/= (/) ) )
10 9 ex 
 |-  ( N =/= (/) -> ( N e. Fin -> ( N e. Fin /\ N e. Fin /\ N =/= (/) ) ) )
11 10 adantr 
 |-  ( ( N =/= (/) /\ R e. Ring ) -> ( N e. Fin -> ( N e. Fin /\ N e. Fin /\ N =/= (/) ) ) )
12 6 11 syl5com 
 |-  ( X e. B -> ( ( N =/= (/) /\ R e. Ring ) -> ( N e. Fin /\ N e. Fin /\ N =/= (/) ) ) )
13 12 adantr 
 |-  ( ( X e. B /\ Y e. V ) -> ( ( N =/= (/) /\ R e. Ring ) -> ( N e. Fin /\ N e. Fin /\ N =/= (/) ) ) )
14 13 impcom 
 |-  ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) -> ( N e. Fin /\ N e. Fin /\ N =/= (/) ) )
15 simpr 
 |-  ( ( N =/= (/) /\ R e. Ring ) -> R e. Ring )
16 simpr 
 |-  ( ( X e. B /\ Y e. V ) -> Y e. V )
17 15 16 anim12i 
 |-  ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) -> ( R e. Ring /\ Y e. V ) )
18 eqid 
 |-  ( Base ` R ) = ( Base ` R )
19 eqid 
 |-  ( ( Base ` R ) ^m ( N X. N ) ) = ( ( Base ` R ) ^m ( N X. N ) )
20 18 19 3 4 3 mavmulsolcl 
 |-  ( ( ( N e. Fin /\ N e. Fin /\ N =/= (/) ) /\ ( R e. Ring /\ Y e. V ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )
21 14 17 20 syl2anc 
 |-  ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )