Metamath Proof Explorer

Theorem ascldimulOLD

Description: Obsolete version of ascldimul as of 5-Nov-2023. (Contributed by Mario Carneiro, 8-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ascldimul.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
ascldimul.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
ascldimul.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
ascldimul.t ⊢ × = ( .r ‘ 𝑊 )
ascldimul.s ⊢ · = ( .r ‘ 𝐹 )
Assertion ascldimulOLD ( ( 𝑊 ∈ 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 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
7 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
8 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
9 7 8 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
10 6 9 syl ⊢ ( 𝑊 ∈ AssAlg → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
11 7 4 8 ringlidm ⊢ ( ( 𝑊 ∈ Ring ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
12 6 10 11 syl2anc ⊢ ( 𝑊 ∈ AssAlg → ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
13 12 oveq2d ⊢ ( 𝑊 ∈ AssAlg → ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
14 13 oveq2d ⊢ ( 𝑊 ∈ AssAlg → ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
15 14 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
16 simp1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑊 ∈ AssAlg )
17 simp2 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑅 ∈ 𝐾 )
18 10 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
19 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
20 19 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑊 ∈ LMod )
21 simp3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → 𝑆 ∈ 𝐾 )
22 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
23 7 2 22 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝐾 ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) → ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ ( Base ‘ 𝑊 ) )
24 20 21 18 23 syl3anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ ( Base ‘ 𝑊 ) )
25 7 2 3 22 4 assaass ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑅 ∈ 𝐾 ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ) )
26 16 17 18 24 25 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ) )
27 7 2 3 22 4 assaassr ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑆 ∈ 𝐾 ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 1r ‘ 𝑊 ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) ) )
28 16 21 18 18 27 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 1r ‘ 𝑊 ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) ) )
29 28 oveq2d ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) ) ) )
30 26 29 eqtrd ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) × ( 1r ‘ 𝑊 ) ) ) ) )
31 7 2 22 3 5 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
32 20 17 21 18 31 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
33 15 30 32 3eqtr4rd ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
34 2 assasca ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ CRing )
35 crngring ⊢ ( 𝐹 ∈ CRing → 𝐹 ∈ Ring )
36 34 35 syl ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
37 3 5 ringcl ⊢ ( ( 𝐹 ∈ Ring ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 · 𝑆 ) ∈ 𝐾 )
38 36 37 syl3an1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝑅 · 𝑆 ) ∈ 𝐾 )
39 1 2 3 22 8 asclval ⊢ ( ( 𝑅 · 𝑆 ) ∈ 𝐾 → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
40 38 39 syl ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝑅 · 𝑆 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
41 1 2 3 22 8 asclval ⊢ ( 𝑅 ∈ 𝐾 → ( 𝐴 ‘ 𝑅 ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
42 17 41 syl ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑅 ) = ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
43 1 2 3 22 8 asclval ⊢ ( 𝑆 ∈ 𝐾 → ( 𝐴 ‘ 𝑆 ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
44 21 43 syl ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) = ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
45 42 44 oveq12d ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) = ( ( 𝑅 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) × ( 𝑆 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
46 33 40 45 3eqtr4d ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ ( 𝑅 · 𝑆 ) ) = ( ( 𝐴 ‘ 𝑅 ) × ( 𝐴 ‘ 𝑆 ) ) )