Metamath Proof Explorer

Theorem cntzun

Description: The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023)

Ref Expression
Hypotheses cntzun.b 
|- B = ( Base ` M )
cntzun.z 
|- Z = ( Cntz ` M )
Assertion cntzun 
|- ( ( X C_ B /\ Y C_ B ) -> ( Z ` ( X u. Y ) ) = ( ( Z ` X ) i^i ( Z ` Y ) ) )

Proof

Step Hyp Ref Expression
1 cntzun.b 
 |-  B = ( Base ` M )
2 cntzun.z 
 |-  Z = ( Cntz ` M )
3 ralunb 
 |-  ( A. y e. ( X u. Y ) ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) <-> ( A. y e. X ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) /\ A. y e. Y ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) )
4 3 a1i 
 |-  ( ( ( X C_ B /\ Y C_ B ) /\ x e. B ) -> ( A. y e. ( X u. Y ) ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) <-> ( A. y e. X ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) /\ A. y e. Y ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) )
5 4 pm5.32da 
 |-  ( ( X C_ B /\ Y C_ B ) -> ( ( x e. B /\ A. y e. ( X u. Y ) ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) <-> ( x e. B /\ ( A. y e. X ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) /\ A. y e. Y ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) ) )
6 anandi 
 |-  ( ( x e. B /\ ( A. y e. X ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) /\ A. y e. Y ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) <-> ( ( x e. B /\ A. y e. X ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) /\ ( x e. B /\ A. y e. Y ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) )
7 5 6 bitrdi 
 |-  ( ( X C_ B /\ Y C_ B ) -> ( ( x e. B /\ A. y e. ( X u. Y ) ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) <-> ( ( x e. B /\ A. y e. X ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) /\ ( x e. B /\ A. y e. Y ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) ) )
8 unss 
 |-  ( ( X C_ B /\ Y C_ B ) <-> ( X u. Y ) C_ B )
9 eqid 
 |-  ( +g ` M ) = ( +g ` M )
10 1 9 2 elcntz 
 |-  ( ( X u. Y ) C_ B -> ( x e. ( Z ` ( X u. Y ) ) <-> ( x e. B /\ A. y e. ( X u. Y ) ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) )
11 8 10 sylbi 
 |-  ( ( X C_ B /\ Y C_ B ) -> ( x e. ( Z ` ( X u. Y ) ) <-> ( x e. B /\ A. y e. ( X u. Y ) ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) )
12 1 9 2 elcntz 
 |-  ( X C_ B -> ( x e. ( Z ` X ) <-> ( x e. B /\ A. y e. X ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) )
13 1 9 2 elcntz 
 |-  ( Y C_ B -> ( x e. ( Z ` Y ) <-> ( x e. B /\ A. y e. Y ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) )
14 12 13 bi2anan9 
 |-  ( ( X C_ B /\ Y C_ B ) -> ( ( x e. ( Z ` X ) /\ x e. ( Z ` Y ) ) <-> ( ( x e. B /\ A. y e. X ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) /\ ( x e. B /\ A. y e. Y ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) ) ) )
15 7 11 14 3bitr4d 
 |-  ( ( X C_ B /\ Y C_ B ) -> ( x e. ( Z ` ( X u. Y ) ) <-> ( x e. ( Z ` X ) /\ x e. ( Z ` Y ) ) ) )
16 elin 
 |-  ( x e. ( ( Z ` X ) i^i ( Z ` Y ) ) <-> ( x e. ( Z ` X ) /\ x e. ( Z ` Y ) ) )
17 15 16 bitr4di 
 |-  ( ( X C_ B /\ Y C_ B ) -> ( x e. ( Z ` ( X u. Y ) ) <-> x e. ( ( Z ` X ) i^i ( Z ` Y ) ) ) )
18 17 eqrdv 
 |-  ( ( X C_ B /\ Y C_ B ) -> ( Z ` ( X u. Y ) ) = ( ( Z ` X ) i^i ( Z ` Y ) ) )