marepvfval

Description: First substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019) (Revised by AV, 26-Feb-2019) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Hypotheses	marepvfval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	marepvfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	marepvfval.q	⊢ 𝑄 = ( 𝑁 matRepV 𝑅 )
	marepvfval.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑_m 𝑁 )
Assertion	marepvfval	⊢ 𝑄 = ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		marepvfval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		marepvfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		marepvfval.q	⊢ 𝑄 = ( 𝑁 matRepV 𝑅 )
4		marepvfval.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑_m 𝑁 )
5	2	fvexi	⊢ 𝐵 ∈ V
6	4	ovexi	⊢ 𝑉 ∈ V
7	6	a1i	⊢ ( ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → 𝑉 ∈ V )
8		mpoexga	⊢ ( ( 𝐵 ∈ V ∧ 𝑉 ∈ V ) → ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) ∈ V )
9	5 7 8	sylancr	⊢ ( ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) ∈ V )
10		oveq12	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
11	10 1	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = 𝐴 )
12	11	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ 𝐴 ) )
13	12 2	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = 𝐵 )
14		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
15	14	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
16		simpl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
17	15 16	oveq12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) = ( ( Base ‘ 𝑅 ) ↑_m 𝑁 ) )
18	17 4	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) = 𝑉 )
19		eqidd	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) = if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) )
20	16 16 19	mpoeq123dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) )
21	16 20	mpteq12dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑘 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
22	13 18 21	mpoeq123dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) ↦ ( 𝑘 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) = ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
23		df-marepv	⊢ matRepV = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑟 ) ↑_m 𝑛 ) ↦ ( 𝑘 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
24	22 23	ovmpoga	⊢ ( ( 𝑁 ∈ V ∧ 𝑅 ∈ V ∧ ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) ∈ V ) → ( 𝑁 matRepV 𝑅 ) = ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
25	9 24	mpd3an3	⊢ ( ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 matRepV 𝑅 ) = ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
26	23	mpondm0	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 matRepV 𝑅 ) = ∅ )
27	1	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
28	2 27	eqtri	⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
29		matbas0pc	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )
30	28 29	syl5eq	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
31	30	orcd	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐵 = ∅ ∨ 𝑉 = ∅ ) )
32		0mpo0	⊢ ( ( 𝐵 = ∅ ∨ 𝑉 = ∅ ) → ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) = ∅ )
33	31 32	syl	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) = ∅ )
34	26 33	eqtr4d	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 matRepV 𝑅 ) = ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
35	25 34	pm2.61i	⊢ ( 𝑁 matRepV 𝑅 ) = ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
36	3 35	eqtri	⊢ 𝑄 = ( 𝑚 ∈ 𝐵 , 𝑣 ∈ 𝑉 ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )

Metamath Proof Explorer

Theorem marepvfval

Proof