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 20990

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 20989	. . . 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 6677	. . . . 5 ⊢ (1^st ‘(1^st ‘𝑜)) ∈ V
5		fvex 6677	. . . . 5 ⊢ (2^nd ‘(1^st ‘𝑜)) ∈ V
6		fvex 6677	. . . . . . 7 ⊢ (2^nd ‘𝑜) ∈ V
7		eqidd 2822	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_m (𝑚 × 𝑛)))
8		xpeq2 5570	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑛 × 𝑝) = (𝑛 × (2^nd ‘𝑜)))
9	8	oveq2d 7166	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) = ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))))
10		eqidd 2822	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑚 = 𝑚)
11		id 22	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑝 = (2^nd ‘𝑜))
12		eqidd 2822	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
13	10, 11, 12	mpoeq123dv 7223	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
14	7, 9, 13	mpoeq123dv 7223	. . . . . . 7 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
15	6, 14	csbie 3917	. . . . . 6 ⊢ ⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
16		xpeq12 5574	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑚 × 𝑛) = ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))))
17	16	oveq2d 7166	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((Base‘𝑟) ↑_m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))))
18		simpr 487	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑛 = (2^nd ‘(1^st ‘𝑜)))
19	18	xpeq1d 5578	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑛 × (2^nd ‘𝑜)) = ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)))
20	19	oveq2d 7166	. . . . . . 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 483	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑚 = (1^st ‘(1^st ‘𝑜)))
23		eqidd 2822	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (2^nd ‘𝑜) = (2^nd ‘𝑜))
24		eqidd 2822	. . . . . . . . . 10 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))
25	18, 24	mpteq12dv 5143	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))
26	25	oveq2d 7166	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
27	22, 23, 26	mpoeq123dv 7223	. . . . . . 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 7223	. . . . . 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	syl5eq 2868	. . . . 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 3921	. . . 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 769	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → 𝑟 = 𝑅)
32	31	fveq2d 6668	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = (Base‘𝑅))
33		mamufval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
34	32, 33	syl6eqr 2874	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = 𝐵)
35		fveq2 6664	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘𝑜) = (1^st ‘⟨𝑀, 𝑁, 𝑃⟩))
36	35	fveq2d 6668	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘(1^st ‘𝑜)) = (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
37	36	ad2antll 727	. . . . . . . 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 7697	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
42	38, 39, 40, 41	syl3anc 1367	. . . . . . . . 9 ⊢ (𝜑 → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
43	42	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
44	37, 43	eqtrd 2856	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘𝑜)) = 𝑀)
45	35	fveq2d 6668	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
46	45	ad2antll 727	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
47		ot2ndg 7698	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
48	38, 39, 40, 47	syl3anc 1367	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
49	48	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
50	46, 49	eqtrd 2856	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = 𝑁)
51	44, 50	xpeq12d 5580	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))) = (𝑀 × 𝑁))
52	34, 51	oveq12d 7168	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))) = (𝐵 ↑_m (𝑀 × 𝑁)))
53		fveq2 6664	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
54	53	ad2antll 727	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
55		ot3rdg 7699	. . . . . . . . . 10 ⊢ (𝑃 ∈ Fin → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
56	40, 55	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
57	56	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
58	54, 57	eqtrd 2856	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = 𝑃)
59	50, 58	xpeq12d 5580	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)) = (𝑁 × 𝑃))
60	34, 59	oveq12d 7168	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) = (𝐵 ↑_m (𝑁 × 𝑃)))
61	31	fveq2d 6668	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = (._r‘𝑅))
62		mamufval.t	. . . . . . . . . 10 ⊢ · = (._r‘𝑅)
63	61, 62	syl6eqr 2874	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = · )
64	63	oveqd 7167	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))
65	50, 64	mpteq12dv 5143	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))
66	31, 65	oveq12d 7168	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))
67	44, 58, 66	mpoeq123dv 7223	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))
68	52, 60, 67	mpoeq123dv 7223	. . . 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	syl5eq 2868	. . 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 3514	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
72		otex 5349	. . . 4 ⊢ ⟨𝑀, 𝑁, 𝑃⟩ ∈ V
73	72	a1i 11	. . 3 ⊢ (𝜑 → ⟨𝑀, 𝑁, 𝑃⟩ ∈ V)
74		ovex 7183	. . . . 5 ⊢ (𝐵 ↑_m (𝑀 × 𝑁)) ∈ V
75		ovex 7183	. . . . 5 ⊢ (𝐵 ↑_m (𝑁 × 𝑃)) ∈ V
76	74, 75	mpoex 7771	. . . 4 ⊢ (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V
77	76	a1i 11	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V)
78	3, 69, 71, 73, 77	ovmpod 7296	. 2 ⊢ (𝜑 → (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩) = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
79	1, 78	syl5eq 2868	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 = wceq 1533 ∈ wcel 2110 Vcvv 3494 ⦋csb 3882 ⟨cotp 4568 ↦ cmpt 5138 × cxp 5547 ‘cfv 6349 (class class class)co 7150 ∈ cmpo 7152 1^st c1st 7681 2^nd c2nd 7682 ↑_m cmap 8400 Fincfn 8503 Basecbs 16477 ._rcmulr 16560 Σ_g cgsu 16708 maMul cmmul 20988

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-op 4567 df-ot 4569 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-ov 7153 df-oprab 7154 df-mpo 7155 df-1st 7683 df-2nd 7684 df-mamu 20989

This theorem is referenced by: mamuval 20991 mamudm 20993

W3C validator