Metamath Proof Explorer

Theorem asclmulg

Description: Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024)

Ref Expression
Hypotheses asclmulg.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
asclmulg.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
asclmulg.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
asclmulg.m ⊢ ↑ = ( .g ‘ 𝑊 )
asclmulg.t ⊢ ∗ = ( .g ‘ 𝐹 )
Assertion asclmulg ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑁 ∗ 𝑋 ) ) = ( 𝑁 ↑ ( 𝐴 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 asclmulg.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 asclmulg.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 asclmulg.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
4 asclmulg.m ⊢ ↑ = ( .g ‘ 𝑊 )
5 asclmulg.t ⊢ ∗ = ( .g ‘ 𝐹 )
6 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
7 6 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → 𝑊 ∈ LMod )
8 simp3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
9 simp2 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → 𝑁 ∈ ℕ0 )
10 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
11 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
13 11 12 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
14 10 13 syl ⊢ ( 𝑊 ∈ AssAlg → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
15 14 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
16 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
17 11 2 16 3 4 5 lmodvsmmulgdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑁 ↑ ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) = ( ( 𝑁 ∗ 𝑋 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
18 7 8 9 15 17 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( 𝑁 ↑ ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) = ( ( 𝑁 ∗ 𝑋 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
19 1 2 3 16 12 asclval ⊢ ( 𝑋 ∈ 𝐾 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
20 8 19 syl ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
21 20 oveq2d ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( 𝑁 ↑ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑁 ↑ ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
22 2 assasca ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ CRing )
23 22 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → 𝐹 ∈ CRing )
24 23 crnggrpd ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → 𝐹 ∈ Grp )
25 9 nn0zd ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → 𝑁 ∈ ℤ )
26 3 5 24 25 8 mulgcld ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( 𝑁 ∗ 𝑋 ) ∈ 𝐾 )
27 1 2 3 16 12 asclval ⊢ ( ( 𝑁 ∗ 𝑋 ) ∈ 𝐾 → ( 𝐴 ‘ ( 𝑁 ∗ 𝑋 ) ) = ( ( 𝑁 ∗ 𝑋 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
28 26 27 syl ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑁 ∗ 𝑋 ) ) = ( ( 𝑁 ∗ 𝑋 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
29 18 21 28 3eqtr4rd ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑁 ∗ 𝑋 ) ) = ( 𝑁 ↑ ( 𝐴 ‘ 𝑋 ) ) )