Theorem lmatval

Description: Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020)

	Ref	Expression
Assertion	lmatval	⊢ ( 𝑀 ∈ 𝑉 → ( litMat ‘ 𝑀 ) = ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑀 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑀 ‘ 0 ) ) ) ↦ ( ( 𝑀 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
2		fveq2	⊢ ( 𝑚 = 𝑀 → ( ♯ ‘ 𝑚 ) = ( ♯ ‘ 𝑀 ) )
3	2	oveq2d	⊢ ( 𝑚 = 𝑀 → ( 1 ... ( ♯ ‘ 𝑚 ) ) = ( 1 ... ( ♯ ‘ 𝑀 ) ) )
4		fveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ 0 ) = ( 𝑀 ‘ 0 ) )
5	4	fveq2d	⊢ ( 𝑚 = 𝑀 → ( ♯ ‘ ( 𝑚 ‘ 0 ) ) = ( ♯ ‘ ( 𝑀 ‘ 0 ) ) )
6	5	oveq2d	⊢ ( 𝑚 = 𝑀 → ( 1 ... ( ♯ ‘ ( 𝑚 ‘ 0 ) ) ) = ( 1 ... ( ♯ ‘ ( 𝑀 ‘ 0 ) ) ) )
7		fveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ( 𝑖 − 1 ) ) = ( 𝑀 ‘ ( 𝑖 − 1 ) ) )
8	7	fveq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑀 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) )
9	3 6 8	mpoeq123dv	⊢ ( 𝑚 = 𝑀 → ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑚 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑚 ‘ 0 ) ) ) ↦ ( ( 𝑚 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) = ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑀 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑀 ‘ 0 ) ) ) ↦ ( ( 𝑀 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
10		df-lmat	⊢ litMat = ( 𝑚 ∈ V ↦ ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑚 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑚 ‘ 0 ) ) ) ↦ ( ( 𝑚 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
11		ovex	⊢ ( 1 ... ( ♯ ‘ 𝑀 ) ) ∈ V
12		ovex	⊢ ( 1 ... ( ♯ ‘ ( 𝑀 ‘ 0 ) ) ) ∈ V
13	11 12	mpoex	⊢ ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑀 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑀 ‘ 0 ) ) ) ↦ ( ( 𝑀 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) ∈ V
14	9 10 13	fvmpt	⊢ ( 𝑀 ∈ V → ( litMat ‘ 𝑀 ) = ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑀 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑀 ‘ 0 ) ) ) ↦ ( ( 𝑀 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
15	1 14	syl	⊢ ( 𝑀 ∈ 𝑉 → ( litMat ‘ 𝑀 ) = ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑀 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑀 ‘ 0 ) ) ) ↦ ( ( 𝑀 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )