Step |
Hyp |
Ref |
Expression |
1 |
|
grprinvlem.c |
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B ) |
2 |
|
grprinvlem.o |
|- ( ph -> O e. B ) |
3 |
|
grprinvlem.i |
|- ( ( ph /\ x e. B ) -> ( O .+ x ) = x ) |
4 |
|
grprinvlem.a |
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) |
5 |
|
grprinvlem.n |
|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O ) |
6 |
|
grprinvlem.x |
|- ( ( ph /\ ps ) -> X e. B ) |
7 |
|
grprinvlem.e |
|- ( ( ph /\ ps ) -> ( X .+ X ) = X ) |
8 |
5
|
ralrimiva |
|- ( ph -> A. x e. B E. y e. B ( y .+ x ) = O ) |
9 |
|
oveq2 |
|- ( x = z -> ( y .+ x ) = ( y .+ z ) ) |
10 |
9
|
eqeq1d |
|- ( x = z -> ( ( y .+ x ) = O <-> ( y .+ z ) = O ) ) |
11 |
10
|
rexbidv |
|- ( x = z -> ( E. y e. B ( y .+ x ) = O <-> E. y e. B ( y .+ z ) = O ) ) |
12 |
11
|
cbvralvw |
|- ( A. x e. B E. y e. B ( y .+ x ) = O <-> A. z e. B E. y e. B ( y .+ z ) = O ) |
13 |
8 12
|
sylib |
|- ( ph -> A. z e. B E. y e. B ( y .+ z ) = O ) |
14 |
|
oveq2 |
|- ( z = X -> ( y .+ z ) = ( y .+ X ) ) |
15 |
14
|
eqeq1d |
|- ( z = X -> ( ( y .+ z ) = O <-> ( y .+ X ) = O ) ) |
16 |
15
|
rexbidv |
|- ( z = X -> ( E. y e. B ( y .+ z ) = O <-> E. y e. B ( y .+ X ) = O ) ) |
17 |
16
|
rspccva |
|- ( ( A. z e. B E. y e. B ( y .+ z ) = O /\ X e. B ) -> E. y e. B ( y .+ X ) = O ) |
18 |
13 6 17
|
syl2an2r |
|- ( ( ph /\ ps ) -> E. y e. B ( y .+ X ) = O ) |
19 |
7
|
oveq2d |
|- ( ( ph /\ ps ) -> ( y .+ ( X .+ X ) ) = ( y .+ X ) ) |
20 |
19
|
adantr |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> ( y .+ ( X .+ X ) ) = ( y .+ X ) ) |
21 |
|
simprr |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> ( y .+ X ) = O ) |
22 |
21
|
oveq1d |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> ( ( y .+ X ) .+ X ) = ( O .+ X ) ) |
23 |
4
|
caovassg |
|- ( ( ph /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) ) |
24 |
23
|
ad4ant14 |
|- ( ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) ) |
25 |
|
simprl |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> y e. B ) |
26 |
6
|
adantr |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> X e. B ) |
27 |
24 25 26 26
|
caovassd |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> ( ( y .+ X ) .+ X ) = ( y .+ ( X .+ X ) ) ) |
28 |
|
oveq2 |
|- ( y = X -> ( O .+ y ) = ( O .+ X ) ) |
29 |
|
id |
|- ( y = X -> y = X ) |
30 |
28 29
|
eqeq12d |
|- ( y = X -> ( ( O .+ y ) = y <-> ( O .+ X ) = X ) ) |
31 |
3
|
ralrimiva |
|- ( ph -> A. x e. B ( O .+ x ) = x ) |
32 |
|
oveq2 |
|- ( x = y -> ( O .+ x ) = ( O .+ y ) ) |
33 |
|
id |
|- ( x = y -> x = y ) |
34 |
32 33
|
eqeq12d |
|- ( x = y -> ( ( O .+ x ) = x <-> ( O .+ y ) = y ) ) |
35 |
34
|
cbvralvw |
|- ( A. x e. B ( O .+ x ) = x <-> A. y e. B ( O .+ y ) = y ) |
36 |
31 35
|
sylib |
|- ( ph -> A. y e. B ( O .+ y ) = y ) |
37 |
36
|
adantr |
|- ( ( ph /\ ps ) -> A. y e. B ( O .+ y ) = y ) |
38 |
30 37 6
|
rspcdva |
|- ( ( ph /\ ps ) -> ( O .+ X ) = X ) |
39 |
38
|
adantr |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> ( O .+ X ) = X ) |
40 |
22 27 39
|
3eqtr3d |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> ( y .+ ( X .+ X ) ) = X ) |
41 |
20 40 21
|
3eqtr3d |
|- ( ( ( ph /\ ps ) /\ ( y e. B /\ ( y .+ X ) = O ) ) -> X = O ) |
42 |
18 41
|
rexlimddv |
|- ( ( ph /\ ps ) -> X = O ) |