Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwssub Structured version   Unicode version

Theorem pwssub 16309
 Description: Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015.)
Hypotheses
Ref Expression
pwsgrp.y s
pwsinvg.b
pwssub.m
pwssub.n
Assertion
Ref Expression
pwssub

Proof of Theorem pwssub
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 755 . . . 4
2 pwsgrp.y . . . . . 6 s
3 eqid 2457 . . . . . 6
4 pwsinvg.b . . . . . 6
5 simpll 753 . . . . . 6
6 simprl 756 . . . . . 6
72, 3, 4, 5, 1, 6pwselbas 14905 . . . . 5
87ffvelrnda 6032 . . . 4
9 fvex 5882 . . . . 5
109a1i 11 . . . 4
117feqmptd 5926 . . . 4
12 simprr 757 . . . . . 6
13 eqid 2457 . . . . . . 7
14 eqid 2457 . . . . . . 7
152, 4, 13, 14pwsinvg 16308 . . . . . 6
165, 1, 12, 15syl3anc 1228 . . . . 5
172, 3, 4, 5, 1, 12pwselbas 14905 . . . . . . 7
1817ffvelrnda 6032 . . . . . 6
1917feqmptd 5926 . . . . . 6
203, 13grpinvf 16220 . . . . . . . 8
2120ad2antrr 725 . . . . . . 7
2221feqmptd 5926 . . . . . 6
23 fveq2 5872 . . . . . 6
2418, 19, 22, 23fmptco 6065 . . . . 5
2516, 24eqtrd 2498 . . . 4
261, 8, 10, 11, 25offval2 6555 . . 3
272pwsgrp 16307 . . . . . 6
2827adantr 465 . . . . 5
294, 14grpinvcl 16221 . . . . 5
3028, 12, 29syl2anc 661 . . . 4
31 eqid 2457 . . . 4
32 eqid 2457 . . . 4
332, 4, 5, 1, 6, 30, 31, 32pwsplusgval 14906 . . 3
34 pwssub.m . . . . . 6
353, 31, 13, 34grpsubval 16219 . . . . 5
368, 18, 35syl2anc 661 . . . 4
3736mpteq2dva 4543 . . 3
3826, 33, 373eqtr4d 2508 . 2
39 pwssub.n . . . 4
404, 32, 14, 39grpsubval 16219 . . 3