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 20559

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	⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑_𝑚 (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_𝑚 (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_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 20558	. . . 4 ⊢ maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1^st ‘(1^st ‘𝑜)) / 𝑚⦌⦋(2^nd ‘(1^st ‘𝑜)) / 𝑛⦌⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
3	2	a1i 11	. . 3 ⊢ (𝜑 → maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1^st ‘(1^st ‘𝑜)) / 𝑚⦌⦋(2^nd ‘(1^st ‘𝑜)) / 𝑛⦌⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))))
4		fvex 6447	. . . . 5 ⊢ (1^st ‘(1^st ‘𝑜)) ∈ V
5		fvex 6447	. . . . 5 ⊢ (2^nd ‘(1^st ‘𝑜)) ∈ V
6		fvex 6447	. . . . . . 7 ⊢ (2^nd ‘𝑜) ∈ V
7		eqidd 2827	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)))
8		xpeq2 5364	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑛 × 𝑝) = (𝑛 × (2^nd ‘𝑜)))
9	8	oveq2d 6922	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_𝑚 (𝑛 × 𝑝)) = ((Base‘𝑟) ↑_𝑚 (𝑛 × (2^nd ‘𝑜))))
10		eqidd 2827	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑚 = 𝑚)
11		id 22	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑝 = (2^nd ‘𝑜))
12		eqidd 2827	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
13	10, 11, 12	mpt2eq123dv 6978	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
14	7, 9, 13	mpt2eq123dv 6978	. . . . . . 7 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
15	6, 14	csbie 3784	. . . . . 6 ⊢ ⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
16		xpeq12 5368	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑚 × 𝑛) = ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))))
17	16	oveq2d 6922	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_𝑚 ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))))
18		simpr 479	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑛 = (2^nd ‘(1^st ‘𝑜)))
19	18	xpeq1d 5372	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑛 × (2^nd ‘𝑜)) = ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)))
20	19	oveq2d 6922	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((Base‘𝑟) ↑_𝑚 (𝑛 × (2^nd ‘𝑜))) = ((Base‘𝑟) ↑_𝑚 ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))))
21		id 22	. . . . . . . . 9 ⊢ (𝑚 = (1^st ‘(1^st ‘𝑜)) → 𝑚 = (1^st ‘(1^st ‘𝑜)))
22	21	adantr 474	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑚 = (1^st ‘(1^st ‘𝑜)))
23		eqidd 2827	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (2^nd ‘𝑜) = (2^nd ‘𝑜))
24		eqidd 2827	. . . . . . . . . 10 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))
25	18, 24	mpteq12dv 4957	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))
26	25	oveq2d 6922	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
27	22, 23, 26	mpt2eq123dv 6978	. . . . . . 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	mpt2eq123dv 6978	. . . . . 6 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_𝑚 ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) ↦ (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
29	15, 28	syl5eq 2874	. . . . 5 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_𝑚 ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) ↦ (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
30	4, 5, 29	csbie2 3788	. . . 4 ⊢ ⦋(1^st ‘(1^st ‘𝑜)) / 𝑚⦌⦋(2^nd ‘(1^st ‘𝑜)) / 𝑛⦌⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_𝑚 ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) ↦ (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
31		simprl 789	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → 𝑟 = 𝑅)
32	31	fveq2d 6438	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = (Base‘𝑅))
33		mamufval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
34	32, 33	syl6eqr 2880	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = 𝐵)
35		fveq2 6434	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘𝑜) = (1^st ‘⟨𝑀, 𝑁, 𝑃⟩))
36	35	fveq2d 6438	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘(1^st ‘𝑜)) = (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
37	36	ad2antll 722	. . . . . . . 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 7443	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
42	38, 39, 40, 41	syl3anc 1496	. . . . . . . . 9 ⊢ (𝜑 → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
43	42	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
44	37, 43	eqtrd 2862	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘𝑜)) = 𝑀)
45	35	fveq2d 6438	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
46	45	ad2antll 722	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
47		ot2ndg 7444	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
48	38, 39, 40, 47	syl3anc 1496	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
49	48	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
50	46, 49	eqtrd 2862	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = 𝑁)
51	44, 50	xpeq12d 5374	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))) = (𝑀 × 𝑁))
52	34, 51	oveq12d 6924	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_𝑚 ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))) = (𝐵 ↑_𝑚 (𝑀 × 𝑁)))
53		fveq2 6434	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
54	53	ad2antll 722	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
55		ot3rdg 7445	. . . . . . . . . 10 ⊢ (𝑃 ∈ Fin → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
56	40, 55	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
57	56	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
58	54, 57	eqtrd 2862	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = 𝑃)
59	50, 58	xpeq12d 5374	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)) = (𝑁 × 𝑃))
60	34, 59	oveq12d 6924	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_𝑚 ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) = (𝐵 ↑_𝑚 (𝑁 × 𝑃)))
61	31	fveq2d 6438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = (._r‘𝑅))
62		mamufval.t	. . . . . . . . . 10 ⊢ · = (._r‘𝑅)
63	61, 62	syl6eqr 2880	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = · )
64	63	oveqd 6923	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))
65	50, 64	mpteq12dv 4957	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))
66	31, 65	oveq12d 6924	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))
67	44, 58, 66	mpt2eq123dv 6978	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))
68	52, 60, 67	mpt2eq123dv 6978	. . . 4 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑥 ∈ ((Base‘𝑟) ↑_𝑚 ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) ↦ (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ (𝐵 ↑_𝑚 (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_𝑚 (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
69	30, 68	syl5eq 2874	. . 3 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ⦋(1^st ‘(1^st ‘𝑜)) / 𝑚⦌⦋(2^nd ‘(1^st ‘𝑜)) / 𝑛⦌⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_𝑚 (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ (𝐵 ↑_𝑚 (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_𝑚 (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
70		mamufval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑉)
71		elex 3430	. . . 4 ⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V)
72	70, 71	syl 17	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
73		otex 5155	. . . 4 ⊢ ⟨𝑀, 𝑁, 𝑃⟩ ∈ V
74	73	a1i 11	. . 3 ⊢ (𝜑 → ⟨𝑀, 𝑁, 𝑃⟩ ∈ V)
75		ovex 6938	. . . . 5 ⊢ (𝐵 ↑_𝑚 (𝑀 × 𝑁)) ∈ V
76		ovex 6938	. . . . 5 ⊢ (𝐵 ↑_𝑚 (𝑁 × 𝑃)) ∈ V
77	75, 76	mpt2ex 7511	. . . 4 ⊢ (𝑥 ∈ (𝐵 ↑_𝑚 (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_𝑚 (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V
78	77	a1i 11	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑_𝑚 (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_𝑚 (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V)
79	3, 69, 72, 74, 78	ovmpt2d 7049	. 2 ⊢ (𝜑 → (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩) = (𝑥 ∈ (𝐵 ↑_𝑚 (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_𝑚 (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
80	1, 79	syl5eq 2874	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑_𝑚 (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_𝑚 (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 386 = wceq 1658 ∈ wcel 2166 Vcvv 3415 ⦋csb 3758 ⟨cotp 4406 ↦ cmpt 4953 × cxp 5341 ‘cfv 6124 (class class class)co 6906 ↦ cmpt2 6908 1^st c1st 7427 2^nd c2nd 7428 ↑_𝑚 cmap 8123 Fincfn 8223 Basecbs 16223 ._rcmulr 16307 Σ_g cgsu 16455 maMul cmmul 20557

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-rep 4995 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210

This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-ral 3123 df-rex 3124 df-reu 3125 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-ot 4407 df-uni 4660 df-iun 4743 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-ov 6909 df-oprab 6910 df-mpt2 6911 df-1st 7429 df-2nd 7430 df-mamu 20558

This theorem is referenced by: mamuval 20560 mamudm 20562

W3C validator