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 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
12 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
13 12 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑊 ∈ Ring )
14 10 11 13 ringidcld ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
15 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
16 10 2 15 3 5 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
17 7 8 9 14 16 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
18 2 assasca ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
19 3 5 ringcl ⊢ ( ( 𝐹 ∈ Ring ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 · 𝑆 ) ∈ 𝐾 )
20 18 19 syl3an1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 · 𝑆 ) ∈ 𝐾 )
21 1 2 3 15 11 asclval ⊢ ( ( 𝑅 · 𝑆 ) ∈ 𝐾 → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
22 20 21 syl ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
23 1 2 12 6 3 10 asclf ⊢ ( 𝑊 ∈ AssAlg → 𝐴 : 𝐾 ⟶ ( Base ‘ 𝑊 ) )
24 23 ffvelcdmda ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) ∈ ( Base ‘ 𝑊 ) )
25 24 3adant2 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) ∈ ( Base ‘ 𝑊 ) )
26 1 2 3 10 4 15 asclmul1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ ( 𝐴 ‘ 𝑆 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝐴 ‘ 𝑆 ) ) )
27 25 26 syld3an3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝐴 ‘ 𝑆 ) ) )
28 1 2 3 15 11 asclval ⊢ ( 𝑆 ∈ 𝐾 → ( 𝐴 ‘ 𝑆 ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
29 28 3ad2ant3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
30 29 oveq2d ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝐴 ‘ 𝑆 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
31 27 30 eqtrd ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
32 17 22 31 3eqtr4d ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) )