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 22734

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 22733	. . . 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 6918	. . . . 5 ⊢ (1^st ‘(1^st ‘𝑜)) ∈ V
5		fvex 6918	. . . . 5 ⊢ (2^nd ‘(1^st ‘𝑜)) ∈ V
6		fvex 6918	. . . . . . 7 ⊢ (2^nd ‘𝑜) ∈ V
7		eqidd 2764	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_m (𝑚 × 𝑛)))
8		xpeq2 5676	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑛 × 𝑝) = (𝑛 × (2^nd ‘𝑜)))
9	8	oveq2d 7456	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) = ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))))
10		eqidd 2764	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑚 = 𝑚)
11		id 23	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → 𝑝 = (2^nd ‘𝑜))
12		eqidd 2764	. . . . . . . . 9 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
13	10, 11, 12	mpoeq123dv 7515	. . . . . . . 8 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
14	7, 9, 13	mpoeq123dv 7515	. . . . . . 7 ⊢ (𝑝 = (2^nd ‘𝑜) → (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))))
15	6, 14	csbie 3886	. . . . . 6 ⊢ ⦋(2^nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑_m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))))
16		xpeq12 5680	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑚 × 𝑛) = ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))))
17	16	oveq2d 7456	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((Base‘𝑟) ↑_m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))))
18		simpr 490	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑛 = (2^nd ‘(1^st ‘𝑜)))
19	18	xpeq1d 5684	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑛 × (2^nd ‘𝑜)) = ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)))
20	19	oveq2d 7456	. . . . . . 7 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((Base‘𝑟) ↑_m (𝑛 × (2^nd ‘𝑜))) = ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))))
21		id 23	. . . . . . . . 9 ⊢ (𝑚 = (1^st ‘(1^st ‘𝑜)) → 𝑚 = (1^st ‘(1^st ‘𝑜)))
22	21	adantr 486	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → 𝑚 = (1^st ‘(1^st ‘𝑜)))
23		eqidd 2764	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (2^nd ‘𝑜) = (2^nd ‘𝑜))
24		eqidd 2764	. . . . . . . . . 10 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))
25	18, 24	mpteq12dv 5195	. . . . . . . . 9 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))
26	25	oveq2d 7456	. . . . . . . 8 ⊢ ((𝑚 = (1^st ‘(1^st ‘𝑜)) ∧ 𝑛 = (2^nd ‘(1^st ‘𝑜))) → (𝑟 Σ_g (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))))
27	22, 23, 26	mpoeq123dv 7515	. . . . . . 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 7515	. . . . . 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 2810	. . . . 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 3890	. . . 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 783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → 𝑟 = 𝑅)
32	31	fveq2d 6909	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = (Base‘𝑅))
33		mamufval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
34	32, 33	eqtr4di 2816	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (Base‘𝑟) = 𝐵)
35		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘𝑜) = (1^st ‘⟨𝑀, 𝑁, 𝑃⟩))
36	35	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (1^st ‘(1^st ‘𝑜)) = (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
37	36	ad2antll 742	. . . . . . . 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 8036	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
42	38, 39, 40, 41	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
43	42	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑀)
44	37, 43	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (1^st ‘(1^st ‘𝑜)) = 𝑀)
45	35	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
46	45	ad2antll 742	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)))
47		ot2ndg 8037	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
48	38, 39, 40, 47	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
49	48	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘⟨𝑀, 𝑁, 𝑃⟩)) = 𝑁)
50	46, 49	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘(1^st ‘𝑜)) = 𝑁)
51	44, 50	xpeq12d 5686	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜))) = (𝑀 × 𝑁))
52	34, 51	oveq12d 7458	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_m ((1^st ‘(1^st ‘𝑜)) × (2^nd ‘(1^st ‘𝑜)))) = (𝐵 ↑_m (𝑀 × 𝑁)))
53		fveq2 6905	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑀, 𝑁, 𝑃⟩ → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
54	53	ad2antll 742	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩))
55		ot3rdg 8038	. . . . . . . . . 10 ⊢ (𝑃 ∈ Fin → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
56	40, 55	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
57	56	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘⟨𝑀, 𝑁, 𝑃⟩) = 𝑃)
58	54, 57	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (2^nd ‘𝑜) = 𝑃)
59	50, 58	xpeq12d 5686	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜)) = (𝑁 × 𝑃))
60	34, 59	oveq12d 7458	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((Base‘𝑟) ↑_m ((2^nd ‘(1^st ‘𝑜)) × (2^nd ‘𝑜))) = (𝐵 ↑_m (𝑁 × 𝑃)))
61	31	fveq2d 6909	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = (._r‘𝑅))
62		mamufval.t	. . . . . . . . . 10 ⊢ · = (._r‘𝑅)
63	61, 62	eqtr4di 2816	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (._r‘𝑟) = · )
64	63	oveqd 7457	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))
65	50, 64	mpteq12dv 5195	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))
66	31, 65	oveq12d 7458	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘)))) = (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))
67	44, 58, 66	mpoeq123dv 7515	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = ⟨𝑀, 𝑁, 𝑃⟩)) → (𝑖 ∈ (1^st ‘(1^st ‘𝑜)), 𝑘 ∈ (2^nd ‘𝑜) ↦ (𝑟 Σ_g (𝑗 ∈ (2^nd ‘(1^st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(._r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))
68	52, 60, 67	mpoeq123dv 7515	. . . 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 2810	. . 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 3477	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
72		otex 5438	. . . 4 ⊢ ⟨𝑀, 𝑁, 𝑃⟩ ∈ V
73	72	a1i 11	. . 3 ⊢ (𝜑 → ⟨𝑀, 𝑁, 𝑃⟩ ∈ V)
74		ovex 7473	. . . . 5 ⊢ (𝐵 ↑_m (𝑀 × 𝑁)) ∈ V
75		ovex 7473	. . . . 5 ⊢ (𝐵 ↑_m (𝑁 × 𝑃)) ∈ V
76	74, 75	mpoex 8114	. . . 4 ⊢ (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V
77	76	a1i 11	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V)
78	3, 69, 71, 73, 77	ovmpod 7593	. 2 ⊢ (𝜑 → (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩) = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
79	1, 78	eqtrid 2810	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑_m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑_m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 Vcvv 3454 ⦋csb 3851 ⟨cotp 4861 ↦ cmpt 5189 × cxp 5653 ‘cfv 6555 (class class class)co 7440 ∈ cmpo 7442 1^st c1st 8020 2^nd c2nd 8021 ↑_m cmap 8872 Fincfn 8998 Basecbs 17413 ._rcmulr 17455 Σ_g cgsu 17637 maMul cmmul 22732

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-ot 4862 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-ov 7443 df-oprab 7444 df-mpo 7445 df-1st 8022 df-2nd 8023 df-mamu 22733

This theorem is used by: mamuval 22735 mamudm 22737

W3C validator