mamures

Description: Rows in a matrix product are functions only of the corresponding rows in the left argument. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	mamures.f	⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
	mamures.g	⊢ 𝐺 = ( 𝑅 maMul ⟨ 𝐼 , 𝑁 , 𝑃 ⟩ )
	mamures.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mamures.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	mamures.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
	mamures.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mamures.p	⊢ ( 𝜑 → 𝑃 ∈ Fin )
	mamures.i	⊢ ( 𝜑 → 𝐼 ⊆ 𝑀 )
	mamures.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) )
	mamures.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑃 ) ) )
Assertion	mamures	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ↾ ( 𝐼 × 𝑃 ) ) = ( ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝐺 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		mamures.f	⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
2		mamures.g	⊢ 𝐺 = ( 𝑅 maMul ⟨ 𝐼 , 𝑁 , 𝑃 ⟩ )
3		mamures.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		mamures.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
5		mamures.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
6		mamures.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		mamures.p	⊢ ( 𝜑 → 𝑃 ∈ Fin )
8		mamures.i	⊢ ( 𝜑 → 𝐼 ⊆ 𝑀 )
9		mamures.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) )
10		mamures.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑃 ) ) )
11		ssidd	⊢ ( 𝜑 → 𝑃 ⊆ 𝑃 )
12		resmpo	⊢ ( ( 𝐼 ⊆ 𝑀 ∧ 𝑃 ⊆ 𝑃 ) → ( ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) ↾ ( 𝐼 × 𝑃 ) ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) )
13	8 11 12	syl2anc	⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) ↾ ( 𝐼 × 𝑃 ) ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) )
14		ovres	⊢ ( ( 𝑖 ∈ 𝐼 ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) = ( 𝑖 𝑋 𝑘 ) )
15	14	3ad2antl2	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) = ( 𝑖 𝑋 𝑘 ) )
16	15	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑘 ) = ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) )
17	16	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) = ( ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) )
18	17	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃 ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) )
19	18	oveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃 ) → ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) )
20	19	mpoeq3dva	⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) )
21	13 20	eqtrd	⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) ↾ ( 𝐼 × 𝑃 ) ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) )
22		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
23	1 3 22 4 5 6 7 9 10	mamuval	⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) )
24	23	reseq1d	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ↾ ( 𝐼 × 𝑃 ) ) = ( ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) ↾ ( 𝐼 × 𝑃 ) ) )
25	5 8	ssfid	⊢ ( 𝜑 → 𝐼 ∈ Fin )
26		elmapi	⊢ ( 𝑋 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
27	9 26	syl	⊢ ( 𝜑 → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
28		xpss1	⊢ ( 𝐼 ⊆ 𝑀 → ( 𝐼 × 𝑁 ) ⊆ ( 𝑀 × 𝑁 ) )
29	8 28	syl	⊢ ( 𝜑 → ( 𝐼 × 𝑁 ) ⊆ ( 𝑀 × 𝑁 ) )
30	27 29	fssresd	⊢ ( 𝜑 → ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) : ( 𝐼 × 𝑁 ) ⟶ 𝐵 )
31	3	fvexi	⊢ 𝐵 ∈ V
32	31	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
33		xpfi	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝐼 × 𝑁 ) ∈ Fin )
34	25 6 33	syl2anc	⊢ ( 𝜑 → ( 𝐼 × 𝑁 ) ∈ Fin )
35	32 34	elmapd	⊢ ( 𝜑 → ( ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) ∈ ( 𝐵 ↑_m ( 𝐼 × 𝑁 ) ) ↔ ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) : ( 𝐼 × 𝑁 ) ⟶ 𝐵 ) )
36	30 35	mpbird	⊢ ( 𝜑 → ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) ∈ ( 𝐵 ↑_m ( 𝐼 × 𝑁 ) ) )
37	2 3 22 4 25 6 7 36 10	mamuval	⊢ ( 𝜑 → ( ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝐺 𝑌 ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝑃 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝑘 ) ( ._r ‘ 𝑅 ) ( 𝑘 𝑌 𝑗 ) ) ) ) ) )
38	21 24 37	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ↾ ( 𝐼 × 𝑃 ) ) = ( ( 𝑋 ↾ ( 𝐼 × 𝑁 ) ) 𝐺 𝑌 ) )

Metamath Proof Explorer

Theorem mamures

Proof