Theorem veronesematbasd

Description: The matrix whose i -th row is the Veronese image of Ai belongs to the base set of ( 1 ... 6 ) Mat RRfld . (Contributed by Jiamin Zhao, 19-Aug-2026)

	Ref	Expression
Hypotheses	veronesemat.a	No typesetting found for |- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) with typecode |-
	veronesemat.f	$$⊢\phi \to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
Assertion	veronesematbasd	$$⊢\phi \to V\in {\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$

Proof

Step	Hyp	Ref	Expression
1		veronesemat.a	Could not format V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) : No typesetting found for |- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) with typecode |-
2		veronesemat.f	$$⊢\phi \to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
3		2fveq3	Could not format ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) ) : No typesetting found for |- ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) ) with typecode |-
4	3	fveq1d	Could not format ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) ) : No typesetting found for |- ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) ) with typecode |-
5		fveq2	Could not format ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
6	4 5	cbvmpov	Could not format ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
7	1 6	eqtri	Could not format V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
8	7	a1i	Could not format ( ph -> V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) : No typesetting found for |- ( ph -> V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) with typecode |-
9	2	adantr	$$⊢\left(\phi \wedge \left(u\in \left(1\dots 6\right)\wedge v\in \left(1\dots 6\right)\right)\right)\to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
10		simprl	$$⊢\left(\phi \wedge \left(u\in \left(1\dots 6\right)\wedge v\in \left(1\dots 6\right)\right)\right)\to u\in \left(1\dots 6\right)$$
11	9 10	ffvelcdmd	$$⊢\left(\phi \wedge \left(u\in \left(1\dots 6\right)\wedge v\in \left(1\dots 6\right)\right)\right)\to A\left(u\right)\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
12		simprr	$$⊢\left(\phi \wedge \left(u\in \left(1\dots 6\right)\wedge v\in \left(1\dots 6\right)\right)\right)\to v\in \left(1\dots 6\right)$$
13		veronesefvcl	Could not format ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) : No typesetting found for |- ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) with typecode |-
14	11 12 13	syl2anc	Could not format ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) : No typesetting found for |- ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) with typecode |-
15	8 14	fmpod	$$⊢\phi \to V:\left(1\dots 6\right)\times \left(1\dots 6\right)⟶ℝ$$
16		reex	$$⊢ℝ\in \mathrm{V}$$
17		ovex	$$⊢\left(1\dots 6\right)\in \mathrm{V}$$
18		sqxpexg	$$⊢\left(1\dots 6\right)\in \mathrm{V}\to \left(1\dots 6\right)\times \left(1\dots 6\right)\in \mathrm{V}$$
19	17 18	ax-mp	$$⊢\left(1\dots 6\right)\times \left(1\dots 6\right)\in \mathrm{V}$$
20	16 19	elmap	$$⊢V\in \left({ℝ}^{\left(\left(1\dots 6\right)\times \left(1\dots 6\right)\right)}\right)\leftrightarrow V:\left(1\dots 6\right)\times \left(1\dots 6\right)⟶ℝ$$
21	15 20	sylibr	$$⊢\phi \to V\in \left({ℝ}^{\left(\left(1\dots 6\right)\times \left(1\dots 6\right)\right)}\right)$$
22		fzfi	$$⊢\left(1\dots 6\right)\in \mathrm{Fin}$$
23		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
24	23	elexi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{V}$$
25		eqid	$$⊢\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}=\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}$$
26		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
27	25 26	matbas2	$$⊢\left(\left(1\dots 6\right)\in \mathrm{Fin}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{V}\right)\to {ℝ}^{\left(\left(1\dots 6\right)\times \left(1\dots 6\right)\right)}={\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$
28	22 24 27	mp2an	$$⊢{ℝ}^{\left(\left(1\dots 6\right)\times \left(1\dots 6\right)\right)}={\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$
29	21 28	eleqtrdi	$$⊢\phi \to V\in {\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$