Metamath Proof Explorer

Theorem ascldimul

Description: The algebra scalar lifting function distributes over multiplication. (Contributed by Mario Carneiro, 8-Mar-2015) (Proof shortened by SN, 5-Nov-2023)

Ref Expression
Hypotheses ascldimul.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
ascldimul.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
ascldimul.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
ascldimul.t ⊢ × = ( .r ‘ 𝑊 )
ascldimul.s ⊢ · = ( .r ‘ 𝐹 )
Assertion ascldimul ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ascldimul.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 ascldimul.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 ascldimul.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
4 ascldimul.t ⊢ × = ( .r ‘ 𝑊 )
5 ascldimul.s ⊢ · = ( .r ‘ 𝐹 )
6 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
7 6 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑊 ∈ LMod )
8 simp2 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑅 ∈ 𝐾 )
9 simp3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑆 ∈ 𝐾 )
10 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
11 10 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑊 ∈ Ring )
12 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
14 12 13 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
15 11 14 syl ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
16 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
17 12 2 16 3 5 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
18 7 8 9 15 17 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
19 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
20 6 19 syl ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
21 3 5 ringcl ⊢ ( ( 𝐹 ∈ Ring ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 · 𝑆 ) ∈ 𝐾 )
22 20 21 syl3an1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 · 𝑆 ) ∈ 𝐾 )
23 1 2 3 16 13 asclval ⊢ ( ( 𝑅 · 𝑆 ) ∈ 𝐾 → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
24 22 23 syl ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
25 1 2 10 6 3 12 asclf ⊢ ( 𝑊 ∈ AssAlg → 𝐴 : 𝐾 ⟶ ( Base ‘ 𝑊 ) )
26 25 ffvelcdmda ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) ∈ ( Base ‘ 𝑊 ) )
27 26 3adant2 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) ∈ ( Base ‘ 𝑊 ) )
28 1 2 3 12 4 16 asclmul1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ ( 𝐴 ‘ 𝑆 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝐴 ‘ 𝑆 ) ) )
29 27 28 syld3an3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝐴 ‘ 𝑆 ) ) )
30 1 2 3 16 13 asclval ⊢ ( 𝑆 ∈ 𝐾 → ( 𝐴 ‘ 𝑆 ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
31 30 3ad2ant3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
32 31 oveq2d ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝐴 ‘ 𝑆 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
33 29 32 eqtrd ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
34 18 24 33 3eqtr4d ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) )