This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cntzi

Description: Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses cntzi.p 
|- .+ = ( +g ` M )
cntzi.z 
|- Z = ( Cntz ` M )
Assertion cntzi 
|- ( ( X e. ( Z ` S ) /\ Y e. S ) -> ( X .+ Y ) = ( Y .+ X ) )

Proof

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 ) )