mamufval

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

	Ref	Expression
Hypotheses	mamufval.f	⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
	mamufval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mamufval.t	⊢ · = ( ._r ‘ 𝑅 )
	mamufval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	mamufval.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
	mamufval.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mamufval.p	⊢ ( 𝜑 → 𝑃 ∈ Fin )
Assertion	mamufval	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑃 ) ) ↦ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem mamufval

Proof