Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > assamulgscmlem1 | Structured version Visualization version GIF version | ||
| Description: Lemma 1 for assamulgscm 21821 (induction base). (Contributed by AV, 26-Aug-2019.) |
| Ref | Expression |
|---|---|
| assamulgscm.v | β’ π = (Baseβπ) |
| assamulgscm.f | β’ πΉ = (Scalarβπ) |
| assamulgscm.b | β’ π΅ = (BaseβπΉ) |
| assamulgscm.s | β’ Β· = ( Β·π βπ) |
| assamulgscm.g | β’ πΊ = (mulGrpβπΉ) |
| assamulgscm.p | β’ β = (.gβπΊ) |
| assamulgscm.h | β’ π» = (mulGrpβπ) |
| assamulgscm.e | β’ πΈ = (.gβπ») |
| Ref | Expression |
|---|---|
| assamulgscmlem1 | β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0πΈ(π΄ Β· π)) = ((0 β π΄) Β· (0πΈπ))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | assalmod 21781 | . . . 4 β’ (π β AssAlg β π β LMod) | |
| 2 | assaring 21782 | . . . . 5 β’ (π β AssAlg β π β Ring) | |
| 3 | assamulgscm.v | . . . . . 6 β’ π = (Baseβπ) | |
| 4 | eqid 2727 | . . . . . 6 β’ (1rβπ) = (1rβπ) | |
| 5 | 3, 4 | ringidcl 20191 | . . . . 5 β’ (π β Ring β (1rβπ) β π) |
| 6 | 2, 5 | syl 17 | . . . 4 β’ (π β AssAlg β (1rβπ) β π) |
| 7 | assamulgscm.f | . . . . . 6 β’ πΉ = (Scalarβπ) | |
| 8 | assamulgscm.s | . . . . . 6 β’ Β· = ( Β·π βπ) | |
| 9 | eqid 2727 | . . . . . 6 β’ (1rβπΉ) = (1rβπΉ) | |
| 10 | 3, 7, 8, 9 | lmodvs1 20762 | . . . . 5 β’ ((π β LMod β§ (1rβπ) β π) β ((1rβπΉ) Β· (1rβπ)) = (1rβπ)) |
| 11 | 10 | eqcomd 2733 | . . . 4 β’ ((π β LMod β§ (1rβπ) β π) β (1rβπ) = ((1rβπΉ) Β· (1rβπ))) |
| 12 | 1, 6, 11 | syl2anc 583 | . . 3 β’ (π β AssAlg β (1rβπ) = ((1rβπΉ) Β· (1rβπ))) |
| 13 | 12 | adantl 481 | . 2 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (1rβπ) = ((1rβπΉ) Β· (1rβπ))) |
| 14 | 1 | adantl 481 | . . . 4 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β π β LMod) |
| 15 | simpll 766 | . . . 4 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β π΄ β π΅) | |
| 16 | simplr 768 | . . . 4 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β π β π) | |
| 17 | assamulgscm.b | . . . . 5 β’ π΅ = (BaseβπΉ) | |
| 18 | 3, 7, 8, 17 | lmodvscl 20750 | . . . 4 β’ ((π β LMod β§ π΄ β π΅ β§ π β π) β (π΄ Β· π) β π) |
| 19 | 14, 15, 16, 18 | syl3anc 1369 | . . 3 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (π΄ Β· π) β π) |
| 20 | assamulgscm.h | . . . . 5 β’ π» = (mulGrpβπ) | |
| 21 | 20, 3 | mgpbas 20071 | . . . 4 β’ π = (Baseβπ») |
| 22 | 20, 4 | ringidval 20114 | . . . 4 β’ (1rβπ) = (0gβπ») |
| 23 | assamulgscm.e | . . . 4 β’ πΈ = (.gβπ») | |
| 24 | 21, 22, 23 | mulg0 19021 | . . 3 β’ ((π΄ Β· π) β π β (0πΈ(π΄ Β· π)) = (1rβπ)) |
| 25 | 19, 24 | syl 17 | . 2 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0πΈ(π΄ Β· π)) = (1rβπ)) |
| 26 | assamulgscm.g | . . . . . 6 β’ πΊ = (mulGrpβπΉ) | |
| 27 | 26, 17 | mgpbas 20071 | . . . . 5 β’ π΅ = (BaseβπΊ) |
| 28 | 26, 9 | ringidval 20114 | . . . . 5 β’ (1rβπΉ) = (0gβπΊ) |
| 29 | assamulgscm.p | . . . . 5 β’ β = (.gβπΊ) | |
| 30 | 27, 28, 29 | mulg0 19021 | . . . 4 β’ (π΄ β π΅ β (0 β π΄) = (1rβπΉ)) |
| 31 | 15, 30 | syl 17 | . . 3 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0 β π΄) = (1rβπΉ)) |
| 32 | 21, 22, 23 | mulg0 19021 | . . . 4 β’ (π β π β (0πΈπ) = (1rβπ)) |
| 33 | 16, 32 | syl 17 | . . 3 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0πΈπ) = (1rβπ)) |
| 34 | 31, 33 | oveq12d 7432 | . 2 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β ((0 β π΄) Β· (0πΈπ)) = ((1rβπΉ) Β· (1rβπ))) |
| 35 | 13, 25, 34 | 3eqtr4d 2777 | 1 β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0πΈ(π΄ Β· π)) = ((0 β π΄) Β· (0πΈπ))) |
| Colors of variables: wff setvar class |
| Syntax hints: β wi 4 β§ wa 395 = wceq 1534 β wcel 2099 βcfv 6542 (class class class)co 7414 0cc0 11130 Basecbs 17171 Scalarcsca 17227 Β·π cvsca 17228 .gcmg 19014 mulGrpcmgp 20065 1rcur 20112 Ringcrg 20164 LModclmod 20732 AssAlgcasa 21771 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207 |
| This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-er 8718 df-en 8956 df-dom 8957 df-sdom 8958 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-nn 12235 df-2 12297 df-n0 12495 df-z 12581 df-uz 12845 df-seq 13991 df-sets 17124 df-slot 17142 df-ndx 17154 df-base 17172 df-plusg 17237 df-0g 17414 df-mgm 18591 df-sgrp 18670 df-mnd 18686 df-mulg 19015 df-mgp 20066 df-ur 20113 df-ring 20166 df-lmod 20734 df-assa 21774 |
| This theorem is referenced by: assamulgscm 21821 |
| Copyright terms: Public domain | W3C validator |