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 ⊢ 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) )
veronesemat.f ⊢ ( 𝜑 → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
Assertion veronesematbasd ( 𝜑 → 𝑉 ∈ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) )

Proof

Step Hyp Ref Expression
1 veronesemat.a ⊢ 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) )
2 veronesemat.f ⊢ ( 𝜑 → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
3 2fveq3 ⊢ ( 𝑖 = 𝑢 → ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) )
4 3 fveq1d ⊢ ( 𝑖 = 𝑢 → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) )
5 fveq2 ⊢ ( 𝑗 = 𝑣 → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
6 4 5 cbvmpov ⊢ ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) ) = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
7 1 6 eqtri ⊢ 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
8 7 a1i ⊢ ( 𝜑 → 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
9 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
10 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → 𝑢 ∈ ( 1 ... 6 ) )
11 9 10 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
12 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → 𝑣 ∈ ( 1 ... 6 ) )
13 veronesefvcl ⊢ ( ( ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
14 11 12 13 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
15 8 14 fmpod ⊢ ( 𝜑 → 𝑉 : ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ⟶ ℝ )
16 reex ⊢ ℝ ∈ V
17 ovex ⊢ ( 1 ... 6 ) ∈ V
18 sqxpexg ⊢ ( ( 1 ... 6 ) ∈ V → ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ∈ V )
19 17 18 ax-mp ⊢ ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ∈ V
20 16 19 elmap ⊢ ( 𝑉 ∈ ( ℝ ↑m ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ) ↔ 𝑉 : ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ⟶ ℝ )
21 15 20 sylibr ⊢ ( 𝜑 → 𝑉 ∈ ( ℝ ↑m ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ) )
22 fzfi ⊢ ( 1 ... 6 ) ∈ Fin
23 refld ⊢ ℝfld ∈ Field
24 23 elexi ⊢ ℝfld ∈ V
25 eqid ⊢ ( ( 1 ... 6 ) Mat ℝfld ) = ( ( 1 ... 6 ) Mat ℝfld )
26 rebase ⊢ ℝ = ( Base ‘ ℝfld )
27 25 26 matbas2 ⊢ ( ( ( 1 ... 6 ) ∈ Fin ∧ ℝfld ∈ V ) → ( ℝ ↑m ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ) = ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) )
28 22 24 27 mp2an ⊢ ( ℝ ↑m ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ) = ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) )
29 21 28 eleqtrdi ⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) )