Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frlmgsum Unicode version

Theorem frlmgsum 26917
 Description: Finite commutative sums in a free module are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 5-Jul-2015.)
Hypotheses
Ref Expression
frlmgsum.y freeLMod
frlmgsum.b
frlmgsum.z
frlmgsum.i
frlmgsum.j
frlmgsum.r
frlmgsum.f
frlmgsum.w
Assertion
Ref Expression
frlmgsum g g
Distinct variable groups:   ,,   ,,   ,,   , ,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem frlmgsum
StepHypRef Expression
1 frlmgsum.r . . . 4
2 frlmgsum.i . . . 4
3 frlmgsum.y . . . . 5 freeLMod
4 frlmgsum.b . . . . 5
53, 4frlmpws 26903 . . . 4 ringLMod s s
61, 2, 5syl2anc 643 . . 3 ringLMod s s
76oveq1d 6049 . 2 g ringLMod s s g
8 eqid 2401 . . 3 ringLMod s ringLMod s
9 eqid 2401 . . 3 ringLMod s ringLMod s
10 eqid 2401 . . 3 ringLMod s s ringLMod s s
11 ovex 6059 . . . 4 ringLMod s
1211a1i 11 . . 3 ringLMod s
13 frlmgsum.j . . 3
14 eqid 2401 . . . . . 6 ringLMod s ringLMod s
153, 4, 14frlmlss 26904 . . . . 5 ringLMod s
161, 2, 15syl2anc 643 . . . 4 ringLMod s
178, 14lssss 15954 . . . 4 ringLMod s ringLMod s
1816, 17syl 16 . . 3 ringLMod s
19 frlmgsum.f . . . 4
20 eqid 2401 . . . 4
2119, 20fmptd 5846 . . 3
22 rlmlmod 16217 . . . . . 6 ringLMod
231, 22syl 16 . . . . 5 ringLMod
24 eqid 2401 . . . . . 6 ringLMod s ringLMod s
2524pwslmod 15987 . . . . 5 ringLMod ringLMod s
2623, 2, 25syl2anc 643 . . . 4 ringLMod s
27 eqid 2401 . . . . 5 ringLMod s ringLMod s
2827, 14lss0cl 15964 . . . 4 ringLMod s ringLMod s ringLMod s
2926, 16, 28syl2anc 643 . . 3 ringLMod s
30 lmodcmn 15933 . . . . . . 7 ringLMod ringLMod CMnd
3123, 30syl 16 . . . . . 6 ringLMod CMnd
32 cmnmnd 15368 . . . . . 6 ringLMod CMnd ringLMod
3331, 32syl 16 . . . . 5 ringLMod
3424pwsmnd 14671 . . . . 5 ringLMod ringLMod s
3533, 2, 34syl2anc 643 . . . 4 ringLMod s
368, 9, 27mndlrid 14656 . . . 4 ringLMod s ringLMod s ringLMod s ringLMod s ringLMod s ringLMod s
3735, 36sylan 458 . . 3 ringLMod s ringLMod s ringLMod s ringLMod s ringLMod s
388, 9, 10, 12, 13, 18, 21, 29, 37gsumress 14718 . 2 ringLMod s g ringLMod s s g
39 rlmbas 16208 . . . 4 ringLMod
402adantr 452 . . . . . . . . 9
41 eqid 2401 . . . . . . . . . 10
423, 41, 4frlmbasf 26913 . . . . . . . . 9
4340, 19, 42syl2anc 643 . . . . . . . 8
44 eqid 2401 . . . . . . . . 9
4544fmpt 5843 . . . . . . . 8
4643, 45sylibr 204 . . . . . . 7
4746r19.21bi 2761 . . . . . 6
4847an32s 780 . . . . 5
4948anasss 629 . . . 4
50 frlmgsum.z . . . . . . . . 9
516fveq2d 5686 . . . . . . . . . 10 ringLMod s s
5214lsssubg 15974 . . . . . . . . . . . 12 ringLMod s ringLMod s SubGrpringLMod s
5326, 16, 52syl2anc 643 . . . . . . . . . . 11 SubGrpringLMod s
5410, 27subg0 14891 . . . . . . . . . . 11 SubGrpringLMod s ringLMod s ringLMod s s
5553, 54syl 16 . . . . . . . . . 10 ringLMod s ringLMod s s
5651, 55eqtr4d 2436 . . . . . . . . 9 ringLMod s
5750, 56syl5eq 2445 . . . . . . . 8 ringLMod s
5857sneqd 3784 . . . . . . 7 ringLMod s
5958difeq2d 3422 . . . . . 6 ringLMod s
6059imaeq2d 5157 . . . . 5 ringLMod s
61 frlmgsum.w . . . . 5
6260, 61eqeltrrd 2476 . . . 4 ringLMod s
6324, 39, 27, 2, 13, 31, 49, 62pwsgsum 15494 . . 3 ringLMod s g ringLMod g
64 mptexg 5918 . . . . . 6
6513, 64syl 16 . . . . 5
66 fvex 5696 . . . . . 6 ringLMod
6766a1i 11 . . . . 5 ringLMod
6839a1i 11 . . . . 5 ringLMod
69 rlmplusg 16209 . . . . . 6 ringLMod
7069a1i 11 . . . . 5 ringLMod
7165, 1, 67, 68, 70gsumpropd 14717 . . . 4 g ringLMod g
7271mpteq2dv 4251 . . 3 g ringLMod g
7363, 72eqtr4d 2436 . 2 ringLMod s g g
747, 38, 733eqtr2d 2439 1 g g
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   wceq 1649   wcel 1721  wral 2663  cvv 2913   cdif 3274   wss 3277  csn 3771   cmpt 4221  ccnv 4831  cima 4835  wf 5404  cfv 5408  (class class class)co 6034  cfn 7059  cbs 13410   ↾s cress 13411   cplusg 13470   s cpws 13611  c0g 13664   g cgsu 13665  cmnd 14625  SubGrpcsubg 14879  CMndccmn 15353  crg 15601  clmod 15891  clss 15949  ringLModcrglmod 16182   freeLMod cfrlm 26897 This theorem is referenced by:  uvcresum  26927 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-se 4497  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-oadd 6678  df-er 6855  df-map 6970  df-ixp 7014  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-sup 7395  df-oi 7426  df-card 7773  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-nn 9947  df-2 10004  df-3 10005  df-4 10006  df-5 10007  df-6 10008  df-7 10009  df-8 10010  df-9 10011  df-10 10012  df-n0 10168  df-z 10229  df-dec 10329  df-uz 10435  df-fz 10990  df-fzo 11080  df-seq 11265  df-hash 11560  df-struct 13412  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-ress 13417  df-plusg 13483  df-mulr 13484  df-sca 13486  df-vsca 13487  df-tset 13489  df-ple 13490  df-ds 13492  df-hom 13494  df-cco 13495  df-prds 13612  df-pws 13614  df-0g 13668  df-gsum 13669  df-mnd 14631  df-mhm 14679  df-grp 14753  df-minusg 14754  df-sbg 14755  df-subg 14882  df-cntz 15057  df-cmn 15355  df-abl 15356  df-mgp 15590  df-rng 15604  df-ur 15606  df-subrg 15807  df-lmod 15893  df-lss 15950  df-sra 16185  df-rgmod 16186  df-dsmm 26883  df-frlm 26899
 Copyright terms: Public domain W3C validator