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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	slesolex.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	slesolex.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
	slesolex.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
Assertion	slesolvec	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		slesolex.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		slesolex.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		slesolex.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4		slesolex.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
5	1 2	matrcl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6	5	simpld	⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
7		simpr	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin ) → 𝑁 ∈ Fin )
8		simpl	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin ) → 𝑁 ≠ ∅ )
9	7 7 8	3jca	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) )
10	9	ex	⊢ ( 𝑁 ≠ ∅ → ( 𝑁 ∈ Fin → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) )
11	10	adantr	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) )
12	6 11	syl5com	⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) )
13	12	adantr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) )
14	13	impcom	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) )
15		simpr	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
16		simpr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
17	15 16	anim12i	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑉 ) )
18		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19		eqid	⊢ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) )
20	18 19 3 4 3	mavmulsolcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )
21	14 17 20	syl2anc	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )