matbas2d

Description: The base set of the matrix ring as a mapping operation. (Contributed by Stefan O'Rear, 11-Jul-2018)

	Ref	Expression
Hypotheses	matbas2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matbas2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	matbas2i.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	matbas2d.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	matbas2d.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	matbas2d.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝐶 ∈ 𝐾 )
Assertion	matbas2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		matbas2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matbas2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		matbas2i.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		matbas2d.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
5		matbas2d.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
6		matbas2d.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝐶 ∈ 𝐾 )
7	6	3expb	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝐶 ∈ 𝐾 )
8	7	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 𝐶 ∈ 𝐾 )
9		eqid	⊢ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 )
10	9	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 𝐶 ∈ 𝐾 ↔ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
11	8 10	sylib	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
12	1 2	matbas2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝐾 ↑_m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
13	4 5 12	syl2anc	⊢ ( 𝜑 → ( 𝐾 ↑_m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
14	3 13	eqtr4id	⊢ ( 𝜑 → 𝐵 = ( 𝐾 ↑_m ( 𝑁 × 𝑁 ) ) )
15	14	eleq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) ∈ 𝐵 ↔ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) ∈ ( 𝐾 ↑_m ( 𝑁 × 𝑁 ) ) ) )
16	2	fvexi	⊢ 𝐾 ∈ V
17	4 4	xpexd	⊢ ( 𝜑 → ( 𝑁 × 𝑁 ) ∈ V )
18		elmapg	⊢ ( ( 𝐾 ∈ V ∧ ( 𝑁 × 𝑁 ) ∈ V ) → ( ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) ∈ ( 𝐾 ↑_m ( 𝑁 × 𝑁 ) ) ↔ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 ) )
19	16 17 18	sylancr	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) ∈ ( 𝐾 ↑_m ( 𝑁 × 𝑁 ) ) ↔ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 ) )
20	15 19	bitrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) ∈ 𝐵 ↔ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 ) )
21	11 20	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 𝐶 ) ∈ 𝐵 )

Metamath Proof Explorer

Theorem matbas2d

Proof