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 |
|
oveq1 |
|- ( y = n -> ( y .+ x ) = ( n .+ x ) ) |
7 |
6
|
eqeq1d |
|- ( y = n -> ( ( y .+ x ) = O <-> ( n .+ x ) = O ) ) |
8 |
7
|
cbvrexvw |
|- ( E. y e. B ( y .+ x ) = O <-> E. n e. B ( n .+ x ) = O ) |
9 |
5 8
|
sylib |
|- ( ( ph /\ x e. B ) -> E. n e. B ( n .+ x ) = O ) |
10 |
4
|
caovassg |
|- ( ( ph /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) ) |
11 |
10
|
adantlr |
|- ( ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) ) |
12 |
|
simprl |
|- ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> x e. B ) |
13 |
|
simprrl |
|- ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> n e. B ) |
14 |
11 12 13 12
|
caovassd |
|- ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( ( x .+ n ) .+ x ) = ( x .+ ( n .+ x ) ) ) |
15 |
|
simprrr |
|- ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( n .+ x ) = O ) |
16 |
1 2 3 4 5 12 13 15
|
grprinvd |
|- ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( x .+ n ) = O ) |
17 |
16
|
oveq1d |
|- ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( ( x .+ n ) .+ x ) = ( O .+ x ) ) |
18 |
15
|
oveq2d |
|- ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( x .+ ( n .+ x ) ) = ( x .+ O ) ) |
19 |
14 17 18
|
3eqtr3d |
|- ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( O .+ x ) = ( x .+ O ) ) |
20 |
19
|
anassrs |
|- ( ( ( ph /\ x e. B ) /\ ( n e. B /\ ( n .+ x ) = O ) ) -> ( O .+ x ) = ( x .+ O ) ) |
21 |
9 20
|
rexlimddv |
|- ( ( ph /\ x e. B ) -> ( O .+ x ) = ( x .+ O ) ) |
22 |
21 3
|
eqtr3d |
|- ( ( ph /\ x e. B ) -> ( x .+ O ) = x ) |