Metamath Proof Explorer

Theorem crosspdotsumi

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

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

Proof

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