mvmulfval

Description: Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019)

	Ref	Expression
Hypotheses	mvmulfval.x	⊢ × = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
	mvmulfval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mvmulfval.t	⊢ · = ( ._r ‘ 𝑅 )
	mvmulfval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	mvmulfval.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
	mvmulfval.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
Assertion	mvmulfval	⊢ ( 𝜑 → × = ( 𝑥 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑_m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mvmulfval.x	⊢ × = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
2		mvmulfval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		mvmulfval.t	⊢ · = ( ._r ‘ 𝑅 )
4		mvmulfval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
5		mvmulfval.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
6		mvmulfval.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		df-mvmul	⊢ maVecMul = ( 𝑟 ∈ V , 𝑜 ∈ V ↦ ⦋ ( 1^st ‘ 𝑜 ) / 𝑚 ⦌ ⦋ ( 2^nd ‘ 𝑜 ) / 𝑛 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) ↦ ( 𝑖 ∈ 𝑚 ↦ ( 𝑟 Σ_g ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )
8	7	a1i	⊢ ( 𝜑 → maVecMul = ( 𝑟 ∈ V , 𝑜 ∈ V ↦ ⦋ ( 1^st ‘ 𝑜 ) / 𝑚 ⦌ ⦋ ( 2^nd ‘ 𝑜 ) / 𝑛 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) ↦ ( 𝑖 ∈ 𝑚 ↦ ( 𝑟 Σ_g ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) ) )
9		fvex	⊢ ( 1^st ‘ 𝑜 ) ∈ V
10		fvex	⊢ ( 2^nd ‘ 𝑜 ) ∈ V
11		xpeq12	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → ( 𝑚 × 𝑛 ) = ( ( 1^st ‘ 𝑜 ) × ( 2^nd ‘ 𝑜 ) ) )
12	11	oveq2d	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → ( ( Base ‘ 𝑟 ) ↑_m ( 𝑚 × 𝑛 ) ) = ( ( Base ‘ 𝑟 ) ↑_m ( ( 1^st ‘ 𝑜 ) × ( 2^nd ‘ 𝑜 ) ) ) )
13		oveq2	⊢ ( 𝑛 = ( 2^nd ‘ 𝑜 ) → ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) = ( ( Base ‘ 𝑟 ) ↑_m ( 2^nd ‘ 𝑜 ) ) )
14	13	adantl	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) = ( ( Base ‘ 𝑟 ) ↑_m ( 2^nd ‘ 𝑜 ) ) )
15		simpl	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → 𝑚 = ( 1^st ‘ 𝑜 ) )
16		simpr	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → 𝑛 = ( 2^nd ‘ 𝑜 ) )
17	16	mpteq1d	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) )
18	17	oveq2d	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → ( 𝑟 Σ_g ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) = ( 𝑟 Σ_g ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) )
19	15 18	mpteq12dv	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → ( 𝑖 ∈ 𝑚 ↦ ( 𝑟 Σ_g ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) = ( 𝑖 ∈ ( 1^st ‘ 𝑜 ) ↦ ( 𝑟 Σ_g ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) )
20	12 14 19	mpoeq123dv	⊢ ( ( 𝑚 = ( 1^st ‘ 𝑜 ) ∧ 𝑛 = ( 2^nd ‘ 𝑜 ) ) → ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) ↦ ( 𝑖 ∈ 𝑚 ↦ ( 𝑟 Σ_g ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( ( 1^st ‘ 𝑜 ) × ( 2^nd ‘ 𝑜 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( 2^nd ‘ 𝑜 ) ) ↦ ( 𝑖 ∈ ( 1^st ‘ 𝑜 ) ↦ ( 𝑟 Σ_g ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )
21	9 10 20	csbie2	⊢ ⦋ ( 1^st ‘ 𝑜 ) / 𝑚 ⦌ ⦋ ( 2^nd ‘ 𝑜 ) / 𝑛 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) ↦ ( 𝑖 ∈ 𝑚 ↦ ( 𝑟 Σ_g ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( ( 1^st ‘ 𝑜 ) × ( 2^nd ‘ 𝑜 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( 2^nd ‘ 𝑜 ) ) ↦ ( 𝑖 ∈ ( 1^st ‘ 𝑜 ) ↦ ( 𝑟 Σ_g ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) )
22		simprl	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → 𝑟 = 𝑅 )
23	22	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
24	23 2	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( Base ‘ 𝑟 ) = 𝐵 )
25		fveq2	⊢ ( 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ → ( 1^st ‘ 𝑜 ) = ( 1^st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
26	25	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 1^st ‘ 𝑜 ) = ( 1^st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
27		op1stg	⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 1^st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
28	5 6 27	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
29	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 1^st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
30	26 29	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 1^st ‘ 𝑜 ) = 𝑀 )
31		fveq2	⊢ ( 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ → ( 2^nd ‘ 𝑜 ) = ( 2^nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
32	31	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 2^nd ‘ 𝑜 ) = ( 2^nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
33		op2ndg	⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 2^nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
34	5 6 33	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
35	34	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 2^nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
36	32 35	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 2^nd ‘ 𝑜 ) = 𝑁 )
37	30 36	xpeq12d	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( ( 1^st ‘ 𝑜 ) × ( 2^nd ‘ 𝑜 ) ) = ( 𝑀 × 𝑁 ) )
38	24 37	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( ( Base ‘ 𝑟 ) ↑_m ( ( 1^st ‘ 𝑜 ) × ( 2^nd ‘ 𝑜 ) ) ) = ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) )
39	24 36	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( ( Base ‘ 𝑟 ) ↑_m ( 2^nd ‘ 𝑜 ) ) = ( 𝐵 ↑_m 𝑁 ) )
40		fveq2	⊢ ( 𝑟 = 𝑅 → ( ._r ‘ 𝑟 ) = ( ._r ‘ 𝑅 ) )
41	40	adantr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) → ( ._r ‘ 𝑟 ) = ( ._r ‘ 𝑅 ) )
42	41	adantl	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( ._r ‘ 𝑟 ) = ( ._r ‘ 𝑅 ) )
43	42 3	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( ._r ‘ 𝑟 ) = · )
44	43	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) )
45	36 44	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) )
46	22 45	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 𝑟 Σ_g ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) )
47	30 46	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 𝑖 ∈ ( 1^st ‘ 𝑜 ) ↦ ( 𝑟 Σ_g ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) = ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) )
48	38 39 47	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( ( 1^st ‘ 𝑜 ) × ( 2^nd ‘ 𝑜 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( 2^nd ‘ 𝑜 ) ) ↦ ( 𝑖 ∈ ( 1^st ‘ 𝑜 ) ↦ ( 𝑟 Σ_g ( 𝑗 ∈ ( 2^nd ‘ 𝑜 ) ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑_m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )
49	21 48	syl5eq	⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑜 = ⟨ 𝑀 , 𝑁 ⟩ ) ) → ⦋ ( 1^st ‘ 𝑜 ) / 𝑚 ⦌ ⦋ ( 2^nd ‘ 𝑜 ) / 𝑛 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑_m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) ↦ ( 𝑖 ∈ 𝑚 ↦ ( 𝑟 Σ_g ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( ._r ‘ 𝑟 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑_m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )
50	4	elexd	⊢ ( 𝜑 → 𝑅 ∈ V )
51		opex	⊢ ⟨ 𝑀 , 𝑁 ⟩ ∈ V
52	51	a1i	⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ V )
53		ovex	⊢ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) ∈ V
54		ovex	⊢ ( 𝐵 ↑_m 𝑁 ) ∈ V
55	53 54	mpoex	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑_m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) ∈ V
56	55	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑_m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) ∈ V )
57	8 49 50 52 56	ovmpod	⊢ ( 𝜑 → ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑥 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑_m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )
58	1 57	syl5eq	⊢ ( 𝜑 → × = ( 𝑥 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑_m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )

Metamath Proof Explorer

Theorem mvmulfval

Proof