Metamath Proof Explorer

Theorem crosspdotsumlem

Description: Lemma for crosspdotd . Expand the group sum over ( 1 ... 3 ) into an explicit three-term sum. (Contributed by Jiamin Zhao, 12-Aug-2026)

Ref Expression
Hypotheses crosspdotd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
crosspdotd.2 ⊢ ( 𝜑 → 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
crosspdotd.3 ⊢ ( 𝜑 → 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
Assertion crosspdotsumlem ( 𝜑 → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 crosspdotd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
2 crosspdotd.2 ⊢ ( 𝜑 → 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
3 crosspdotd.3 ⊢ ( 𝜑 → 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
4 1 2 3 3jca ⊢ ( 𝜑 → ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) )
5 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
6 5 oveq1i ⊢ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = ( ( ℂfld ↾s ℝ ) Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) )
7 6 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = ( ( ℂfld ↾s ℝ ) Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) )
8 fzfid ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 1 ... 3 ) ∈ Fin )
9 simp1 ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
10 elmapi ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → 𝐴 : ( 1 ... 3 ) ⟶ ℝ )
11 9 10 syl ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → 𝐴 : ( 1 ... 3 ) ⟶ ℝ )
12 11 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) ∧ 𝑘 ∈ ( 1 ... 3 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
13 simp2 ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
14 simp3 ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
15 13 14 crosspcld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 𝐵 ⊠ 𝐶 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
16 elmapi ⊢ ( ( 𝐵 ⊠ 𝐶 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝐵 ⊠ 𝐶 ) : ( 1 ... 3 ) ⟶ ℝ )
17 15 16 syl ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 𝐵 ⊠ 𝐶 ) : ( 1 ... 3 ) ⟶ ℝ )
18 17 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) ∧ 𝑘 ∈ ( 1 ... 3 ) ) → ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
19 12 18 remulcld ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) ∧ 𝑘 ∈ ( 1 ... 3 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ∈ ℝ )
20 8 19 regsumfsum ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( ℂfld ↾s ℝ ) Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) )
21 1p2e3 ⊢ ( 1 + 2 ) = 3
22 21 eqcomi ⊢ 3 = ( 1 + 2 )
23 22 oveq2i ⊢ ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) )
24 1z ⊢ 1 ∈ ℤ
25 fztp ⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
26 24 25 ax-mp ⊢ ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
27 23 26 eqtri ⊢ ( 1 ... 3 ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
28 27 sumeq1i ⊢ Σ 𝑘 ∈ ( 1 ... 3 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = Σ 𝑘 ∈ { 1 , ( 1 + 1 ) , ( 1 + 2 ) } ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) )
29 28 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → Σ 𝑘 ∈ ( 1 ... 3 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = Σ 𝑘 ∈ { 1 , ( 1 + 1 ) , ( 1 + 2 ) } ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) )
30 eqidd ⊢ ( 1 ∈ ℤ → 1 = 1 )
31 1p1e2 ⊢ ( 1 + 1 ) = 2
32 31 a1i ⊢ ( 1 ∈ ℤ → ( 1 + 1 ) = 2 )
33 21 a1i ⊢ ( 1 ∈ ℤ → ( 1 + 2 ) = 3 )
34 30 32 33 tpeq123d ⊢ ( 1 ∈ ℤ → { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 } )
35 24 34 ax-mp ⊢ { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 }
36 35 sumeq1i ⊢ Σ 𝑘 ∈ { 1 , ( 1 + 1 ) , ( 1 + 2 ) } ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = Σ 𝑘 ∈ { 1 , 2 , 3 } ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) )
37 36 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → Σ 𝑘 ∈ { 1 , ( 1 + 1 ) , ( 1 + 2 ) } ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = Σ 𝑘 ∈ { 1 , 2 , 3 } ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) )
38 fveq2 ⊢ ( 𝑘 = 1 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 1 ) )
39 fveq2 ⊢ ( 𝑘 = 1 → ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) = ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) )
40 38 39 oveq12d ⊢ ( 𝑘 = 1 → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) )
41 fveq2 ⊢ ( 𝑘 = 2 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 2 ) )
42 fveq2 ⊢ ( 𝑘 = 2 → ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) = ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) )
43 41 42 oveq12d ⊢ ( 𝑘 = 2 → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) )
44 fveq2 ⊢ ( 𝑘 = 3 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 3 ) )
45 fveq2 ⊢ ( 𝑘 = 3 → ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) = ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) )
46 44 45 oveq12d ⊢ ( 𝑘 = 3 → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) )
47 9 rr3fv1cld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 𝐴 ‘ 1 ) ∈ ℝ )
48 15 rr3fv1cld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ∈ ℝ )
49 47 48 remulcld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) ∈ ℝ )
50 49 recnd ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) ∈ ℂ )
51 9 rr3fv2cld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 𝐴 ‘ 2 ) ∈ ℝ )
52 15 rr3fv2cld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ∈ ℝ )
53 51 52 remulcld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) ∈ ℝ )
54 53 recnd ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) ∈ ℂ )
55 9 rr3fv3cld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 𝐴 ‘ 3 ) ∈ ℝ )
56 15 rr3fv3cld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ∈ ℝ )
57 55 56 remulcld ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ∈ ℝ )
58 57 recnd ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ∈ ℂ )
59 50 54 58 3jca ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) ∈ ℂ ∧ ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) ∈ ℂ ∧ ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ∈ ℂ ) )
60 2z ⊢ 2 ∈ ℤ
61 3z ⊢ 3 ∈ ℤ
62 24 60 61 3pm3.2i ⊢ ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 3 ∈ ℤ )
63 62 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 3 ∈ ℤ ) )
64 1ne2 ⊢ 1 ≠ 2
65 64 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → 1 ≠ 2 )
66 1ne3 ⊢ 1 ≠ 3
67 66 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → 1 ≠ 3 )
68 2ne3 ⊢ 2 ≠ 3
69 68 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → 2 ≠ 3 )
70 40 43 46 59 63 65 67 69 sumtp ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → Σ 𝑘 ∈ { 1 , 2 , 3 } ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = ( ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) )
71 50 54 58 addassd ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) )
72 70 71 eqtrd ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → Σ 𝑘 ∈ { 1 , 2 , 3 } ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) )
73 29 37 72 3eqtrd ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → Σ 𝑘 ∈ ( 1 ... 3 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) )
74 7 20 73 3eqtrd ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) )
75 4 74 syl ⊢ ( 𝜑 → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) )