Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ressmulgnn0 Structured version   Unicode version

Theorem ressmulgnn0 26062
 Description: Values for the group multiple function in a restricted structure (Contributed by Thierry Arnoux, 14-Jun-2017.)
Hypotheses
Ref Expression
ressmulgnn.1 s
ressmulgnn.2
ressmulgnn.3 .g
ressmulgnn.4
ressmulgnn0.4
Assertion
Ref Expression
ressmulgnn0 .g

Proof of Theorem ressmulgnn0
StepHypRef Expression
1 simpr 458 . . 3
2 simplr 749 . . 3
3 ressmulgnn.1 . . . 4 s
4 ressmulgnn.2 . . . 4
5 ressmulgnn.3 . . . 4 .g
6 ressmulgnn.4 . . . 4
73, 4, 5, 6ressmulgnn 26061 . . 3 .g
81, 2, 7syl2anc 656 . 2 .g
9 simplr 749 . . . . 5
10 eqid 2441 . . . . . . . 8
113, 10ressbas2 14225 . . . . . . 7
124, 11ax-mp 5 . . . . . 6
13 ressmulgnn0.4 . . . . . 6
14 eqid 2441 . . . . . 6 .g .g
1512, 13, 14mulg0 15625 . . . . 5 .g
169, 15syl 16 . . . 4 .g
17 simpr 458 . . . . 5
1817oveq1d 6105 . . . 4 .g .g
194, 9sseldi 3351 . . . . 5
20 eqid 2441 . . . . . 6
2110, 20, 5mulg0 15625 . . . . 5
2219, 21syl 16 . . . 4
2316, 18, 223eqtr4d 2483 . . 3 .g
2417oveq1d 6105 . . 3
2523, 24eqtr4d 2476 . 2 .g
26 elnn0 10577 . . . 4
2726biimpi 194 . . 3