![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cayhamlem2 | Structured version Visualization version GIF version |
Description: Lemma for cayhamlem3 21202. (Contributed by AV, 24-Nov-2019.) |
Ref | Expression |
---|---|
cayhamlem2.k | ⊢ 𝐾 = (Base‘𝑅) |
cayhamlem2.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
cayhamlem2.b | ⊢ 𝐵 = (Base‘𝐴) |
cayhamlem2.1 | ⊢ 1 = (1r‘𝐴) |
cayhamlem2.m | ⊢ ∗ = ( ·𝑠 ‘𝐴) |
cayhamlem2.e | ⊢ ↑ = (.g‘(mulGrp‘𝐴)) |
cayhamlem2.r | ⊢ · = (.r‘𝐴) |
Ref | Expression |
---|---|
cayhamlem2 | ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐻‘𝐿) ∗ (𝐿 ↑ 𝑀)) = ((𝐿 ↑ 𝑀) · ((𝐻‘𝐿) ∗ 1 ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmapi 8230 | . . . . . . . 8 ⊢ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) → 𝐻:ℕ0⟶𝐾) | |
2 | 1 | ffvelrnda 6678 | . . . . . . 7 ⊢ ((𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐻‘𝐿) ∈ 𝐾) |
3 | 2 | adantl 474 | . . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐻‘𝐿) ∈ 𝐾) |
4 | cayhamlem2.k | . . . . . . . . 9 ⊢ 𝐾 = (Base‘𝑅) | |
5 | cayhamlem2.a | . . . . . . . . . . . 12 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
6 | 5 | matsca2 20736 | . . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝐴)) |
7 | 6 | 3adant3 1112 | . . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 = (Scalar‘𝐴)) |
8 | 7 | fveq2d 6505 | . . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Base‘𝑅) = (Base‘(Scalar‘𝐴))) |
9 | 4, 8 | syl5req 2827 | . . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Base‘(Scalar‘𝐴)) = 𝐾) |
10 | 9 | eleq2d 2851 | . . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝐻‘𝐿) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝐻‘𝐿) ∈ 𝐾)) |
11 | 10 | adantr 473 | . . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐻‘𝐿) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝐻‘𝐿) ∈ 𝐾)) |
12 | 3, 11 | mpbird 249 | . . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐻‘𝐿) ∈ (Base‘(Scalar‘𝐴))) |
13 | eqid 2778 | . . . . . 6 ⊢ (algSc‘𝐴) = (algSc‘𝐴) | |
14 | eqid 2778 | . . . . . 6 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴) | |
15 | eqid 2778 | . . . . . 6 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴)) | |
16 | cayhamlem2.m | . . . . . 6 ⊢ ∗ = ( ·𝑠 ‘𝐴) | |
17 | cayhamlem2.1 | . . . . . 6 ⊢ 1 = (1r‘𝐴) | |
18 | 13, 14, 15, 16, 17 | asclval 19832 | . . . . 5 ⊢ ((𝐻‘𝐿) ∈ (Base‘(Scalar‘𝐴)) → ((algSc‘𝐴)‘(𝐻‘𝐿)) = ((𝐻‘𝐿) ∗ 1 )) |
19 | 12, 18 | syl 17 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((algSc‘𝐴)‘(𝐻‘𝐿)) = ((𝐻‘𝐿) ∗ 1 )) |
20 | 19 | eqcomd 2784 | . . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐻‘𝐿) ∗ 1 ) = ((algSc‘𝐴)‘(𝐻‘𝐿))) |
21 | 20 | oveq2d 6994 | . 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐿 ↑ 𝑀) · ((𝐻‘𝐿) ∗ 1 )) = ((𝐿 ↑ 𝑀) · ((algSc‘𝐴)‘(𝐻‘𝐿)))) |
22 | 5 | matassa 20760 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ AssAlg) |
23 | 22 | 3adant3 1112 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ AssAlg) |
24 | 23 | adantr 473 | . . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐴 ∈ AssAlg) |
25 | crngring 19034 | . . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
26 | 25 | anim2i 607 | . . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
27 | 26 | 3adant3 1112 | . . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
28 | 5 | matring 20759 | . . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
29 | eqid 2778 | . . . . . . 7 ⊢ (mulGrp‘𝐴) = (mulGrp‘𝐴) | |
30 | 29 | ringmgp 19029 | . . . . . 6 ⊢ (𝐴 ∈ Ring → (mulGrp‘𝐴) ∈ Mnd) |
31 | 27, 28, 30 | 3syl 18 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝐴) ∈ Mnd) |
32 | 31 | adantr 473 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → (mulGrp‘𝐴) ∈ Mnd) |
33 | simprr 760 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℕ0) | |
34 | simpl3 1173 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ 𝐵) | |
35 | cayhamlem2.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐴) | |
36 | 29, 35 | mgpbas 18971 | . . . . 5 ⊢ 𝐵 = (Base‘(mulGrp‘𝐴)) |
37 | cayhamlem2.e | . . . . 5 ⊢ ↑ = (.g‘(mulGrp‘𝐴)) | |
38 | 36, 37 | mulgnn0cl 18032 | . . . 4 ⊢ (((mulGrp‘𝐴) ∈ Mnd ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ 𝐵) → (𝐿 ↑ 𝑀) ∈ 𝐵) |
39 | 32, 33, 34, 38 | syl3anc 1351 | . . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐿 ↑ 𝑀) ∈ 𝐵) |
40 | cayhamlem2.r | . . . 4 ⊢ · = (.r‘𝐴) | |
41 | 13, 14, 15, 35, 40, 16 | asclmul2 19837 | . . 3 ⊢ ((𝐴 ∈ AssAlg ∧ (𝐻‘𝐿) ∈ (Base‘(Scalar‘𝐴)) ∧ (𝐿 ↑ 𝑀) ∈ 𝐵) → ((𝐿 ↑ 𝑀) · ((algSc‘𝐴)‘(𝐻‘𝐿))) = ((𝐻‘𝐿) ∗ (𝐿 ↑ 𝑀))) |
42 | 24, 12, 39, 41 | syl3anc 1351 | . 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐿 ↑ 𝑀) · ((algSc‘𝐴)‘(𝐻‘𝐿))) = ((𝐻‘𝐿) ∗ (𝐿 ↑ 𝑀))) |
43 | 21, 42 | eqtr2d 2815 | 1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐻‘𝐿) ∗ (𝐿 ↑ 𝑀)) = ((𝐿 ↑ 𝑀) · ((𝐻‘𝐿) ∗ 1 ))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ‘cfv 6190 (class class class)co 6978 ↑𝑚 cmap 8208 Fincfn 8308 ℕ0cn0 11710 Basecbs 16342 .rcmulr 16425 Scalarcsca 16427 ·𝑠 cvsca 16428 Mndcmnd 17765 .gcmg 18014 mulGrpcmgp 18965 1rcur 18977 Ringcrg 19023 CRingccrg 19024 AssAlgcasa 19806 algSccascl 19808 Mat cmat 20723 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5050 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-cnex 10393 ax-resscn 10394 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-mulcom 10401 ax-addass 10402 ax-mulass 10403 ax-distr 10404 ax-i2m1 10405 ax-1ne0 10406 ax-1rid 10407 ax-rnegex 10408 ax-rrecex 10409 ax-cnre 10410 ax-pre-lttri 10411 ax-pre-lttrn 10412 ax-pre-ltadd 10413 ax-pre-mulgt0 10414 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-tp 4447 df-op 4449 df-ot 4451 df-uni 4714 df-int 4751 df-iun 4795 df-iin 4796 df-br 4931 df-opab 4993 df-mpt 5010 df-tr 5032 df-id 5313 df-eprel 5318 df-po 5327 df-so 5328 df-fr 5367 df-se 5368 df-we 5369 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-pred 5988 df-ord 6034 df-on 6035 df-lim 6036 df-suc 6037 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-isom 6199 df-riota 6939 df-ov 6981 df-oprab 6982 df-mpo 6983 df-of 7229 df-om 7399 df-1st 7503 df-2nd 7504 df-supp 7636 df-wrecs 7752 df-recs 7814 df-rdg 7852 df-1o 7907 df-oadd 7911 df-er 8091 df-map 8210 df-ixp 8262 df-en 8309 df-dom 8310 df-sdom 8311 df-fin 8312 df-fsupp 8631 df-sup 8703 df-oi 8771 df-card 9164 df-pnf 10478 df-mnf 10479 df-xr 10480 df-ltxr 10481 df-le 10482 df-sub 10674 df-neg 10675 df-nn 11442 df-2 11506 df-3 11507 df-4 11508 df-5 11509 df-6 11510 df-7 11511 df-8 11512 df-9 11513 df-n0 11711 df-z 11797 df-dec 11915 df-uz 12062 df-fz 12712 df-fzo 12853 df-seq 13188 df-hash 13509 df-struct 16344 df-ndx 16345 df-slot 16346 df-base 16348 df-sets 16349 df-ress 16350 df-plusg 16437 df-mulr 16438 df-sca 16440 df-vsca 16441 df-ip 16442 df-tset 16443 df-ple 16444 df-ds 16446 df-hom 16448 df-cco 16449 df-0g 16574 df-gsum 16575 df-prds 16580 df-pws 16582 df-mre 16718 df-mrc 16719 df-acs 16721 df-mgm 17713 df-sgrp 17755 df-mnd 17766 df-mhm 17806 df-submnd 17807 df-grp 17897 df-minusg 17898 df-sbg 17899 df-mulg 18015 df-subg 18063 df-ghm 18130 df-cntz 18221 df-cmn 18671 df-abl 18672 df-mgp 18966 df-ur 18978 df-ring 19025 df-cring 19026 df-subrg 19259 df-lmod 19361 df-lss 19429 df-sra 19669 df-rgmod 19670 df-assa 19809 df-ascl 19811 df-dsmm 20581 df-frlm 20596 df-mamu 20700 df-mat 20724 |
This theorem is referenced by: cayhamlem3 21202 |
Copyright terms: Public domain | W3C validator |