Metamath Proof Explorer

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 
|- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) )
veronesemat.f 
|- ( ph -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
Assertion veronesematbasd 
|- ( ph -> V e. ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) )

Proof

Step Hyp Ref Expression
1 veronesemat.a 
 |-  V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) )
2 veronesemat.f 
 |-  ( ph -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
3 2fveq3 
 |-  ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) )
4 3 fveq1d 
 |-  ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) )
5 fveq2 
 |-  ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) )
6 4 5 cbvmpov 
 |-  ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
7 1 6 eqtri 
 |-  V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
8 7 a1i 
 |-  ( ph -> V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) )
9 2 adantr 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
10 simprl 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> u e. ( 1 ... 6 ) )
11 9 10 ffvelcdmd 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) )
12 simprr 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> v e. ( 1 ... 6 ) )
13 veronesefvcl 
 |-  ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
14 11 12 13 syl2anc 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
15 8 14 fmpod 
 |-  ( ph -> V : ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) --> RR )
16 reex 
 |-  RR e. _V
17 ovex 
 |-  ( 1 ... 6 ) e. _V
18 sqxpexg 
 |-  ( ( 1 ... 6 ) e. _V -> ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) e. _V )
19 17 18 ax-mp 
 |-  ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) e. _V
20 16 19 elmap 
 |-  ( V e. ( RR ^m ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) ) <-> V : ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) --> RR )
21 15 20 sylibr 
 |-  ( ph -> V e. ( RR ^m ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) ) )
22 fzfi 
 |-  ( 1 ... 6 ) e. Fin
23 refld 
 |-  RRfld e. Field
24 23 elexi 
 |-  RRfld e. _V
25 eqid 
 |-  ( ( 1 ... 6 ) Mat RRfld ) = ( ( 1 ... 6 ) Mat RRfld )
26 rebase 
 |-  RR = ( Base ` RRfld )
27 25 26 matbas2 
 |-  ( ( ( 1 ... 6 ) e. Fin /\ RRfld e. _V ) -> ( RR ^m ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) ) = ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) )
28 22 24 27 mp2an 
 |-  ( RR ^m ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) ) = ( Base ` ( ( 1 ... 6 ) Mat RRfld ) )
29 21 28 eleqtrdi 
 |-  ( ph -> V e. ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) )