| Step |
Hyp |
Ref |
Expression |
| 1 |
|
veroquad.a |
⊢ 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) ) |
| 2 |
|
veroquad.f |
⊢ ( 𝜑 → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) ) |
| 3 |
|
veroquad.k |
⊢ ( 𝜑 → 𝐾 : ( 1 ... 6 ) ⟶ ℝ ) |
| 4 |
|
veroquad.q |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) = 0 ) |
| 5 |
|
rebase |
⊢ ℝ = ( Base ‘ ℝfld ) |
| 6 |
|
replusg |
⊢ + = ( +g ‘ ℝfld ) |
| 7 |
|
refld |
⊢ ℝfld ∈ Field |
| 8 |
7
|
elexi |
⊢ ℝfld ∈ V |
| 9 |
8
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ℝfld ∈ V ) |
| 10 |
|
6nn |
⊢ 6 ∈ ℕ |
| 11 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
| 12 |
10 11
|
eleqtri |
⊢ 6 ∈ ( ℤ≥ ‘ 1 ) |
| 13 |
12
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → 6 ∈ ( ℤ≥ ‘ 1 ) ) |
| 14 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → 𝐾 : ( 1 ... 6 ) ⟶ ℝ ) |
| 15 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → 𝑣 ∈ ( 1 ... 6 ) ) |
| 16 |
14 15
|
ffvelcdmd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 𝑣 ) ∈ ℝ ) |
| 17 |
1 2
|
veronesematrowd |
⊢ ( 𝜑 → curry 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) ) |
| 18 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ∈ V ) |
| 19 |
17 18
|
fvmpt2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( curry 𝑉 ‘ 𝑖 ) = ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) |
| 20 |
19
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( curry 𝑉 ‘ 𝑖 ) = ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) |
| 21 |
20
|
fveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑣 ) ) |
| 22 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) ) |
| 23 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → 𝑖 ∈ ( 1 ... 6 ) ) |
| 24 |
22 23
|
ffvelcdmd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) |
| 25 |
|
veronesefvcl |
⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑣 ) ∈ ℝ ) |
| 26 |
24 25
|
sylancom |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑣 ) ∈ ℝ ) |
| 27 |
21 26
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ∈ ℝ ) |
| 28 |
16 27
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ∈ ℝ ) |
| 29 |
28
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) : ( 1 ... 6 ) ⟶ ℝ ) |
| 30 |
5 6 9 13 29
|
gsumval2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ℝfld Σg ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) = ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 6 ) ) |
| 31 |
|
5nn |
⊢ 5 ∈ ℕ |
| 32 |
31 11
|
eleqtri |
⊢ 5 ∈ ( ℤ≥ ‘ 1 ) |
| 33 |
|
seqp1 |
⊢ ( 5 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 5 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 5 + 1 ) ) ) ) |
| 34 |
32 33
|
ax-mp |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 5 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 5 + 1 ) ) ) |
| 35 |
|
5p1e6 |
⊢ ( 5 + 1 ) = 6 |
| 36 |
35
|
fveq2i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 5 + 1 ) ) = ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 6 ) |
| 37 |
35
|
fveq2i |
⊢ ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 5 + 1 ) ) = ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 6 ) |
| 38 |
37
|
oveq2i |
⊢ ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 5 + 1 ) ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 6 ) ) |
| 39 |
34 36 38
|
3eqtr3i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 6 ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 6 ) ) |
| 40 |
|
4nn |
⊢ 4 ∈ ℕ |
| 41 |
40 11
|
eleqtri |
⊢ 4 ∈ ( ℤ≥ ‘ 1 ) |
| 42 |
|
seqp1 |
⊢ ( 4 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 4 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 4 + 1 ) ) ) ) |
| 43 |
41 42
|
ax-mp |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 4 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 4 + 1 ) ) ) |
| 44 |
|
4p1e5 |
⊢ ( 4 + 1 ) = 5 |
| 45 |
44
|
fveq2i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 4 + 1 ) ) = ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) |
| 46 |
44
|
fveq2i |
⊢ ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 4 + 1 ) ) = ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 5 ) |
| 47 |
46
|
oveq2i |
⊢ ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 4 + 1 ) ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 5 ) ) |
| 48 |
43 45 47
|
3eqtr3i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 5 ) ) |
| 49 |
|
3nn |
⊢ 3 ∈ ℕ |
| 50 |
49 11
|
eleqtri |
⊢ 3 ∈ ( ℤ≥ ‘ 1 ) |
| 51 |
|
seqp1 |
⊢ ( 3 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 3 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 3 + 1 ) ) ) ) |
| 52 |
50 51
|
ax-mp |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 3 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 3 + 1 ) ) ) |
| 53 |
|
3p1e4 |
⊢ ( 3 + 1 ) = 4 |
| 54 |
53
|
fveq2i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 3 + 1 ) ) = ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) |
| 55 |
53
|
fveq2i |
⊢ ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 3 + 1 ) ) = ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 4 ) |
| 56 |
55
|
oveq2i |
⊢ ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 3 + 1 ) ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 4 ) ) |
| 57 |
52 54 56
|
3eqtr3i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 4 ) ) |
| 58 |
|
2eluzge1 |
⊢ 2 ∈ ( ℤ≥ ‘ 1 ) |
| 59 |
|
seqp1 |
⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 2 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 2 + 1 ) ) ) ) |
| 60 |
58 59
|
ax-mp |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 2 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 2 + 1 ) ) ) |
| 61 |
|
2p1e3 |
⊢ ( 2 + 1 ) = 3 |
| 62 |
61
|
fveq2i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 2 + 1 ) ) = ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) |
| 63 |
61
|
fveq2i |
⊢ ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 2 + 1 ) ) = ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 3 ) |
| 64 |
63
|
oveq2i |
⊢ ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 2 + 1 ) ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 3 ) ) |
| 65 |
60 62 64
|
3eqtr3i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 3 ) ) |
| 66 |
|
1nn |
⊢ 1 ∈ ℕ |
| 67 |
66 11
|
eleqtri |
⊢ 1 ∈ ( ℤ≥ ‘ 1 ) |
| 68 |
|
seqp1 |
⊢ ( 1 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 1 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 1 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 1 + 1 ) ) ) ) |
| 69 |
67 68
|
ax-mp |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 1 + 1 ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 1 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 1 + 1 ) ) ) |
| 70 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
| 71 |
70
|
fveq2i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ ( 1 + 1 ) ) = ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) |
| 72 |
70
|
fveq2i |
⊢ ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 1 + 1 ) ) = ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 2 ) |
| 73 |
72
|
oveq2i |
⊢ ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 1 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ ( 1 + 1 ) ) ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 1 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 2 ) ) |
| 74 |
69 71 73
|
3eqtr3i |
⊢ ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) = ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 1 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 2 ) ) |
| 75 |
|
1z |
⊢ 1 ∈ ℤ |
| 76 |
|
eqid |
⊢ ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) = ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) |
| 77 |
|
fveq2 |
⊢ ( 𝑣 = 1 → ( 𝐾 ‘ 𝑣 ) = ( 𝐾 ‘ 1 ) ) |
| 78 |
|
fveq2 |
⊢ ( 𝑣 = 1 → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) = ( ( curry 𝑉 ‘ 𝑖 ) ‘ 1 ) ) |
| 79 |
77 78
|
oveq12d |
⊢ ( 𝑣 = 1 → ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) = ( ( 𝐾 ‘ 1 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 1 ) ) ) |
| 80 |
|
1re |
⊢ 1 ∈ ℝ |
| 81 |
|
6re |
⊢ 6 ∈ ℝ |
| 82 |
|
1lt6 |
⊢ 1 < 6 |
| 83 |
80 81 82
|
ltleii |
⊢ 1 ≤ 6 |
| 84 |
|
elfz1b |
⊢ ( 1 ∈ ( 1 ... 6 ) ↔ ( 1 ∈ ℕ ∧ 6 ∈ ℕ ∧ 1 ≤ 6 ) ) |
| 85 |
66 10 83 84
|
mpbir3an |
⊢ 1 ∈ ( 1 ... 6 ) |
| 86 |
85
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → 1 ∈ ( 1 ... 6 ) ) |
| 87 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 1 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 1 ) ) ∈ V ) |
| 88 |
76 79 86 87
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 1 ) = ( ( 𝐾 ‘ 1 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 1 ) ) ) |
| 89 |
19
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 1 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 1 ) ) |
| 90 |
2
|
ffvelcdmda |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) |
| 91 |
90
|
veronesev1lem |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 1 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) |
| 92 |
89 91
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 1 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) |
| 93 |
92
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 1 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 1 ) ) = ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) ) |
| 94 |
88 93
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 1 ) = ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) ) |
| 95 |
75 94
|
seq1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 1 ) = ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) ) |
| 96 |
|
fveq2 |
⊢ ( 𝑣 = 2 → ( 𝐾 ‘ 𝑣 ) = ( 𝐾 ‘ 2 ) ) |
| 97 |
|
fveq2 |
⊢ ( 𝑣 = 2 → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) = ( ( curry 𝑉 ‘ 𝑖 ) ‘ 2 ) ) |
| 98 |
96 97
|
oveq12d |
⊢ ( 𝑣 = 2 → ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) = ( ( 𝐾 ‘ 2 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 2 ) ) ) |
| 99 |
|
2nn |
⊢ 2 ∈ ℕ |
| 100 |
|
2re |
⊢ 2 ∈ ℝ |
| 101 |
|
2lt6 |
⊢ 2 < 6 |
| 102 |
100 81 101
|
ltleii |
⊢ 2 ≤ 6 |
| 103 |
|
elfz1b |
⊢ ( 2 ∈ ( 1 ... 6 ) ↔ ( 2 ∈ ℕ ∧ 6 ∈ ℕ ∧ 2 ≤ 6 ) ) |
| 104 |
99 10 102 103
|
mpbir3an |
⊢ 2 ∈ ( 1 ... 6 ) |
| 105 |
104
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → 2 ∈ ( 1 ... 6 ) ) |
| 106 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 2 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 2 ) ) ∈ V ) |
| 107 |
76 98 105 106
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 2 ) = ( ( 𝐾 ‘ 2 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 2 ) ) ) |
| 108 |
19
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 2 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 2 ) ) |
| 109 |
90
|
veronesev2lem |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 2 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) |
| 110 |
108 109
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 2 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) |
| 111 |
110
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 2 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 2 ) ) = ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) |
| 112 |
107 111
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 2 ) = ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) |
| 113 |
95 112
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 1 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 2 ) ) = ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) ) |
| 114 |
74 113
|
eqtrid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) = ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) ) |
| 115 |
|
fveq2 |
⊢ ( 𝑣 = 3 → ( 𝐾 ‘ 𝑣 ) = ( 𝐾 ‘ 3 ) ) |
| 116 |
|
fveq2 |
⊢ ( 𝑣 = 3 → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) = ( ( curry 𝑉 ‘ 𝑖 ) ‘ 3 ) ) |
| 117 |
115 116
|
oveq12d |
⊢ ( 𝑣 = 3 → ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) = ( ( 𝐾 ‘ 3 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 3 ) ) ) |
| 118 |
|
3re |
⊢ 3 ∈ ℝ |
| 119 |
|
3lt6 |
⊢ 3 < 6 |
| 120 |
118 81 119
|
ltleii |
⊢ 3 ≤ 6 |
| 121 |
|
elfz1b |
⊢ ( 3 ∈ ( 1 ... 6 ) ↔ ( 3 ∈ ℕ ∧ 6 ∈ ℕ ∧ 3 ≤ 6 ) ) |
| 122 |
49 10 120 121
|
mpbir3an |
⊢ 3 ∈ ( 1 ... 6 ) |
| 123 |
122
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → 3 ∈ ( 1 ... 6 ) ) |
| 124 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 3 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 3 ) ) ∈ V ) |
| 125 |
76 117 123 124
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 3 ) = ( ( 𝐾 ‘ 3 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 3 ) ) ) |
| 126 |
19
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 3 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 3 ) ) |
| 127 |
90
|
veronesev3lem |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 3 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) |
| 128 |
126 127
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 3 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) |
| 129 |
128
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 3 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 3 ) ) = ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) |
| 130 |
125 129
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 3 ) = ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) |
| 131 |
114 130
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 2 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 3 ) ) = ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) ) |
| 132 |
65 131
|
eqtrid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) = ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) ) |
| 133 |
|
fveq2 |
⊢ ( 𝑣 = 4 → ( 𝐾 ‘ 𝑣 ) = ( 𝐾 ‘ 4 ) ) |
| 134 |
|
fveq2 |
⊢ ( 𝑣 = 4 → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) = ( ( curry 𝑉 ‘ 𝑖 ) ‘ 4 ) ) |
| 135 |
133 134
|
oveq12d |
⊢ ( 𝑣 = 4 → ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) = ( ( 𝐾 ‘ 4 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 4 ) ) ) |
| 136 |
|
4re |
⊢ 4 ∈ ℝ |
| 137 |
|
4lt6 |
⊢ 4 < 6 |
| 138 |
136 81 137
|
ltleii |
⊢ 4 ≤ 6 |
| 139 |
|
elfz1b |
⊢ ( 4 ∈ ( 1 ... 6 ) ↔ ( 4 ∈ ℕ ∧ 6 ∈ ℕ ∧ 4 ≤ 6 ) ) |
| 140 |
40 10 138 139
|
mpbir3an |
⊢ 4 ∈ ( 1 ... 6 ) |
| 141 |
140
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → 4 ∈ ( 1 ... 6 ) ) |
| 142 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 4 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 4 ) ) ∈ V ) |
| 143 |
76 135 141 142
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 4 ) = ( ( 𝐾 ‘ 4 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 4 ) ) ) |
| 144 |
19
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 4 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 4 ) ) |
| 145 |
90
|
veronesev4lem |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 4 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) |
| 146 |
144 145
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 4 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) |
| 147 |
146
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 4 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 4 ) ) = ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) |
| 148 |
143 147
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 4 ) = ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) |
| 149 |
132 148
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 3 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 4 ) ) = ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) ) |
| 150 |
57 149
|
eqtrid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) = ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) ) |
| 151 |
|
fveq2 |
⊢ ( 𝑣 = 5 → ( 𝐾 ‘ 𝑣 ) = ( 𝐾 ‘ 5 ) ) |
| 152 |
|
fveq2 |
⊢ ( 𝑣 = 5 → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) = ( ( curry 𝑉 ‘ 𝑖 ) ‘ 5 ) ) |
| 153 |
151 152
|
oveq12d |
⊢ ( 𝑣 = 5 → ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) = ( ( 𝐾 ‘ 5 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 5 ) ) ) |
| 154 |
|
5re |
⊢ 5 ∈ ℝ |
| 155 |
|
5lt6 |
⊢ 5 < 6 |
| 156 |
154 81 155
|
ltleii |
⊢ 5 ≤ 6 |
| 157 |
|
elfz1b |
⊢ ( 5 ∈ ( 1 ... 6 ) ↔ ( 5 ∈ ℕ ∧ 6 ∈ ℕ ∧ 5 ≤ 6 ) ) |
| 158 |
31 10 156 157
|
mpbir3an |
⊢ 5 ∈ ( 1 ... 6 ) |
| 159 |
158
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → 5 ∈ ( 1 ... 6 ) ) |
| 160 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 5 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 5 ) ) ∈ V ) |
| 161 |
76 153 159 160
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 5 ) = ( ( 𝐾 ‘ 5 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 5 ) ) ) |
| 162 |
19
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 5 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 5 ) ) |
| 163 |
90
|
veronesev5lem |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 5 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) |
| 164 |
162 163
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 5 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) |
| 165 |
164
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 5 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 5 ) ) = ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) |
| 166 |
161 165
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 5 ) = ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) |
| 167 |
150 166
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 4 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 5 ) ) = ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) ) |
| 168 |
48 167
|
eqtrid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) = ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) ) |
| 169 |
|
fveq2 |
⊢ ( 𝑣 = 6 → ( 𝐾 ‘ 𝑣 ) = ( 𝐾 ‘ 6 ) ) |
| 170 |
|
fveq2 |
⊢ ( 𝑣 = 6 → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) = ( ( curry 𝑉 ‘ 𝑖 ) ‘ 6 ) ) |
| 171 |
169 170
|
oveq12d |
⊢ ( 𝑣 = 6 → ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) = ( ( 𝐾 ‘ 6 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 6 ) ) ) |
| 172 |
81
|
leidi |
⊢ 6 ≤ 6 |
| 173 |
|
elfz1b |
⊢ ( 6 ∈ ( 1 ... 6 ) ↔ ( 6 ∈ ℕ ∧ 6 ∈ ℕ ∧ 6 ≤ 6 ) ) |
| 174 |
10 10 172 173
|
mpbir3an |
⊢ 6 ∈ ( 1 ... 6 ) |
| 175 |
174
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → 6 ∈ ( 1 ... 6 ) ) |
| 176 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 6 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 6 ) ) ∈ V ) |
| 177 |
76 171 175 176
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 6 ) = ( ( 𝐾 ‘ 6 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 6 ) ) ) |
| 178 |
19
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 6 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 6 ) ) |
| 179 |
90
|
veronesev6lem |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 6 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) |
| 180 |
178 179
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 6 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) |
| 181 |
180
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 6 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 6 ) ) = ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) |
| 182 |
177 181
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 6 ) = ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) |
| 183 |
168 182
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 5 ) + ( ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ‘ 6 ) ) = ( ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) |
| 184 |
39 183
|
eqtrid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( seq 1 ( + , ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) ‘ 6 ) = ( ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) |
| 185 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → 𝐾 : ( 1 ... 6 ) ⟶ ℝ ) |
| 186 |
185 86
|
ffvelcdmd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 1 ) ∈ ℝ ) |
| 187 |
90
|
rr3fv1cld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ∈ ℝ ) |
| 188 |
187
|
resqcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ∈ ℝ ) |
| 189 |
186 188
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) ∈ ℝ ) |
| 190 |
189
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) ∈ ℂ ) |
| 191 |
185 105
|
ffvelcdmd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 2 ) ∈ ℝ ) |
| 192 |
90
|
rr3fv2cld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ∈ ℝ ) |
| 193 |
192
|
resqcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ∈ ℝ ) |
| 194 |
191 193
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ∈ ℝ ) |
| 195 |
194
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ∈ ℂ ) |
| 196 |
190 195
|
addcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) ∈ ℂ ) |
| 197 |
185 123
|
ffvelcdmd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 3 ) ∈ ℝ ) |
| 198 |
90
|
rr3fv3cld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ∈ ℝ ) |
| 199 |
198
|
resqcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ∈ ℝ ) |
| 200 |
197 199
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ∈ ℝ ) |
| 201 |
200
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ∈ ℂ ) |
| 202 |
196 201
|
addcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) ∈ ℂ ) |
| 203 |
185 141
|
ffvelcdmd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 4 ) ∈ ℝ ) |
| 204 |
187 192
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ∈ ℝ ) |
| 205 |
203 204
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ∈ ℝ ) |
| 206 |
205
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ∈ ℂ ) |
| 207 |
185 159
|
ffvelcdmd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 5 ) ∈ ℝ ) |
| 208 |
192 198
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ∈ ℝ ) |
| 209 |
207 208
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ∈ ℝ ) |
| 210 |
209
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ∈ ℂ ) |
| 211 |
202 206 210
|
addassd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) = ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) ) ) |
| 212 |
211
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) = ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) |
| 213 |
206 210
|
addcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) ∈ ℂ ) |
| 214 |
185 175
|
ffvelcdmd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 6 ) ∈ ℝ ) |
| 215 |
198 187
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ∈ ℝ ) |
| 216 |
214 215
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ∈ ℝ ) |
| 217 |
216
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ∈ ℂ ) |
| 218 |
202 213 217
|
addassd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) = ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) ) |
| 219 |
212 218
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) = ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) ) |
| 220 |
30 184 219
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ℝfld Σg ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) = ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) ) |
| 221 |
|
fveq2 |
⊢ ( 𝑣 = 𝑗 → ( 𝐾 ‘ 𝑣 ) = ( 𝐾 ‘ 𝑗 ) ) |
| 222 |
|
fveq2 |
⊢ ( 𝑣 = 𝑗 → ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) = ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑗 ) ) |
| 223 |
221 222
|
oveq12d |
⊢ ( 𝑣 = 𝑗 → ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) = ( ( 𝐾 ‘ 𝑗 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑗 ) ) ) |
| 224 |
223
|
cbvmptv |
⊢ ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) = ( 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑗 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑗 ) ) ) |
| 225 |
224
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) = ( 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑗 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑗 ) ) ) ) |
| 226 |
225
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ℝfld Σg ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑣 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑣 ) ) ) ) = ( ℝfld Σg ( 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑗 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑗 ) ) ) ) ) |
| 227 |
220 226 4
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ℝfld Σg ( 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑗 ) · ( ( curry 𝑉 ‘ 𝑖 ) ‘ 𝑗 ) ) ) ) = 0 ) |