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 20992

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 20991	. . . 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 6658	. . . . 5 ⊢ (1^st ‘(1^st ‘𝑜)) ∈ V
5		fvex 6658	. . . . 5 ⊢ (2^nd ‘(1^st ‘𝑜)) ∈ V
6		fvex 6658	. . . . . . 7 ⊢ (2^nd ‘𝑜) ∈ V
7		eqidd 2799	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_m (𝑚 × 𝑛)))
8		xpeq2 5540	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑛 × 𝑝) = (𝑛 × (2^nd ‘𝑜)))
9	8	oveq2d 7151	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) = ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))))
10		eqidd 2799	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑚 = 𝑚)
11		id 22	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑝 = (2^nd ‘𝑜))
12		eqidd 2799	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
13	10, 11, 12	mpoeq123dv 7208	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
14	7, 9, 13	mpoeq123dv 7208	. . . . . . 7 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
15	6, 14	csbie 3863	. . . . . 6 ⊢ ⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
16		xpeq12 5544	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑚 × 𝑛) = ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))))
17	16	oveq2d 7151	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((Base‘𝑟) ↑_m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))))
18		simpr 488	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑛 = (2^nd ‘(1^st ‘𝑜)))
19	18	xpeq1d 5548	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑛 × (2^nd ‘𝑜)) = ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)))
20	19	oveq2d 7151	. . . . . . 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 484	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑚 = (1^st ‘(1^st ‘𝑜)))
23		eqidd 2799	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (2^nd ‘𝑜) = (2^nd ‘𝑜))
24		eqidd 2799	. . . . . . . . . 10 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))
25	18, 24	mpteq12dv 5115	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))
26	25	oveq2d 7151	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
27	22, 23, 26	mpoeq123dv 7208	. . . . . . 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 7208	. . . . . 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 2845	. . . . 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 3867	. . . 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 770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → 𝑟 = 𝑅)
32	31	fveq2d 6649	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = (Base‘𝑅))
33		mamufval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
34	32, 33	eqtr4di 2851	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = 𝐵)
35		fveq2 6645	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘𝑜) = (1^st ‘⟨𝑀, 𝑁, 𝑃⟩))
36	35	fveq2d 6649	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘(1^st ‘𝑜)) = (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
37	36	ad2antll 728	. . . . . . . 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 7685	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
42	38, 39, 40, 41	syl3anc 1368	. . . . . . . . 9 ⊢ (𝜑 → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
43	42	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
44	37, 43	eqtrd 2833	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘𝑜)) = 𝑀)
45	35	fveq2d 6649	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
46	45	ad2antll 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
47		ot2ndg 7686	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
48	38, 39, 40, 47	syl3anc 1368	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
49	48	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
50	46, 49	eqtrd 2833	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = 𝑁)
51	44, 50	xpeq12d 5550	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))) = (𝑀 × 𝑁))
52	34, 51	oveq12d 7153	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))) = (𝐵 ↑_m (𝑀 × 𝑁)))
53		fveq2 6645	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
54	53	ad2antll 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
55		ot3rdg 7687	. . . . . . . . . 10 ⊢ (𝑃 ∈ Fin → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
56	40, 55	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
57	56	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
58	54, 57	eqtrd 2833	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = 𝑃)
59	50, 58	xpeq12d 5550	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)) = (𝑁 × 𝑃))
60	34, 59	oveq12d 7153	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) = (𝐵 ↑_m (𝑁 × 𝑃)))
61	31	fveq2d 6649	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = (._r‘𝑅))
62		mamufval.t	. . . . . . . . . 10 ⊢ · = (._r‘𝑅)
63	61, 62	eqtr4di 2851	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = · )
64	63	oveqd 7152	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))
65	50, 64	mpteq12dv 5115	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))
66	31, 65	oveq12d 7153	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))
67	44, 58, 66	mpoeq123dv 7208	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))
68	52, 60, 67	mpoeq123dv 7208	. . . 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 2845	. . 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 3461	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
72		otex 5322	. . . 4 ⊢ ⟨𝑀, 𝑁, 𝑃⟩ ∈ V
73	72	a1i 11	. . 3 ⊢ (𝜑 → ⟨𝑀, 𝑁, 𝑃⟩ ∈ V)
74		ovex 7168	. . . . 5 ⊢ (𝐵 ↑_m (𝑀 × 𝑁)) ∈ V
75		ovex 7168	. . . . 5 ⊢ (𝐵 ↑_m (𝑁 × 𝑃)) ∈ V
76	74, 75	mpoex 7760	. . . 4 ⊢ (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V
77	76	a1i 11	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V)
78	3, 69, 71, 73, 77	ovmpod 7281	. 2 ⊢ (𝜑 → (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩) = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
79	1, 78	syl5eq 2845	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 Vcvv 3441 ⦋csb 3828 ⟨cotp 4533 ↦ cmpt 5110 × cxp 5517 ‘cfv 6324 (class class class)co 7135 ∈ cmpo 7137 1^st c1st 7669 2^nd c2nd 7670 ↑_m cmap 8389 Fincfn 8492 Basecbs 16475 ._rcmulr 16558 Σ_g cgsu 16706 maMul cmmul 20990

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-ot 4534 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-1st 7671 df-2nd 7672 df-mamu 20991

This theorem is referenced by: mamuval 20993 mamudm 20995

W3C validator