Metamath Proof Explorer

Theorem resscntz

Description: Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses resscntz.p 
|- H = ( G |`s A )
resscntz.z 
|- Z = ( Cntz ` G )
resscntz.y 
|- Y = ( Cntz ` H )
Assertion resscntz 
|- ( ( A e. V /\ S C_ A ) -> ( Y ` S ) = ( ( Z ` S ) i^i A ) )

Proof

Step Hyp Ref Expression
1 resscntz.p 
 |-  H = ( G |`s A )
2 resscntz.z 
 |-  Z = ( Cntz ` G )
3 resscntz.y 
 |-  Y = ( Cntz ` H )
4 eqid 
 |-  ( Base ` H ) = ( Base ` H )
5 4 3 cntzrcl 
 |-  ( x e. ( Y ` S ) -> ( H e. _V /\ S C_ ( Base ` H ) ) )
6 5 simprd 
 |-  ( x e. ( Y ` S ) -> S C_ ( Base ` H ) )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 1 7 ressbasss 
 |-  ( Base ` H ) C_ ( Base ` G )
9 6 8 sstrdi 
 |-  ( x e. ( Y ` S ) -> S C_ ( Base ` G ) )
10 9 a1i 
 |-  ( ( A e. V /\ S C_ A ) -> ( x e. ( Y ` S ) -> S C_ ( Base ` G ) ) )
11 elinel1 
 |-  ( x e. ( ( Z ` S ) i^i A ) -> x e. ( Z ` S ) )
12 7 2 cntzrcl 
 |-  ( x e. ( Z ` S ) -> ( G e. _V /\ S C_ ( Base ` G ) ) )
13 12 simprd 
 |-  ( x e. ( Z ` S ) -> S C_ ( Base ` G ) )
14 11 13 syl 
 |-  ( x e. ( ( Z ` S ) i^i A ) -> S C_ ( Base ` G ) )
15 14 a1i 
 |-  ( ( A e. V /\ S C_ A ) -> ( x e. ( ( Z ` S ) i^i A ) -> S C_ ( Base ` G ) ) )
16 elin 
 |-  ( x e. ( A i^i ( Base ` G ) ) <-> ( x e. A /\ x e. ( Base ` G ) ) )
17 1 7 ressbas 
 |-  ( A e. V -> ( A i^i ( Base ` G ) ) = ( Base ` H ) )
18 17 eleq2d 
 |-  ( A e. V -> ( x e. ( A i^i ( Base ` G ) ) <-> x e. ( Base ` H ) ) )
19 16 18 bitr3id 
 |-  ( A e. V -> ( ( x e. A /\ x e. ( Base ` G ) ) <-> x e. ( Base ` H ) ) )
20 eqid 
 |-  ( +g ` G ) = ( +g ` G )
21 1 20 ressplusg 
 |-  ( A e. V -> ( +g ` G ) = ( +g ` H ) )
22 21 oveqd 
 |-  ( A e. V -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
23 21 oveqd 
 |-  ( A e. V -> ( y ( +g ` G ) x ) = ( y ( +g ` H ) x ) )
24 22 23 eqeq12d 
 |-  ( A e. V -> ( ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
25 24 ralbidv 
 |-  ( A e. V -> ( A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> A. y e. S ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
26 19 25 anbi12d 
 |-  ( A e. V -> ( ( ( x e. A /\ x e. ( Base ` G ) ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) <-> ( x e. ( Base ` H ) /\ A. y e. S ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) ) )
27 26 ad2antrr 
 |-  ( ( ( A e. V /\ S C_ A ) /\ S C_ ( Base ` G ) ) -> ( ( ( x e. A /\ x e. ( Base ` G ) ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) <-> ( x e. ( Base ` H ) /\ A. y e. S ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) ) )
28 anass 
 |-  ( ( ( x e. A /\ x e. ( Base ` G ) ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) <-> ( x e. A /\ ( x e. ( Base ` G ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
29 27 28 bitr3di 
 |-  ( ( ( A e. V /\ S C_ A ) /\ S C_ ( Base ` G ) ) -> ( ( x e. ( Base ` H ) /\ A. y e. S ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) <-> ( x e. A /\ ( x e. ( Base ` G ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) ) )
30 ssin 
 |-  ( ( S C_ A /\ S C_ ( Base ` G ) ) <-> S C_ ( A i^i ( Base ` G ) ) )
31 17 sseq2d 
 |-  ( A e. V -> ( S C_ ( A i^i ( Base ` G ) ) <-> S C_ ( Base ` H ) ) )
32 30 31 syl5bb 
 |-  ( A e. V -> ( ( S C_ A /\ S C_ ( Base ` G ) ) <-> S C_ ( Base ` H ) ) )
33 32 biimpd 
 |-  ( A e. V -> ( ( S C_ A /\ S C_ ( Base ` G ) ) -> S C_ ( Base ` H ) ) )
34 33 impl 
 |-  ( ( ( A e. V /\ S C_ A ) /\ S C_ ( Base ` G ) ) -> S C_ ( Base ` H ) )
35 eqid 
 |-  ( +g ` H ) = ( +g ` H )
36 4 35 3 elcntz 
 |-  ( S C_ ( Base ` H ) -> ( x e. ( Y ` S ) <-> ( x e. ( Base ` H ) /\ A. y e. S ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) ) )
37 34 36 syl 
 |-  ( ( ( A e. V /\ S C_ A ) /\ S C_ ( Base ` G ) ) -> ( x e. ( Y ` S ) <-> ( x e. ( Base ` H ) /\ A. y e. S ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) ) )
38 elin 
 |-  ( x e. ( ( Z ` S ) i^i A ) <-> ( x e. ( Z ` S ) /\ x e. A ) )
39 38 biancomi 
 |-  ( x e. ( ( Z ` S ) i^i A ) <-> ( x e. A /\ x e. ( Z ` S ) ) )
40 7 20 2 elcntz 
 |-  ( S C_ ( Base ` G ) -> ( x e. ( Z ` S ) <-> ( x e. ( Base ` G ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
41 40 adantl 
 |-  ( ( ( A e. V /\ S C_ A ) /\ S C_ ( Base ` G ) ) -> ( x e. ( Z ` S ) <-> ( x e. ( Base ` G ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
42 41 anbi2d 
 |-  ( ( ( A e. V /\ S C_ A ) /\ S C_ ( Base ` G ) ) -> ( ( x e. A /\ x e. ( Z ` S ) ) <-> ( x e. A /\ ( x e. ( Base ` G ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) ) )
43 39 42 syl5bb 
 |-  ( ( ( A e. V /\ S C_ A ) /\ S C_ ( Base ` G ) ) -> ( x e. ( ( Z ` S ) i^i A ) <-> ( x e. A /\ ( x e. ( Base ` G ) /\ A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) ) )
44 29 37 43 3bitr4d 
 |-  ( ( ( A e. V /\ S C_ A ) /\ S C_ ( Base ` G ) ) -> ( x e. ( Y ` S ) <-> x e. ( ( Z ` S ) i^i A ) ) )
45 44 ex 
 |-  ( ( A e. V /\ S C_ A ) -> ( S C_ ( Base ` G ) -> ( x e. ( Y ` S ) <-> x e. ( ( Z ` S ) i^i A ) ) ) )
46 10 15 45 pm5.21ndd 
 |-  ( ( A e. V /\ S C_ A ) -> ( x e. ( Y ` S ) <-> x e. ( ( Z ` S ) i^i A ) ) )
47 46 eqrdv 
 |-  ( ( A e. V /\ S C_ A ) -> ( Y ` S ) = ( ( Z ` S ) i^i A ) )