Step |
Hyp |
Ref |
Expression |
1 |
|
cntzi.p |
|- .+ = ( +g ` M ) |
2 |
|
cntzi.z |
|- Z = ( Cntz ` M ) |
3 |
|
eqid |
|- ( Base ` M ) = ( Base ` M ) |
4 |
3 2
|
cntzrcl |
|- ( X e. ( Z ` S ) -> ( M e. _V /\ S C_ ( Base ` M ) ) ) |
5 |
3 1 2
|
elcntz |
|- ( S C_ ( Base ` M ) -> ( X e. ( Z ` S ) <-> ( X e. ( Base ` M ) /\ A. y e. S ( X .+ y ) = ( y .+ X ) ) ) ) |
6 |
4 5
|
simpl2im |
|- ( X e. ( Z ` S ) -> ( X e. ( Z ` S ) <-> ( X e. ( Base ` M ) /\ A. y e. S ( X .+ y ) = ( y .+ X ) ) ) ) |
7 |
6
|
simplbda |
|- ( ( X e. ( Z ` S ) /\ X e. ( Z ` S ) ) -> A. y e. S ( X .+ y ) = ( y .+ X ) ) |
8 |
7
|
anidms |
|- ( X e. ( Z ` S ) -> A. y e. S ( X .+ y ) = ( y .+ X ) ) |
9 |
|
oveq2 |
|- ( y = Y -> ( X .+ y ) = ( X .+ Y ) ) |
10 |
|
oveq1 |
|- ( y = Y -> ( y .+ X ) = ( Y .+ X ) ) |
11 |
9 10
|
eqeq12d |
|- ( y = Y -> ( ( X .+ y ) = ( y .+ X ) <-> ( X .+ Y ) = ( Y .+ X ) ) ) |
12 |
11
|
rspccva |
|- ( ( A. y e. S ( X .+ y ) = ( y .+ X ) /\ Y e. S ) -> ( X .+ Y ) = ( Y .+ X ) ) |
13 |
8 12
|
sylan |
|- ( ( X e. ( Z ` S ) /\ Y e. S ) -> ( X .+ Y ) = ( Y .+ X ) ) |