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 A = algSc W
asclmulg.f F = Scalar W
asclmulg.k K = Base F
asclmulg.m × ˙ = W
asclmulg.t ˙ = F
Assertion asclmulg W AssAlg N 0 X K A N ˙ X = N × ˙ A X

Proof

Step Hyp Ref Expression
1 asclmulg.a A = algSc W
2 asclmulg.f F = Scalar W
3 asclmulg.k K = Base F
4 asclmulg.m × ˙ = W
5 asclmulg.t ˙ = F
6 assalmod W AssAlg W LMod
7 6 3ad2ant1 W AssAlg N 0 X K W LMod
8 simp3 W AssAlg N 0 X K X K
9 simp2 W AssAlg N 0 X K N 0
10 assaring W AssAlg W Ring
11 eqid Base W = Base W
12 eqid 1 W = 1 W
13 11 12 ringidcl W Ring 1 W Base W
14 10 13 syl W AssAlg 1 W Base W
15 14 3ad2ant1 W AssAlg N 0 X K 1 W Base W
16 eqid W = W
17 11 2 16 3 4 5 lmodvsmmulgdi W LMod X K N 0 1 W Base W N × ˙ X W 1 W = N ˙ X W 1 W
18 7 8 9 15 17 syl13anc W AssAlg N 0 X K N × ˙ X W 1 W = N ˙ X W 1 W
19 1 2 3 16 12 asclval X K A X = X W 1 W
20 8 19 syl W AssAlg N 0 X K A X = X W 1 W
21 20 oveq2d W AssAlg N 0 X K N × ˙ A X = N × ˙ X W 1 W
22 2 assasca W AssAlg F CRing
23 22 3ad2ant1 W AssAlg N 0 X K F CRing
24 23 crnggrpd W AssAlg N 0 X K F Grp
25 9 nn0zd W AssAlg N 0 X K N
26 3 5 24 25 8 mulgcld W AssAlg N 0 X K N ˙ X K
27 1 2 3 16 12 asclval N ˙ X K A N ˙ X = N ˙ X W 1 W
28 26 27 syl W AssAlg N 0 X K A N ˙ X = N ˙ X W 1 W
29 18 21 28 3eqtr4rd W AssAlg N 0 X K A N ˙ X = N × ˙ A X