Users' Mathboxes Mathbox for Rohan Ridenour < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mnringmulrcld Structured version   Visualization version   GIF version

Theorem mnringmulrcld 42977
Description: Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.)
Hypotheses
Ref Expression
mnringmulrcld.2 ๐น = (๐‘… MndRing ๐‘€)
mnringmulrcld.3 ๐ต = (Baseโ€˜๐น)
mnringmulrcld.1 ๐ด = (Baseโ€˜๐‘€)
mnringmulrcld.4 ยท = (.rโ€˜๐น)
mnringmulrcld.5 (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
mnringmulrcld.6 (๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘ˆ)
mnringmulrcld.7 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
mnringmulrcld.8 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)
Assertion
Ref Expression
mnringmulrcld (๐œ‘ โ†’ (๐‘‹ ยท ๐‘Œ) โˆˆ ๐ต)

Proof of Theorem mnringmulrcld
Dummy variables ๐‘Ž ๐‘ ๐‘ ๐‘– are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mnringmulrcld.2 . . 3 ๐น = (๐‘… MndRing ๐‘€)
2 mnringmulrcld.3 . . 3 ๐ต = (Baseโ€˜๐น)
3 eqid 2732 . . 3 (.rโ€˜๐‘…) = (.rโ€˜๐‘…)
4 eqid 2732 . . 3 (0gโ€˜๐‘…) = (0gโ€˜๐‘…)
5 mnringmulrcld.1 . . 3 ๐ด = (Baseโ€˜๐‘€)
6 eqid 2732 . . 3 (+gโ€˜๐‘€) = (+gโ€˜๐‘€)
7 mnringmulrcld.4 . . 3 ยท = (.rโ€˜๐น)
8 mnringmulrcld.5 . . 3 (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
9 mnringmulrcld.6 . . 3 (๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘ˆ)
10 mnringmulrcld.7 . . 3 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
11 mnringmulrcld.8 . . 3 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11mnringmulrvald 42976 . 2 (๐œ‘ โ†’ (๐‘‹ ยท ๐‘Œ) = (๐น ฮฃg (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))))
13 eqid 2732 . . 3 (0gโ€˜๐น) = (0gโ€˜๐น)
141, 8, 9mnringlmodd 42975 . . . 4 (๐œ‘ โ†’ ๐น โˆˆ LMod)
15 lmodcmn 20519 . . . 4 (๐น โˆˆ LMod โ†’ ๐น โˆˆ CMnd)
1614, 15syl 17 . . 3 (๐œ‘ โ†’ ๐น โˆˆ CMnd)
175fvexi 6905 . . . . 5 ๐ด โˆˆ V
1817, 17xpex 7739 . . . 4 (๐ด ร— ๐ด) โˆˆ V
1918a1i 11 . . 3 (๐œ‘ โ†’ (๐ด ร— ๐ด) โˆˆ V)
2083ad2ant1 1133 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘… โˆˆ Ring)
21 eqid 2732 . . . . . . . . . . . . . . . 16 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘…)
221, 2, 5, 21, 8, 9, 10mnringbasefd 42964 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‹:๐ดโŸถ(Baseโ€˜๐‘…))
23223ad2ant1 1133 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘‹:๐ดโŸถ(Baseโ€˜๐‘…))
24 simp2 1137 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘Ž โˆˆ ๐ด)
2523, 24ffvelcdmd 7087 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐‘‹โ€˜๐‘Ž) โˆˆ (Baseโ€˜๐‘…))
261, 2, 5, 21, 8, 9, 11mnringbasefd 42964 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘Œ:๐ดโŸถ(Baseโ€˜๐‘…))
27263ad2ant1 1133 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘Œ:๐ดโŸถ(Baseโ€˜๐‘…))
28 simp3 1138 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘ โˆˆ ๐ด)
2927, 28ffvelcdmd 7087 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐‘Œโ€˜๐‘) โˆˆ (Baseโ€˜๐‘…))
3021, 3ringcl 20072 . . . . . . . . . . . . 13 ((๐‘… โˆˆ Ring โˆง (๐‘‹โ€˜๐‘Ž) โˆˆ (Baseโ€˜๐‘…) โˆง (๐‘Œโ€˜๐‘) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) โˆˆ (Baseโ€˜๐‘…))
3120, 25, 29, 30syl3anc 1371 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) โˆˆ (Baseโ€˜๐‘…))
3221, 4ring0cl 20083 . . . . . . . . . . . . 13 (๐‘… โˆˆ Ring โ†’ (0gโ€˜๐‘…) โˆˆ (Baseโ€˜๐‘…))
3320, 32syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (0gโ€˜๐‘…) โˆˆ (Baseโ€˜๐‘…))
3431, 33ifcld 4574 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)) โˆˆ (Baseโ€˜๐‘…))
3534adantr 481 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘– โˆˆ ๐ด) โ†’ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)) โˆˆ (Baseโ€˜๐‘…))
3635fmpttd 7114 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))):๐ดโŸถ(Baseโ€˜๐‘…))
3721fvexi 6905 . . . . . . . . . 10 (Baseโ€˜๐‘…) โˆˆ V
3837, 17elmap 8864 . . . . . . . . 9 ((๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ((Baseโ€˜๐‘…) โ†‘m ๐ด) โ†” (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))):๐ดโŸถ(Baseโ€˜๐‘…))
3936, 38sylibr 233 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ((Baseโ€˜๐‘…) โ†‘m ๐ด))
4017a1i 11 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐ด โˆˆ V)
41 eqid 2732 . . . . . . . . 9 (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))
4240, 33, 41sniffsupp 9394 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) finSupp (0gโ€˜๐‘…))
4339, 42jca 512 . . . . . . 7 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ((Baseโ€˜๐‘…) โ†‘m ๐ด) โˆง (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) finSupp (0gโ€˜๐‘…)))
4493ad2ant1 1133 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘€ โˆˆ ๐‘ˆ)
451, 2, 5, 21, 4, 20, 44mnringelbased 42963 . . . . . . 7 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ๐ต โ†” ((๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ((Baseโ€˜๐‘…) โ†‘m ๐ด) โˆง (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) finSupp (0gโ€˜๐‘…))))
4643, 45mpbird 256 . . . . . 6 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ๐ต)
47463expb 1120 . . . . 5 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด)) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ๐ต)
4847ralrimivva 3200 . . . 4 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ ๐ด โˆ€๐‘ โˆˆ ๐ด (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ๐ต)
49 eqid 2732 . . . . 5 (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))) = (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))
5049fmpo 8053 . . . 4 (โˆ€๐‘Ž โˆˆ ๐ด โˆ€๐‘ โˆˆ ๐ด (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ ๐ต โ†” (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))):(๐ด ร— ๐ด)โŸถ๐ต)
5148, 50sylib 217 . . 3 (๐œ‘ โ†’ (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))):(๐ด ร— ๐ด)โŸถ๐ต)
5217, 17mpoex 8065 . . . . 5 (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))) โˆˆ V
5352a1i 11 . . . 4 (๐œ‘ โ†’ (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))) โˆˆ V)
5451ffnd 6718 . . . 4 (๐œ‘ โ†’ (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))) Fn (๐ด ร— ๐ด))
5513fvexi 6905 . . . . 5 (0gโ€˜๐น) โˆˆ V
5655a1i 11 . . . 4 (๐œ‘ โ†’ (0gโ€˜๐น) โˆˆ V)
571, 2, 4, 8, 9, 10mnringbasefsuppd 42965 . . . . . 6 (๐œ‘ โ†’ ๐‘‹ finSupp (0gโ€˜๐‘…))
5857fsuppimpd 9368 . . . . 5 (๐œ‘ โ†’ (๐‘‹ supp (0gโ€˜๐‘…)) โˆˆ Fin)
591, 2, 4, 8, 9, 11mnringbasefsuppd 42965 . . . . . 6 (๐œ‘ โ†’ ๐‘Œ finSupp (0gโ€˜๐‘…))
6059fsuppimpd 9368 . . . . 5 (๐œ‘ โ†’ (๐‘Œ supp (0gโ€˜๐‘…)) โˆˆ Fin)
61 xpfi 9316 . . . . 5 (((๐‘‹ supp (0gโ€˜๐‘…)) โˆˆ Fin โˆง (๐‘Œ supp (0gโ€˜๐‘…)) โˆˆ Fin) โ†’ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆˆ Fin)
6258, 60, 61syl2anc 584 . . . 4 (๐œ‘ โ†’ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆˆ Fin)
63 elxpi 5698 . . . . . . 7 (๐‘ โˆˆ (๐ด ร— ๐ด) โ†’ โˆƒ๐‘Žโˆƒ๐‘(๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด)))
64 simpl 483 . . . . . . . 8 ((๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด)) โ†’ ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ)
65642eximi 1838 . . . . . . 7 (โˆƒ๐‘Žโˆƒ๐‘(๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด)) โ†’ โˆƒ๐‘Žโˆƒ๐‘ ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ)
6663, 65syl 17 . . . . . 6 (๐‘ โˆˆ (๐ด ร— ๐ด) โ†’ โˆƒ๐‘Žโˆƒ๐‘ ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ)
6766adantl 482 . . . . 5 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด)) โ†’ โˆƒ๐‘Žโˆƒ๐‘ ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ)
68 nfv 1917 . . . . . 6 โ„ฒ๐‘Ž(๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด))
69 nfv 1917 . . . . . . 7 โ„ฒ๐‘Ž ๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…)))
70 nfmpo1 7488 . . . . . . . . 9 โ„ฒ๐‘Ž(๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))
71 nfcv 2903 . . . . . . . . 9 โ„ฒ๐‘Ž๐‘
7270, 71nffv 6901 . . . . . . . 8 โ„ฒ๐‘Ž((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘)
73 nfcv 2903 . . . . . . . 8 โ„ฒ๐‘Ž(0gโ€˜๐น)
7472, 73nfeq 2916 . . . . . . 7 โ„ฒ๐‘Ž((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น)
7569, 74nfor 1907 . . . . . 6 โ„ฒ๐‘Ž(๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น))
76 nfv 1917 . . . . . . 7 โ„ฒ๐‘(๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด))
77 nfv 1917 . . . . . . . 8 โ„ฒ๐‘ ๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…)))
78 nfmpo2 7489 . . . . . . . . . 10 โ„ฒ๐‘(๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))
79 nfcv 2903 . . . . . . . . . 10 โ„ฒ๐‘๐‘
8078, 79nffv 6901 . . . . . . . . 9 โ„ฒ๐‘((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘)
81 nfcv 2903 . . . . . . . . 9 โ„ฒ๐‘(0gโ€˜๐น)
8280, 81nfeq 2916 . . . . . . . 8 โ„ฒ๐‘((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น)
8377, 82nfor 1907 . . . . . . 7 โ„ฒ๐‘(๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น))
84 simp3 1138 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ)
85 simp2 1137 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ ๐‘ โˆˆ (๐ด ร— ๐ด))
8684, 85eqeltrrd 2834 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ โŸจ๐‘Ž, ๐‘โŸฉ โˆˆ (๐ด ร— ๐ด))
87 opelxp 5712 . . . . . . . . . 10 (โŸจ๐‘Ž, ๐‘โŸฉ โˆˆ (๐ด ร— ๐ด) โ†” (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด))
8886, 87sylib 217 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด))
89 ianor 980 . . . . . . . . . . . . . . . 16 (ยฌ (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))) โ†” (ยฌ ๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆจ ยฌ ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))))
9022ffnd 6718 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐‘‹ Fn ๐ด)
9117a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐ด โˆˆ V)
924fvexi 6905 . . . . . . . . . . . . . . . . . . . . . . . 24 (0gโ€˜๐‘…) โˆˆ V
9392a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (0gโ€˜๐‘…) โˆˆ V)
94 elsuppfn 8155 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘‹ Fn ๐ด โˆง ๐ด โˆˆ V โˆง (0gโ€˜๐‘…) โˆˆ V) โ†’ (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โ†” (๐‘Ž โˆˆ ๐ด โˆง (๐‘‹โ€˜๐‘Ž) โ‰  (0gโ€˜๐‘…))))
9590, 91, 93, 94syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โ†” (๐‘Ž โˆˆ ๐ด โˆง (๐‘‹โ€˜๐‘Ž) โ‰  (0gโ€˜๐‘…))))
9695biimprd 247 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐‘Ž โˆˆ ๐ด โˆง (๐‘‹โ€˜๐‘Ž) โ‰  (0gโ€˜๐‘…)) โ†’ ๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…))))
97963ad2ant1 1133 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘Ž โˆˆ ๐ด โˆง (๐‘‹โ€˜๐‘Ž) โ‰  (0gโ€˜๐‘…)) โ†’ ๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…))))
9824, 97mpand 693 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘‹โ€˜๐‘Ž) โ‰  (0gโ€˜๐‘…) โ†’ ๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…))))
9998necon1bd 2958 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (ยฌ ๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โ†’ (๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…)))
10026ffnd 6718 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐‘Œ Fn ๐ด)
101 elsuppfn 8155 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘Œ Fn ๐ด โˆง ๐ด โˆˆ V โˆง (0gโ€˜๐‘…) โˆˆ V) โ†’ (๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…)) โ†” (๐‘ โˆˆ ๐ด โˆง (๐‘Œโ€˜๐‘) โ‰  (0gโ€˜๐‘…))))
102100, 91, 93, 101syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…)) โ†” (๐‘ โˆˆ ๐ด โˆง (๐‘Œโ€˜๐‘) โ‰  (0gโ€˜๐‘…))))
103102biimprd 247 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐‘ โˆˆ ๐ด โˆง (๐‘Œโ€˜๐‘) โ‰  (0gโ€˜๐‘…)) โ†’ ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))))
1041033ad2ant1 1133 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘ โˆˆ ๐ด โˆง (๐‘Œโ€˜๐‘) โ‰  (0gโ€˜๐‘…)) โ†’ ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))))
10528, 104mpand 693 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘Œโ€˜๐‘) โ‰  (0gโ€˜๐‘…) โ†’ ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))))
106105necon1bd 2958 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (ยฌ ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…)) โ†’ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…)))
10799, 106orim12d 963 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((ยฌ ๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆจ ยฌ ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))) โ†’ ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…))))
108107imp 407 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง (ยฌ ๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆจ ยฌ ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…)))) โ†’ ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…)))
10989, 108sylan2b 594 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ยฌ (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…)))) โ†’ ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…)))
110 oveq1 7415 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) = ((0gโ€˜๐‘…)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)))
11121, 3, 4ringlz 20106 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘… โˆˆ Ring โˆง (๐‘Œโ€˜๐‘) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((0gโ€˜๐‘…)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) = (0gโ€˜๐‘…))
11220, 29, 111syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((0gโ€˜๐‘…)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) = (0gโ€˜๐‘…))
113110, 112sylan9eqr 2794 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง (๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…)) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) = (0gโ€˜๐‘…))
114 oveq2 7416 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) = ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(0gโ€˜๐‘…)))
11521, 3, 4ringrz 20107 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘… โˆˆ Ring โˆง (๐‘‹โ€˜๐‘Ž) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
11620, 25, 115syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
117114, 116sylan9eqr 2794 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…)) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) = (0gโ€˜๐‘…))
118113, 117jaodan 956 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…))) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) = (0gโ€˜๐‘…))
119118adantr 481 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…))) โˆง ๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘)) โ†’ ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)) = (0gโ€˜๐‘…))
120 eqidd 2733 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…))) โˆง ยฌ ๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘)) โ†’ (0gโ€˜๐‘…) = (0gโ€˜๐‘…))
121119, 120ifeqda 4564 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…))) โ†’ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
122121mpteq2dv 5250 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…))) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (๐‘– โˆˆ ๐ด โ†ฆ (0gโ€˜๐‘…)))
123 fconstmpt 5738 . . . . . . . . . . . . . . . . . . 19 (๐ด ร— {(0gโ€˜๐‘…)}) = (๐‘– โˆˆ ๐ด โ†ฆ (0gโ€˜๐‘…))
1241, 4, 5, 8, 9mnring0g2d 42969 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ด ร— {(0gโ€˜๐‘…)}) = (0gโ€˜๐น))
125123, 124eqtr3id 2786 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘– โˆˆ ๐ด โ†ฆ (0gโ€˜๐‘…)) = (0gโ€˜๐น))
1261253ad2ant1 1133 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ (0gโ€˜๐‘…)) = (0gโ€˜๐น))
127126adantr 481 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…))) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ (0gโ€˜๐‘…)) = (0gโ€˜๐น))
128122, 127eqtrd 2772 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ((๐‘‹โ€˜๐‘Ž) = (0gโ€˜๐‘…) โˆจ (๐‘Œโ€˜๐‘) = (0gโ€˜๐‘…))) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (0gโ€˜๐น))
129109, 128syldan 591 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ยฌ (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…)))) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (0gโ€˜๐น))
130129ex 413 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (ยฌ (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (0gโ€˜๐น)))
131130orrd 861 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (0gโ€˜๐น)))
1321313expb 1120 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด)) โ†’ ((๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (0gโ€˜๐น)))
1331323adant3 1132 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ ((๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (0gโ€˜๐น)))
134 eleq1 2821 . . . . . . . . . . . . 13 (๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โ†” โŸจ๐‘Ž, ๐‘โŸฉ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…)))))
135 opelxp 5712 . . . . . . . . . . . . 13 (โŸจ๐‘Ž, ๐‘โŸฉ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โ†” (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))))
136134, 135bitrdi 286 . . . . . . . . . . . 12 (๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โ†” (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…)))))
1371363ad2ant3 1135 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โ†” (๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…)))))
138 simp2l 1199 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ ๐‘Ž โˆˆ ๐ด)
139 simp2r 1200 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ ๐‘ โˆˆ ๐ด)
140 eqidd 2733 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))) = (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))))
141 simp3 1138 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ)
14217mptex 7224 . . . . . . . . . . . . . . 15 (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ V
143142a1i 11 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) โˆˆ V)
144140, 141, 143fvmpopr2d 7568 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง ๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))
145138, 139, 144mpd3an23 1463 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))
146145eqeq1d 2734 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ (((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น) โ†” (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (0gโ€˜๐น)))
147137, 146orbi12d 917 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ ((๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น)) โ†” ((๐‘Ž โˆˆ (๐‘‹ supp (0gโ€˜๐‘…)) โˆง ๐‘ โˆˆ (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))) = (0gโ€˜๐น))))
148133, 147mpbird 256 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น)))
14988, 148syld3an2 1411 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด) โˆง ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ) โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น)))
1501493expia 1121 . . . . . . 7 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด)) โ†’ (๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น))))
15176, 83, 150exlimd 2211 . . . . . 6 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด)) โ†’ (โˆƒ๐‘ ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น))))
15268, 75, 151exlimd 2211 . . . . 5 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด)) โ†’ (โˆƒ๐‘Žโˆƒ๐‘ ๐‘ = โŸจ๐‘Ž, ๐‘โŸฉ โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น))))
15367, 152mpd 15 . . . 4 ((๐œ‘ โˆง ๐‘ โˆˆ (๐ด ร— ๐ด)) โ†’ (๐‘ โˆˆ ((๐‘‹ supp (0gโ€˜๐‘…)) ร— (๐‘Œ supp (0gโ€˜๐‘…))) โˆจ ((๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))โ€˜๐‘) = (0gโ€˜๐น)))
15453, 54, 56, 62, 153finnzfsuppd 42951 . . 3 (๐œ‘ โ†’ (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…)))) finSupp (0gโ€˜๐น))
1552, 13, 16, 19, 51, 154gsumcl 19782 . 2 (๐œ‘ โ†’ (๐น ฮฃg (๐‘Ž โˆˆ ๐ด, ๐‘ โˆˆ ๐ด โ†ฆ (๐‘– โˆˆ ๐ด โ†ฆ if(๐‘– = (๐‘Ž(+gโ€˜๐‘€)๐‘), ((๐‘‹โ€˜๐‘Ž)(.rโ€˜๐‘…)(๐‘Œโ€˜๐‘)), (0gโ€˜๐‘…))))) โˆˆ ๐ต)
15612, 155eqeltrd 2833 1 (๐œ‘ โ†’ (๐‘‹ ยท ๐‘Œ) โˆˆ ๐ต)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541  โˆƒwex 1781   โˆˆ wcel 2106   โ‰  wne 2940  โˆ€wral 3061  Vcvv 3474  ifcif 4528  {csn 4628  โŸจcop 4634   class class class wbr 5148   โ†ฆ cmpt 5231   ร— cxp 5674   Fn wfn 6538  โŸถwf 6539  โ€˜cfv 6543  (class class class)co 7408   โˆˆ cmpo 7410   supp csupp 8145   โ†‘m cmap 8819  Fincfn 8938   finSupp cfsupp 9360  Basecbs 17143  +gcplusg 17196  .rcmulr 17197  0gc0g 17384   ฮฃg cgsu 17385  CMndccmn 19647  Ringcrg 20055  LModclmod 20470   MndRing cmnring 42955
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-supp 8146  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-er 8702  df-map 8821  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-sup 9436  df-oi 9504  df-card 9933  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12472  df-z 12558  df-dec 12677  df-uz 12822  df-fz 13484  df-fzo 13627  df-seq 13966  df-hash 14290  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-hom 17220  df-cco 17221  df-0g 17386  df-gsum 17387  df-prds 17392  df-pws 17394  df-mgm 18560  df-sgrp 18609  df-mnd 18625  df-grp 18821  df-minusg 18822  df-sbg 18823  df-subg 19002  df-cntz 19180  df-cmn 19649  df-abl 19650  df-mgp 19987  df-ur 20004  df-ring 20057  df-subrg 20316  df-lmod 20472  df-lss 20542  df-sra 20784  df-rgmod 20785  df-dsmm 21286  df-frlm 21301  df-mnring 42956
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator