mavmulsolcl

Description: Every solution of the equation A * X = Y for a matrix A and a vector B is a vector. (Contributed by AV, 27-Feb-2019)

	Ref	Expression
Hypotheses	mavmuldm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mavmuldm.c	⊢ 𝐶 = ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) )
	mavmuldm.d	⊢ 𝐷 = ( 𝐵 ↑_m 𝑁 )
	mavmuldm.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
	mavmulsolcl.e	⊢ 𝐸 = ( 𝐵 ↑_m 𝑀 )
Assertion	mavmulsolcl	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		mavmuldm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		mavmuldm.c	⊢ 𝐶 = ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) )
3		mavmuldm.d	⊢ 𝐷 = ( 𝐵 ↑_m 𝑁 )
4		mavmuldm.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
5		mavmulsolcl.e	⊢ 𝐸 = ( 𝐵 ↑_m 𝑀 )
6		2a1	⊢ ( 𝑋 ∈ 𝐷 → ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) ) )
7		simpl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) → 𝑅 ∈ 𝑉 )
8	7	adantl	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → 𝑅 ∈ 𝑉 )
9		simpl1	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → 𝑀 ∈ Fin )
10		simpl2	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → 𝑁 ∈ Fin )
11	8 9 10	3jca	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) )
12	11	adantl	⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) )
13	1 2 3 4	mavmuldm	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → dom · = ( 𝐶 × 𝐷 ) )
14	12 13	syl	⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → dom · = ( 𝐶 × 𝐷 ) )
15		simpl	⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ¬ 𝑋 ∈ 𝐷 )
16	15	intnand	⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ¬ ( 𝐴 ∈ 𝐶 ∧ 𝑋 ∈ 𝐷 ) )
17		ndmovg	⊢ ( ( dom · = ( 𝐶 × 𝐷 ) ∧ ¬ ( 𝐴 ∈ 𝐶 ∧ 𝑋 ∈ 𝐷 ) ) → ( 𝐴 · 𝑋 ) = ∅ )
18	14 16 17	syl2anc	⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( 𝐴 · 𝑋 ) = ∅ )
19		eqeq1	⊢ ( ( 𝐴 · 𝑋 ) = ∅ → ( ( 𝐴 · 𝑋 ) = 𝑌 ↔ ∅ = 𝑌 ) )
20		elmapi	⊢ ( 𝑌 ∈ ( 𝐵 ↑_m 𝑀 ) → 𝑌 : 𝑀 ⟶ 𝐵 )
21		f0dom0	⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( 𝑀 = ∅ ↔ 𝑌 = ∅ ) )
22	21	biimprd	⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( 𝑌 = ∅ → 𝑀 = ∅ ) )
23	22	necon3d	⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( 𝑀 ≠ ∅ → 𝑌 ≠ ∅ ) )
24	23	com12	⊢ ( 𝑀 ≠ ∅ → ( 𝑌 : 𝑀 ⟶ 𝐵 → 𝑌 ≠ ∅ ) )
25	24	3ad2ant3	⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → ( 𝑌 : 𝑀 ⟶ 𝐵 → 𝑌 ≠ ∅ ) )
26	25	com12	⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) )
27	26	a1d	⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( 𝑅 ∈ 𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) )
28	20 27	syl	⊢ ( 𝑌 ∈ ( 𝐵 ↑_m 𝑀 ) → ( 𝑅 ∈ 𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) )
29	28 5	eleq2s	⊢ ( 𝑌 ∈ 𝐸 → ( 𝑅 ∈ 𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) )
30	29	impcom	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) )
31	30	impcom	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → 𝑌 ≠ ∅ )
32		eqneqall	⊢ ( 𝑌 = ∅ → ( 𝑌 ≠ ∅ → 𝑋 ∈ 𝐷 ) )
33	31 32	syl5com	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( 𝑌 = ∅ → 𝑋 ∈ 𝐷 ) )
34	33	adantl	⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( 𝑌 = ∅ → 𝑋 ∈ 𝐷 ) )
35	34	com12	⊢ ( 𝑌 = ∅ → ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → 𝑋 ∈ 𝐷 ) )
36	35	eqcoms	⊢ ( ∅ = 𝑌 → ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → 𝑋 ∈ 𝐷 ) )
37	19 36	biimtrdi	⊢ ( ( 𝐴 · 𝑋 ) = ∅ → ( ( 𝐴 · 𝑋 ) = 𝑌 → ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → 𝑋 ∈ 𝐷 ) ) )
38	37	com23	⊢ ( ( 𝐴 · 𝑋 ) = ∅ → ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) ) )
39	18 38	mpcom	⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) )
40	39	ex	⊢ ( ¬ 𝑋 ∈ 𝐷 → ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) ) )
41	6 40	pm2.61i	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) )

Metamath Proof Explorer

Theorem mavmulsolcl

Proof