Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > asclmulg | Structured version Visualization version GIF version |
Description: Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
Ref | Expression |
---|---|
asclmulg.a | ⊢ 𝐴 = (algSc‘𝑊) |
asclmulg.f | ⊢ 𝐹 = (Scalar‘𝑊) |
asclmulg.k | ⊢ 𝐾 = (Base‘𝐹) |
asclmulg.m | ⊢ ↑ = (.g‘𝑊) |
asclmulg.t | ⊢ ∗ = (.g‘𝐹) |
Ref | Expression |
---|---|
asclmulg | ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝐴‘(𝑁 ∗ 𝑋)) = (𝑁 ↑ (𝐴‘𝑋))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | assalmod 20630 | . . . 4 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) | |
2 | 1 | 3ad2ant1 1130 | . . 3 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → 𝑊 ∈ LMod) |
3 | simp3 1135 | . . 3 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → 𝑋 ∈ 𝐾) | |
4 | simp2 1134 | . . 3 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → 𝑁 ∈ ℕ0) | |
5 | assaring 20631 | . . . . 5 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) | |
6 | eqid 2758 | . . . . . 6 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
7 | eqid 2758 | . . . . . 6 ⊢ (1r‘𝑊) = (1r‘𝑊) | |
8 | 6, 7 | ringidcl 19394 | . . . . 5 ⊢ (𝑊 ∈ Ring → (1r‘𝑊) ∈ (Base‘𝑊)) |
9 | 5, 8 | syl 17 | . . . 4 ⊢ (𝑊 ∈ AssAlg → (1r‘𝑊) ∈ (Base‘𝑊)) |
10 | 9 | 3ad2ant1 1130 | . . 3 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (1r‘𝑊) ∈ (Base‘𝑊)) |
11 | asclmulg.f | . . . 4 ⊢ 𝐹 = (Scalar‘𝑊) | |
12 | eqid 2758 | . . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
13 | asclmulg.k | . . . 4 ⊢ 𝐾 = (Base‘𝐹) | |
14 | asclmulg.m | . . . 4 ⊢ ↑ = (.g‘𝑊) | |
15 | asclmulg.t | . . . 4 ⊢ ∗ = (.g‘𝐹) | |
16 | 6, 11, 12, 13, 14, 15 | lmodvsmmulgdi 19742 | . . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ (1r‘𝑊) ∈ (Base‘𝑊))) → (𝑁 ↑ (𝑋( ·𝑠 ‘𝑊)(1r‘𝑊))) = ((𝑁 ∗ 𝑋)( ·𝑠 ‘𝑊)(1r‘𝑊))) |
17 | 2, 3, 4, 10, 16 | syl13anc 1369 | . 2 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝑁 ↑ (𝑋( ·𝑠 ‘𝑊)(1r‘𝑊))) = ((𝑁 ∗ 𝑋)( ·𝑠 ‘𝑊)(1r‘𝑊))) |
18 | asclmulg.a | . . . . 5 ⊢ 𝐴 = (algSc‘𝑊) | |
19 | 18, 11, 13, 12, 7 | asclval 20647 | . . . 4 ⊢ (𝑋 ∈ 𝐾 → (𝐴‘𝑋) = (𝑋( ·𝑠 ‘𝑊)(1r‘𝑊))) |
20 | 3, 19 | syl 17 | . . 3 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝐴‘𝑋) = (𝑋( ·𝑠 ‘𝑊)(1r‘𝑊))) |
21 | 20 | oveq2d 7171 | . 2 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝑁 ↑ (𝐴‘𝑋)) = (𝑁 ↑ (𝑋( ·𝑠 ‘𝑊)(1r‘𝑊)))) |
22 | 11 | assasca 20632 | . . . . . 6 ⊢ (𝑊 ∈ AssAlg → 𝐹 ∈ CRing) |
23 | 22 | 3ad2ant1 1130 | . . . . 5 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → 𝐹 ∈ CRing) |
24 | 23 | crnggrpd 19384 | . . . 4 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → 𝐹 ∈ Grp) |
25 | 4 | nn0zd 12129 | . . . 4 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → 𝑁 ∈ ℤ) |
26 | 13, 15, 24, 25, 3 | mulgcld 18321 | . . 3 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝑁 ∗ 𝑋) ∈ 𝐾) |
27 | 18, 11, 13, 12, 7 | asclval 20647 | . . 3 ⊢ ((𝑁 ∗ 𝑋) ∈ 𝐾 → (𝐴‘(𝑁 ∗ 𝑋)) = ((𝑁 ∗ 𝑋)( ·𝑠 ‘𝑊)(1r‘𝑊))) |
28 | 26, 27 | syl 17 | . 2 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝐴‘(𝑁 ∗ 𝑋)) = ((𝑁 ∗ 𝑋)( ·𝑠 ‘𝑊)(1r‘𝑊))) |
29 | 17, 21, 28 | 3eqtr4rd 2804 | 1 ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝐴‘(𝑁 ∗ 𝑋)) = (𝑁 ↑ (𝐴‘𝑋))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ‘cfv 6339 (class class class)co 7155 ℕ0cn0 11939 Basecbs 16546 Scalarcsca 16631 ·𝑠 cvsca 16632 .gcmg 18296 1rcur 19324 Ringcrg 19370 CRingccrg 19371 LModclmod 19707 AssAlgcasa 20620 algSccascl 20622 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5159 ax-sep 5172 ax-nul 5179 ax-pow 5237 ax-pr 5301 ax-un 7464 ax-cnex 10636 ax-resscn 10637 ax-1cn 10638 ax-icn 10639 ax-addcl 10640 ax-addrcl 10641 ax-mulcl 10642 ax-mulrcl 10643 ax-mulcom 10644 ax-addass 10645 ax-mulass 10646 ax-distr 10647 ax-i2m1 10648 ax-1ne0 10649 ax-1rid 10650 ax-rnegex 10651 ax-rrecex 10652 ax-cnre 10653 ax-pre-lttri 10654 ax-pre-lttrn 10655 ax-pre-ltadd 10656 ax-pre-mulgt0 10657 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-iun 4888 df-br 5036 df-opab 5098 df-mpt 5116 df-tr 5142 df-id 5433 df-eprel 5438 df-po 5446 df-so 5447 df-fr 5486 df-we 5488 df-xp 5533 df-rel 5534 df-cnv 5535 df-co 5536 df-dm 5537 df-rn 5538 df-res 5539 df-ima 5540 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7585 df-1st 7698 df-2nd 7699 df-wrecs 7962 df-recs 8023 df-rdg 8061 df-er 8304 df-en 8533 df-dom 8534 df-sdom 8535 df-pnf 10720 df-mnf 10721 df-xr 10722 df-ltxr 10723 df-le 10724 df-sub 10915 df-neg 10916 df-nn 11680 df-2 11742 df-n0 11940 df-z 12026 df-uz 12288 df-fz 12945 df-seq 13424 df-ndx 16549 df-slot 16550 df-base 16552 df-sets 16553 df-plusg 16641 df-0g 16778 df-mgm 17923 df-sgrp 17972 df-mnd 17983 df-grp 18177 df-minusg 18178 df-mulg 18297 df-mgp 19313 df-ur 19325 df-ring 19372 df-cring 19373 df-lmod 19709 df-assa 20623 df-ascl 20625 |
This theorem is referenced by: ply1chr 31194 |
Copyright terms: Public domain | W3C validator |