Metamath Proof Explorer

Theorem crosspdot0lem

Description: Lemma for crosspdotd . Unfold the curried scalar triple product application into an explicit group sum. (Contributed by Jiamin Zhao, 12-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 crosspdot0lem.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
2 crosspdot0lem.2 ⊢ ( 𝜑 → 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
3 crosspdot0lem.3 ⊢ ( 𝜑 → 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
4 df-tripp ⊢ tripp = ( 𝑠 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )
5 fveq1 ⊢ ( 𝑠 = 𝐴 → ( 𝑠 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
6 5 oveq1d ⊢ ( 𝑠 = 𝐴 → ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) )
7 6 mpteq2dv ⊢ ( 𝑠 = 𝐴 → ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) )
8 7 oveq2d ⊢ ( 𝑠 = 𝐴 → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) )
9 8 mpoeq3dv ⊢ ( 𝑠 = 𝐴 → ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑠 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) = ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )
10 ovex ⊢ ( ℝ ↑m ( 1 ... 3 ) ) ∈ V
11 10 10 mpoex ⊢ ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) ∈ V
12 11 a1i ⊢ ( 𝜑 → ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) ∈ V )
13 4 9 1 12 fvmptd3 ⊢ ( 𝜑 → ( tripp ‘ 𝐴 ) = ( 𝑤 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )
14 oveq12 ⊢ ( ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑤 ⊠ 𝑧 ) = ( 𝐵 ⊠ 𝐶 ) )
15 14 fveq1d ⊢ ( ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) = ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) )
16 15 oveq2d ⊢ ( ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) )
17 16 mpteq2dv ⊢ ( ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) )
18 17 oveq2d ⊢ ( ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐵 ∧ 𝑧 = 𝐶 ) ) → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑤 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) )
20 ovexd ⊢ ( 𝜑 → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) ∈ V )
21 13 19 2 3 20 ovmpod ⊢ ( 𝜑 → ( 𝐵 ( tripp ‘ 𝐴 ) 𝐶 ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) )