Metamath Proof Explorer

Theorem mhmmnd

Description: The image of a monoid G under a monoid homomorphism F is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020)

Ref Expression
Hypotheses ghmgrp.f 
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
ghmgrp.x 
|- X = ( Base ` G )
ghmgrp.y 
|- Y = ( Base ` H )
ghmgrp.p 
|- .+ = ( +g ` G )
ghmgrp.q 
|- .+^ = ( +g ` H )
ghmgrp.1 
|- ( ph -> F : X -onto-> Y )
mhmmnd.3 
|- ( ph -> G e. Mnd )
Assertion mhmmnd 
|- ( ph -> H e. Mnd )

Proof

Step Hyp Ref Expression
1 ghmgrp.f 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
2 ghmgrp.x 
 |-  X = ( Base ` G )
3 ghmgrp.y 
 |-  Y = ( Base ` H )
4 ghmgrp.p 
 |-  .+ = ( +g ` G )
5 ghmgrp.q 
 |-  .+^ = ( +g ` H )
6 ghmgrp.1 
 |-  ( ph -> F : X -onto-> Y )
7 mhmmnd.3 
 |-  ( ph -> G e. Mnd )
8 simpllr 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( F ` i ) = a )
9 simpr 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( F ` j ) = b )
10 8 9 oveq12d 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( ( F ` i ) .+^ ( F ` j ) ) = ( a .+^ b ) )
11 simp-5l 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ph )
12 11 1 syl3an1 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
13 simp-4r 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> i e. X )
14 simplr 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> j e. X )
15 12 13 14 mhmlem 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( F ` ( i .+ j ) ) = ( ( F ` i ) .+^ ( F ` j ) ) )
16 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
17 6 16 syl 
 |-  ( ph -> F : X --> Y )
18 17 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> F : X --> Y )
19 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> G e. Mnd )
20 2 4 mndcl 
 |-  ( ( G e. Mnd /\ i e. X /\ j e. X ) -> ( i .+ j ) e. X )
21 19 13 14 20 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( i .+ j ) e. X )
22 18 21 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( F ` ( i .+ j ) ) e. Y )
23 15 22 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( ( F ` i ) .+^ ( F ` j ) ) e. Y )
24 10 23 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( a .+^ b ) e. Y )
25 simpr 
 |-  ( ( a e. Y /\ b e. Y ) -> b e. Y )
26 foelcdmi 
 |-  ( ( F : X -onto-> Y /\ b e. Y ) -> E. j e. X ( F ` j ) = b )
27 6 25 26 syl2an 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y ) ) -> E. j e. X ( F ` j ) = b )
28 27 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) -> E. j e. X ( F ` j ) = b )
29 24 28 r19.29a 
 |-  ( ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( a .+^ b ) e. Y )
30 simpl 
 |-  ( ( a e. Y /\ b e. Y ) -> a e. Y )
31 foelcdmi 
 |-  ( ( F : X -onto-> Y /\ a e. Y ) -> E. i e. X ( F ` i ) = a )
32 6 30 31 syl2an 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y ) ) -> E. i e. X ( F ` i ) = a )
33 29 32 r19.29a 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y ) ) -> ( a .+^ b ) e. Y )
34 simpll 
 |-  ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ c e. Y ) -> ph )
35 simplrl 
 |-  ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ c e. Y ) -> a e. Y )
36 simplrr 
 |-  ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ c e. Y ) -> b e. Y )
37 simpr 
 |-  ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ c e. Y ) -> c e. Y )
38 7 ad2antrr 
 |-  ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) -> G e. Mnd )
39 38 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> G e. Mnd )
40 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> i e. X )
41 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> j e. X )
42 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> k e. X )
43 2 4 mndass 
 |-  ( ( G e. Mnd /\ ( i e. X /\ j e. X /\ k e. X ) ) -> ( ( i .+ j ) .+ k ) = ( i .+ ( j .+ k ) ) )
44 39 40 41 42 43 syl13anc 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( i .+ j ) .+ k ) = ( i .+ ( j .+ k ) ) )
45 44 fveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( F ` ( ( i .+ j ) .+ k ) ) = ( F ` ( i .+ ( j .+ k ) ) ) )
46 simp-7l 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ph )
47 46 1 syl3an1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
48 39 40 41 20 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( i .+ j ) e. X )
49 47 48 42 mhmlem 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( F ` ( ( i .+ j ) .+ k ) ) = ( ( F ` ( i .+ j ) ) .+^ ( F ` k ) ) )
50 2 4 mndcl 
 |-  ( ( G e. Mnd /\ j e. X /\ k e. X ) -> ( j .+ k ) e. X )
51 39 41 42 50 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( j .+ k ) e. X )
52 47 40 51 mhmlem 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( F ` ( i .+ ( j .+ k ) ) ) = ( ( F ` i ) .+^ ( F ` ( j .+ k ) ) ) )
53 45 49 52 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( F ` ( i .+ j ) ) .+^ ( F ` k ) ) = ( ( F ` i ) .+^ ( F ` ( j .+ k ) ) ) )
54 simp1 
 |-  ( ( ph /\ i e. X /\ j e. X ) -> ph )
55 54 1 syl3an1 
 |-  ( ( ( ph /\ i e. X /\ j e. X ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
56 simp2 
 |-  ( ( ph /\ i e. X /\ j e. X ) -> i e. X )
57 simp3 
 |-  ( ( ph /\ i e. X /\ j e. X ) -> j e. X )
58 55 56 57 mhmlem 
 |-  ( ( ph /\ i e. X /\ j e. X ) -> ( F ` ( i .+ j ) ) = ( ( F ` i ) .+^ ( F ` j ) ) )
59 46 40 41 58 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( F ` ( i .+ j ) ) = ( ( F ` i ) .+^ ( F ` j ) ) )
60 59 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( F ` ( i .+ j ) ) .+^ ( F ` k ) ) = ( ( ( F ` i ) .+^ ( F ` j ) ) .+^ ( F ` k ) ) )
61 47 41 42 mhmlem 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( F ` ( j .+ k ) ) = ( ( F ` j ) .+^ ( F ` k ) ) )
62 61 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( F ` i ) .+^ ( F ` ( j .+ k ) ) ) = ( ( F ` i ) .+^ ( ( F ` j ) .+^ ( F ` k ) ) ) )
63 53 60 62 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( ( F ` i ) .+^ ( F ` j ) ) .+^ ( F ` k ) ) = ( ( F ` i ) .+^ ( ( F ` j ) .+^ ( F ` k ) ) ) )
64 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( F ` i ) = a )
65 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( F ` j ) = b )
66 64 65 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( F ` i ) .+^ ( F ` j ) ) = ( a .+^ b ) )
67 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( F ` k ) = c )
68 66 67 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( ( F ` i ) .+^ ( F ` j ) ) .+^ ( F ` k ) ) = ( ( a .+^ b ) .+^ c ) )
69 65 67 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( F ` j ) .+^ ( F ` k ) ) = ( b .+^ c ) )
70 64 69 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( F ` i ) .+^ ( ( F ` j ) .+^ ( F ` k ) ) ) = ( a .+^ ( b .+^ c ) ) )
71 63 68 70 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) /\ k e. X ) /\ ( F ` k ) = c ) -> ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) )
72 foelcdmi 
 |-  ( ( F : X -onto-> Y /\ c e. Y ) -> E. k e. X ( F ` k ) = c )
73 6 72 sylan 
 |-  ( ( ph /\ c e. Y ) -> E. k e. X ( F ` k ) = c )
74 73 3ad2antr3 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) -> E. k e. X ( F ` k ) = c )
75 74 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> E. k e. X ( F ` k ) = c )
76 71 75 r19.29a 
 |-  ( ( ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) /\ j e. X ) /\ ( F ` j ) = b ) -> ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) )
77 27 3adantr3 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) -> E. j e. X ( F ` j ) = b )
78 77 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) -> E. j e. X ( F ` j ) = b )
79 76 78 r19.29a 
 |-  ( ( ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) )
80 32 3adantr3 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) -> E. i e. X ( F ` i ) = a )
81 79 80 r19.29a 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y /\ c e. Y ) ) -> ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) )
82 34 35 36 37 81 syl13anc 
 |-  ( ( ( ph /\ ( a e. Y /\ b e. Y ) ) /\ c e. Y ) -> ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) )
83 82 ralrimiva 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y ) ) -> A. c e. Y ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) )
84 33 83 jca 
 |-  ( ( ph /\ ( a e. Y /\ b e. Y ) ) -> ( ( a .+^ b ) e. Y /\ A. c e. Y ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) ) )
85 84 ralrimivva 
 |-  ( ph -> A. a e. Y A. b e. Y ( ( a .+^ b ) e. Y /\ A. c e. Y ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) ) )
86 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
87 2 86 mndidcl 
 |-  ( G e. Mnd -> ( 0g ` G ) e. X )
88 7 87 syl 
 |-  ( ph -> ( 0g ` G ) e. X )
89 17 88 ffvelcdmd 
 |-  ( ph -> ( F ` ( 0g ` G ) ) e. Y )
90 simplll 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ph )
91 90 1 syl3an1 
 |-  ( ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
92 7 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> G e. Mnd )
93 92 87 syl 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( 0g ` G ) e. X )
94 simplr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> i e. X )
95 91 93 94 mhmlem 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( 0g ` G ) .+ i ) ) = ( ( F ` ( 0g ` G ) ) .+^ ( F ` i ) ) )
96 2 4 86 mndlid 
 |-  ( ( G e. Mnd /\ i e. X ) -> ( ( 0g ` G ) .+ i ) = i )
97 92 94 96 syl2anc 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( 0g ` G ) .+ i ) = i )
98 97 fveq2d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( 0g ` G ) .+ i ) ) = ( F ` i ) )
99 95 98 eqtr3d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` ( 0g ` G ) ) .+^ ( F ` i ) ) = ( F ` i ) )
100 simpr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` i ) = a )
101 100 oveq2d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` ( 0g ` G ) ) .+^ ( F ` i ) ) = ( ( F ` ( 0g ` G ) ) .+^ a ) )
102 99 101 100 3eqtr3d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` ( 0g ` G ) ) .+^ a ) = a )
103 91 94 93 mhmlem 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( i .+ ( 0g ` G ) ) ) = ( ( F ` i ) .+^ ( F ` ( 0g ` G ) ) ) )
104 2 4 86 mndrid 
 |-  ( ( G e. Mnd /\ i e. X ) -> ( i .+ ( 0g ` G ) ) = i )
105 92 94 104 syl2anc 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( i .+ ( 0g ` G ) ) = i )
106 105 fveq2d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( i .+ ( 0g ` G ) ) ) = ( F ` i ) )
107 103 106 eqtr3d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` i ) .+^ ( F ` ( 0g ` G ) ) ) = ( F ` i ) )
108 100 oveq1d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` i ) .+^ ( F ` ( 0g ` G ) ) ) = ( a .+^ ( F ` ( 0g ` G ) ) ) )
109 107 108 100 3eqtr3d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( a .+^ ( F ` ( 0g ` G ) ) ) = a )
110 102 109 jca 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( ( F ` ( 0g ` G ) ) .+^ a ) = a /\ ( a .+^ ( F ` ( 0g ` G ) ) ) = a ) )
111 6 31 sylan 
 |-  ( ( ph /\ a e. Y ) -> E. i e. X ( F ` i ) = a )
112 110 111 r19.29a 
 |-  ( ( ph /\ a e. Y ) -> ( ( ( F ` ( 0g ` G ) ) .+^ a ) = a /\ ( a .+^ ( F ` ( 0g ` G ) ) ) = a ) )
113 112 ralrimiva 
 |-  ( ph -> A. a e. Y ( ( ( F ` ( 0g ` G ) ) .+^ a ) = a /\ ( a .+^ ( F ` ( 0g ` G ) ) ) = a ) )
114 oveq1 
 |-  ( d = ( F ` ( 0g ` G ) ) -> ( d .+^ a ) = ( ( F ` ( 0g ` G ) ) .+^ a ) )
115 114 eqeq1d 
 |-  ( d = ( F ` ( 0g ` G ) ) -> ( ( d .+^ a ) = a <-> ( ( F ` ( 0g ` G ) ) .+^ a ) = a ) )
116 115 ovanraleqv 
 |-  ( d = ( F ` ( 0g ` G ) ) -> ( A. a e. Y ( ( d .+^ a ) = a /\ ( a .+^ d ) = a ) <-> A. a e. Y ( ( ( F ` ( 0g ` G ) ) .+^ a ) = a /\ ( a .+^ ( F ` ( 0g ` G ) ) ) = a ) ) )
117 116 rspcev 
 |-  ( ( ( F ` ( 0g ` G ) ) e. Y /\ A. a e. Y ( ( ( F ` ( 0g ` G ) ) .+^ a ) = a /\ ( a .+^ ( F ` ( 0g ` G ) ) ) = a ) ) -> E. d e. Y A. a e. Y ( ( d .+^ a ) = a /\ ( a .+^ d ) = a ) )
118 89 113 117 syl2anc 
 |-  ( ph -> E. d e. Y A. a e. Y ( ( d .+^ a ) = a /\ ( a .+^ d ) = a ) )
119 3 5 ismnd 
 |-  ( H e. Mnd <-> ( A. a e. Y A. b e. Y ( ( a .+^ b ) e. Y /\ A. c e. Y ( ( a .+^ b ) .+^ c ) = ( a .+^ ( b .+^ c ) ) ) /\ E. d e. Y A. a e. Y ( ( d .+^ a ) = a /\ ( a .+^ d ) = a ) ) )
120 85 118 119 sylanbrc 
 |-  ( ph -> H e. Mnd )