Theorem mavmulcl

Description: Multiplication of an NxN matrix with an N-dimensional vector results in an N-dimensional vector. (Contributed by AV, 6-Dec-2018) (Revised by AV, 23-Feb-2019) (Proof shortened by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	mavmulcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mavmulcl.m	⊢ × = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
	mavmulcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mavmulcl.t	⊢ · = ( .r ‘ 𝑅 )
	mavmulcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mavmulcl.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mavmulcl.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
	mavmulcl.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
Assertion	mavmulcl	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		mavmulcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mavmulcl.m	⊢ × = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
3		mavmulcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		mavmulcl.t	⊢ · = ( .r ‘ 𝑅 )
5		mavmulcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		mavmulcl.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		mavmulcl.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
8		mavmulcl.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
9	1 2 3 4 5 6 7 8	mavmulval	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
10		ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
11	5 10	syl	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ CMnd )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑁 ∈ Fin )
14	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
15	1 3	matbas2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
16	6 5 15	syl2anc	⊢ ( 𝜑 → ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
17	7 16	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
18		elmapi	⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
19	17 18	syl	⊢ ( 𝜑 → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
20	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
22	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
23		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
24	20 22 23	fovrnd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 )
25		elmapi	⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) → 𝑌 : 𝑁 ⟶ 𝐵 )
26	8 25	syl	⊢ ( 𝜑 → 𝑌 : 𝑁 ⟶ 𝐵 )
27	26	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑌 : 𝑁 ⟶ 𝐵 )
28	27 23	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
29	3 4	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 ∧ ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
30	14 24 28 29	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
31	30	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
32	3 12 13 31	gsummptcl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ∈ 𝐵 )
33	32	ralrimiva	⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑁 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ∈ 𝐵 )
34		eqid	⊢ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) )
35	34	fmpt	⊢ ( ∀ 𝑖 ∈ 𝑁 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ∈ 𝐵 ↔ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) : 𝑁 ⟶ 𝐵 )
36	3	fvexi	⊢ 𝐵 ∈ V
37		elmapg	⊢ ( ( 𝐵 ∈ V ∧ 𝑁 ∈ Fin ) → ( ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ ( 𝐵 ↑m 𝑁 ) ↔ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) : 𝑁 ⟶ 𝐵 ) )
38	36 6 37	sylancr	⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ ( 𝐵 ↑m 𝑁 ) ↔ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) : 𝑁 ⟶ 𝐵 ) )
39	35 38	bitr4id	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝑁 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ∈ 𝐵 ↔ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ ( 𝐵 ↑m 𝑁 ) ) )
40	33 39	mpbid	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ ( 𝐵 ↑m 𝑁 ) )
41	9 40	eqeltrd	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) )