mamufval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mamufval		Structured version Visualization version GIF version

Theorem mamufval 22396

Description: Functional value of the matrix multiplication operator. (Contributed by Stefan O'Rear, 2-Sep-2015.)

**Hypotheses**
Ref	Expression
mamufval.f	⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)
mamufval.b	⊢ 𝐵 = (Base‘𝑅)
mamufval.t	⊢ · = (._r‘𝑅)
mamufval.r	⊢ (𝜑 → 𝑅 ∈ 𝑉)
mamufval.m	⊢ (𝜑 → 𝑀 ∈ Fin)
mamufval.n	⊢ (𝜑 → 𝑁 ∈ Fin)
mamufval.p	⊢ (𝜑 → 𝑃 ∈ Fin)

**Assertion**
Ref	Expression
mamufval	⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))

Distinct variable groups: 𝑖,𝑗,𝑘,𝑥,𝑦,𝑀 𝑖,𝑁,𝑗,𝑘,𝑥,𝑦 𝑃,𝑖,𝑗,𝑘,𝑥,𝑦 𝑅,𝑖,𝑗,𝑘,𝑥,𝑦 𝜑,𝑖,𝑗,𝑘,𝑥,𝑦 𝑥,𝐵,𝑦 𝑥, · ,𝑦,𝑖,𝑘 Allowed substitution hints: 𝐵(𝑖,𝑗,𝑘) · (𝑗) 𝐹(𝑥,𝑦,𝑖,𝑗,𝑘) 𝑉(𝑥,𝑦,𝑖,𝑗,𝑘)

Proof of Theorem mamufval Dummy variables 𝑚 𝑛 𝑜 𝑝 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mamufval.f	. 2 ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)
2		df-mamu 22395	. . . 4 ⊢ maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1^st ‘(1^st ‘𝑜)) / 𝑚⦌⦋(2^nd ‘(1^st ‘𝑜)) / 𝑛⦌⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
3	2	a1i 11	. . 3 ⊢ (𝜑 → maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1^st ‘(1^st ‘𝑜)) / 𝑚⦌⦋(2^nd ‘(1^st ‘𝑜)) / 𝑛⦌⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))))
4		fvex 6919	. . . . 5 ⊢ (1^st ‘(1^st ‘𝑜)) ∈ V
5		fvex 6919	. . . . 5 ⊢ (2^nd ‘(1^st ‘𝑜)) ∈ V
6		fvex 6919	. . . . . . 7 ⊢ (2^nd ‘𝑜) ∈ V
7		eqidd 2738	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_m (𝑚 × 𝑛)))
8		xpeq2 5706	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑛 × 𝑝) = (𝑛 × (2^nd ‘𝑜)))
9	8	oveq2d 7447	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) = ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))))
10		eqidd 2738	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑚 = 𝑚)
11		id 22	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑝 = (2^nd ‘𝑜))
12		eqidd 2738	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
13	10, 11, 12	mpoeq123dv 7508	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
14	7, 9, 13	mpoeq123dv 7508	. . . . . . 7 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
15	6, 14	csbie 3934	. . . . . 6 ⊢ ⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
16		xpeq12 5710	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑚 × 𝑛) = ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))))
17	16	oveq2d 7447	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((Base‘𝑟) ↑_m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))))
18		simpr 484	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑛 = (2^nd ‘(1^st ‘𝑜)))
19	18	xpeq1d 5714	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑛 × (2^nd ‘𝑜)) = ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)))
20	19	oveq2d 7447	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) = ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))))
21		id 22	. . . . . . . . 9 ⊢ (𝑚 = (1^st ‘(1^st ‘𝑜)) → 𝑚 = (1^st ‘(1^st ‘𝑜)))
22	21	adantr 480	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑚 = (1^st ‘(1^st ‘𝑜)))
23		eqidd 2738	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (2^nd ‘𝑜) = (2^nd ‘𝑜))
24		eqidd 2738	. . . . . . . . . 10 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))
25	18, 24	mpteq12dv 5233	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))
26	25	oveq2d 7447	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
27	22, 23, 26	mpoeq123dv 7508	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
28	17, 20, 27	mpoeq123dv 7508	. . . . . 6 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) ↦ (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
29	15, 28	eqtrid 2789	. . . . 5 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) ↦ (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
30	4, 5, 29	csbie2 3938	. . . 4 ⊢ ⦋(1^st ‘(1^st ‘𝑜)) / 𝑚⦌⦋(2^nd ‘(1^st ‘𝑜)) / 𝑛⦌⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) ↦ (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
31		simprl 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → 𝑟 = 𝑅)
32	31	fveq2d 6910	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = (Base‘𝑅))
33		mamufval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
34	32, 33	eqtr4di 2795	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = 𝐵)
35		fveq2 6906	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘𝑜) = (1^st ‘⟨𝑀, 𝑁, 𝑃⟩))
36	35	fveq2d 6910	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘(1^st ‘𝑜)) = (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
37	36	ad2antll 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘𝑜)) = (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
38		mamufval.m	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ Fin)
39		mamufval.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ Fin)
40		mamufval.p	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Fin)
41		ot1stg 8028	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
42	38, 39, 40, 41	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
43	42	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
44	37, 43	eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘𝑜)) = 𝑀)
45	35	fveq2d 6910	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
46	45	ad2antll 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
47		ot2ndg 8029	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
48	38, 39, 40, 47	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
49	48	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
50	46, 49	eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = 𝑁)
51	44, 50	xpeq12d 5716	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))) = (𝑀 × 𝑁))
52	34, 51	oveq12d 7449	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))) = (𝐵 ↑_m (𝑀 × 𝑁)))
53		fveq2 6906	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
54	53	ad2antll 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
55		ot3rdg 8030	. . . . . . . . . 10 ⊢ (𝑃 ∈ Fin → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
56	40, 55	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
57	56	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
58	54, 57	eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = 𝑃)
59	50, 58	xpeq12d 5716	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)) = (𝑁 × 𝑃))
60	34, 59	oveq12d 7449	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) = (𝐵 ↑_m (𝑁 × 𝑃)))
61	31	fveq2d 6910	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = (._r‘𝑅))
62		mamufval.t	. . . . . . . . . 10 ⊢ · = (._r‘𝑅)
63	61, 62	eqtr4di 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = · )
64	63	oveqd 7448	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))
65	50, 64	mpteq12dv 5233	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))
66	31, 65	oveq12d 7449	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))
67	44, 58, 66	mpoeq123dv 7508	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))
68	52, 60, 67	mpoeq123dv 7508	. . . 4 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑥 ∈ ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) ↦ (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
69	30, 68	eqtrid 2789	. . 3 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ⦋(1^st ‘(1^st ‘𝑜)) / 𝑚⦌⦋(2^nd ‘(1^st ‘𝑜)) / 𝑛⦌⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
70		mamufval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑉)
71	70	elexd 3504	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
72		otex 5470	. . . 4 ⊢ ⟨𝑀, 𝑁, 𝑃⟩ ∈ V
73	72	a1i 11	. . 3 ⊢ (𝜑 → ⟨𝑀, 𝑁, 𝑃⟩ ∈ V)
74		ovex 7464	. . . . 5 ⊢ (𝐵 ↑_m (𝑀 × 𝑁)) ∈ V
75		ovex 7464	. . . . 5 ⊢ (𝐵 ↑_m (𝑁 × 𝑃)) ∈ V
76	74, 75	mpoex 8104	. . . 4 ⊢ (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V
77	76	a1i 11	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V)
78	3, 69, 71, 73, 77	ovmpod 7585	. 2 ⊢ (𝜑 → (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩) = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
79	1, 78	eqtrid 2789	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 Vcvv 3480 ⦋csb 3899 ⟨cotp 4634 ↦ cmpt 5225 × cxp 5683 ‘cfv 6561 (class class class)co 7431 ∈ cmpo 7433 1^st c1st 8012 2^nd c2nd 8013 ↑_m cmap 8866 Fincfn 8985 Basecbs 17247 ._rcmulr 17298 Σ_g cgsu 17485 maMul cmmul 22394

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-ot 4635 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-1st 8014 df-2nd 8015 df-mamu 22395

This theorem is referenced by: mamuval 22397 mamudm 22399

W3C validator