Metamath Proof Explorer

Theorem crosspdot0i

Description: Unfold the curried scalar triple product application into an explicit group sum. (A helper for crosspdoti .) (Contributed by Jiamin Zhao, 1-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 crosspdot0i.1 ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
2 crosspdot0i.2 ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) )
3 crosspdot0i.3 ⊢ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) )
4 ovex ⊢ ( ℝ ↑m ( 1 ... 3 ) ) ∈ V
5 4 4 mpoex ⊢ ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) ∈ V
6 fveq1 ⊢ ( 𝑠 = 𝐴 → ( 𝑠 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
7 6 oveq1d ⊢ ( 𝑠 = 𝐴 → ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) )
8 7 mpteq2dv ⊢ ( 𝑠 = 𝐴 → ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) )
9 8 oveq2d ⊢ ( 𝑠 = 𝐴 → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) )
10 9 mpoeq3dv ⊢ ( 𝑠 = 𝐴 → ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) = ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )
11 df-tripp ⊢ tripp = ( 𝑠 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )
12 10 11 fvmptg ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) ∈ V ) → ( tripp ‘ 𝐴 ) = ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )
13 1 5 12 mp2an ⊢ ( tripp ‘ 𝐴 ) = ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) )
14 13 oveqi ⊢ ( 𝐵 ( tripp ‘ 𝐴 ) 𝐶 ) = ( 𝐵 ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) 𝐶 )
15 eqidd ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) = ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )
16 simprl ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) ) → 𝑤 = 𝐵 )
17 simprr ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) ) → 𝑧 = 𝐶 )
18 16 17 oveq12d ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) ) → ( 𝑤 ⊠ 𝑧 ) = ( 𝐵 ⊠ 𝐶 ) )
19 18 fveq1d ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) ) → ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) = ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) )
20 19 oveq2d ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) )
21 20 mpteq2dv ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) ) → ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) )
22 21 oveq2d ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) ) → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) )
23 2 a1i ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
24 3 a1i ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
25 ovexd ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) ∈ V )
26 15 22 23 24 25 ovmpod ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝐵 ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) 𝐶 ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) )
27 1 26 ax-mp ⊢ ( 𝐵 ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) 𝐶 ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) )
28 14 27 eqtri ⊢ ( 𝐵 ( tripp ‘ 𝐴 ) 𝐶 ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) )