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

Metamath Proof Explorer

Theorem cntrval2

Description: Express the center Z of a group M as the set of fixed points of the conjugation operation .(+) . (Contributed by Thierry Arnoux, 18-Nov-2025)

Ref Expression
Hypotheses cntrval2.1 ⊢ 𝐵 = ( Base ‘ 𝑀 )
cntrval2.2 ⊢ + = ( +g ‘ 𝑀 )
cntrval2.3 ⊢ − = ( -g ‘ 𝑀 )
cntrval2.4 ⊢ ⊕ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 + 𝑦 ) − 𝑥 ) )
cntrval2.5 ⊢ 𝑍 = ( Cntr ‘ 𝑀 )
Assertion cntrval2 ( 𝑀 ∈ Grp → 𝑍 = ( 𝐵 FixPts ⊕ ) )

Proof

Step Hyp Ref Expression
1 cntrval2.1 ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntrval2.2 ⊢ + = ( +g ‘ 𝑀 )
3 cntrval2.3 ⊢ − = ( -g ‘ 𝑀 )
4 cntrval2.4 ⊢ ⊕ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 + 𝑦 ) − 𝑥 ) )
5 cntrval2.5 ⊢ 𝑍 = ( Cntr ‘ 𝑀 )
6 simpll ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑀 ∈ Grp )
7 simpr ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
8 simplr ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
9 1 2 6 7 8 grpcld ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 + 𝑧 ) ∈ 𝐵 )
10 1 3 6 9 7 grpsubcld ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑝 + 𝑧 ) − 𝑝 ) ∈ 𝐵 )
11 1 2 grprcan ⊢ ( ( 𝑀 ∈ Grp ∧ ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) ) → ( ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) + 𝑝 ) = ( 𝑧 + 𝑝 ) ↔ ( ( 𝑝 + 𝑧 ) − 𝑝 ) = 𝑧 ) )
12 6 10 8 7 11 syl13anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) + 𝑝 ) = ( 𝑧 + 𝑝 ) ↔ ( ( 𝑝 + 𝑧 ) − 𝑝 ) = 𝑧 ) )
13 1 2 3 grpnpcan ⊢ ( ( 𝑀 ∈ Grp ∧ ( 𝑝 + 𝑧 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) + 𝑝 ) = ( 𝑝 + 𝑧 ) )
14 6 9 7 13 syl3anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) + 𝑝 ) = ( 𝑝 + 𝑧 ) )
15 14 eqeq2d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑧 + 𝑝 ) = ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) + 𝑝 ) ↔ ( 𝑧 + 𝑝 ) = ( 𝑝 + 𝑧 ) ) )
16 eqcom ⊢ ( ( 𝑧 + 𝑝 ) = ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) + 𝑝 ) ↔ ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) + 𝑝 ) = ( 𝑧 + 𝑝 ) )
17 15 16 bitr3di ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑧 + 𝑝 ) = ( 𝑝 + 𝑧 ) ↔ ( ( ( 𝑝 + 𝑧 ) − 𝑝 ) + 𝑝 ) = ( 𝑧 + 𝑝 ) ) )
18 4 a1i ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ⊕ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 + 𝑦 ) − 𝑥 ) ) )
19 simprl ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑧 ) ) → 𝑥 = 𝑝 )
20 simprr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑧 ) ) → 𝑦 = 𝑧 )
21 19 20 oveq12d ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑧 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑝 + 𝑧 ) )
22 21 19 oveq12d ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑧 ) ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) = ( ( 𝑝 + 𝑧 ) − 𝑝 ) )
23 ovexd ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑝 + 𝑧 ) − 𝑝 ) ∈ V )
24 18 22 7 8 23 ovmpod ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ⊕ 𝑧 ) = ( ( 𝑝 + 𝑧 ) − 𝑝 ) )
25 24 eqeq1d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑝 ⊕ 𝑧 ) = 𝑧 ↔ ( ( 𝑝 + 𝑧 ) − 𝑝 ) = 𝑧 ) )
26 12 17 25 3bitr4d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑧 + 𝑝 ) = ( 𝑝 + 𝑧 ) ↔ ( 𝑝 ⊕ 𝑧 ) = 𝑧 ) )
27 26 ralbidva ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐵 ( 𝑧 + 𝑝 ) = ( 𝑝 + 𝑧 ) ↔ ∀ 𝑝 ∈ 𝐵 ( 𝑝 ⊕ 𝑧 ) = 𝑧 ) )
28 27 pm5.32da ⊢ ( 𝑀 ∈ Grp → ( ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑝 ∈ 𝐵 ( 𝑧 + 𝑝 ) = ( 𝑝 + 𝑧 ) ) ↔ ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑝 ∈ 𝐵 ( 𝑝 ⊕ 𝑧 ) = 𝑧 ) ) )
29 1 2 5 elcntr ⊢ ( 𝑧 ∈ 𝑍 ↔ ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑝 ∈ 𝐵 ( 𝑧 + 𝑝 ) = ( 𝑝 + 𝑧 ) ) )
30 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑝 ∈ 𝐵 ( 𝑝 ⊕ 𝑧 ) = 𝑧 } ↔ ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑝 ∈ 𝐵 ( 𝑝 ⊕ 𝑧 ) = 𝑧 ) )
31 28 29 30 3bitr4g ⊢ ( 𝑀 ∈ Grp → ( 𝑧 ∈ 𝑍 ↔ 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑝 ∈ 𝐵 ( 𝑝 ⊕ 𝑧 ) = 𝑧 } ) )
32 1 2 3 4 conjga ⊢ ( 𝑀 ∈ Grp → ⊕ ∈ ( 𝑀 GrpAct 𝐵 ) )
33 1 32 fxpgaval ⊢ ( 𝑀 ∈ Grp → ( 𝐵 FixPts ⊕ ) = { 𝑧 ∈ 𝐵 ∣ ∀ 𝑝 ∈ 𝐵 ( 𝑝 ⊕ 𝑧 ) = 𝑧 } )
34 33 eleq2d ⊢ ( 𝑀 ∈ Grp → ( 𝑧 ∈ ( 𝐵 FixPts ⊕ ) ↔ 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑝 ∈ 𝐵 ( 𝑝 ⊕ 𝑧 ) = 𝑧 } ) )
35 31 34 bitr4d ⊢ ( 𝑀 ∈ Grp → ( 𝑧 ∈ 𝑍 ↔ 𝑧 ∈ ( 𝐵 FixPts ⊕ ) ) )
36 35 eqrdv ⊢ ( 𝑀 ∈ Grp → 𝑍 = ( 𝐵 FixPts ⊕ ) )