Step |
Hyp |
Ref |
Expression |
1 |
|
issubmnd.b |
|- B = ( Base ` G ) |
2 |
|
issubmnd.p |
|- .+ = ( +g ` G ) |
3 |
|
issubmnd.z |
|- .0. = ( 0g ` G ) |
4 |
|
issubmnd.h |
|- H = ( G |`s S ) |
5 |
|
simplr |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> H e. Mnd ) |
6 |
|
simprl |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> x e. S ) |
7 |
|
simpll2 |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> S C_ B ) |
8 |
4 1
|
ressbas2 |
|- ( S C_ B -> S = ( Base ` H ) ) |
9 |
7 8
|
syl |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> S = ( Base ` H ) ) |
10 |
6 9
|
eleqtrd |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> x e. ( Base ` H ) ) |
11 |
|
simprr |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> y e. S ) |
12 |
11 9
|
eleqtrd |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> y e. ( Base ` H ) ) |
13 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
14 |
|
eqid |
|- ( +g ` H ) = ( +g ` H ) |
15 |
13 14
|
mndcl |
|- ( ( H e. Mnd /\ x e. ( Base ` H ) /\ y e. ( Base ` H ) ) -> ( x ( +g ` H ) y ) e. ( Base ` H ) ) |
16 |
5 10 12 15
|
syl3anc |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` H ) y ) e. ( Base ` H ) ) |
17 |
1
|
fvexi |
|- B e. _V |
18 |
17
|
ssex |
|- ( S C_ B -> S e. _V ) |
19 |
18
|
3ad2ant2 |
|- ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) -> S e. _V ) |
20 |
4 2
|
ressplusg |
|- ( S e. _V -> .+ = ( +g ` H ) ) |
21 |
19 20
|
syl |
|- ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) -> .+ = ( +g ` H ) ) |
22 |
21
|
ad2antrr |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> .+ = ( +g ` H ) ) |
23 |
22
|
oveqd |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( x ( +g ` H ) y ) ) |
24 |
16 23 9
|
3eltr4d |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S ) |
25 |
24
|
ralrimivva |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ H e. Mnd ) -> A. x e. S A. y e. S ( x .+ y ) e. S ) |
26 |
|
simpl2 |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> S C_ B ) |
27 |
26 8
|
syl |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> S = ( Base ` H ) ) |
28 |
21
|
adantr |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> .+ = ( +g ` H ) ) |
29 |
|
ovrspc2v |
|- ( ( ( u e. S /\ v e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> ( u .+ v ) e. S ) |
30 |
29
|
ancoms |
|- ( ( A. x e. S A. y e. S ( x .+ y ) e. S /\ ( u e. S /\ v e. S ) ) -> ( u .+ v ) e. S ) |
31 |
30
|
3impb |
|- ( ( A. x e. S A. y e. S ( x .+ y ) e. S /\ u e. S /\ v e. S ) -> ( u .+ v ) e. S ) |
32 |
31
|
3adant1l |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) /\ u e. S /\ v e. S ) -> ( u .+ v ) e. S ) |
33 |
|
simpl1 |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> G e. Mnd ) |
34 |
26
|
sseld |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> ( u e. S -> u e. B ) ) |
35 |
26
|
sseld |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> ( v e. S -> v e. B ) ) |
36 |
26
|
sseld |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> ( w e. S -> w e. B ) ) |
37 |
34 35 36
|
3anim123d |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> ( ( u e. S /\ v e. S /\ w e. S ) -> ( u e. B /\ v e. B /\ w e. B ) ) ) |
38 |
37
|
imp |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) /\ ( u e. S /\ v e. S /\ w e. S ) ) -> ( u e. B /\ v e. B /\ w e. B ) ) |
39 |
1 2
|
mndass |
|- ( ( G e. Mnd /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) ) |
40 |
33 38 39
|
syl2an2r |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) /\ ( u e. S /\ v e. S /\ w e. S ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) ) |
41 |
|
simpl3 |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> .0. e. S ) |
42 |
26
|
sselda |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) /\ u e. S ) -> u e. B ) |
43 |
1 2 3
|
mndlid |
|- ( ( G e. Mnd /\ u e. B ) -> ( .0. .+ u ) = u ) |
44 |
33 42 43
|
syl2an2r |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) /\ u e. S ) -> ( .0. .+ u ) = u ) |
45 |
1 2 3
|
mndrid |
|- ( ( G e. Mnd /\ u e. B ) -> ( u .+ .0. ) = u ) |
46 |
33 42 45
|
syl2an2r |
|- ( ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) /\ u e. S ) -> ( u .+ .0. ) = u ) |
47 |
27 28 32 40 41 44 46
|
ismndd |
|- ( ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> H e. Mnd ) |
48 |
25 47
|
impbida |
|- ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) -> ( H e. Mnd <-> A. x e. S A. y e. S ( x .+ y ) e. S ) ) |