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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzun.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	cntzun	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑍 ‘ ( 𝑋 ∪ 𝑌 ) ) = ( ( 𝑍 ‘ 𝑋 ) ∩ ( 𝑍 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cntzun.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzun.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3		ralunb	⊢ ( ∀ 𝑦 ∈ ( 𝑋 ∪ 𝑌 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) )
4	3	a1i	⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝑋 ∪ 𝑌 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
5	4	pm5.32da	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑋 ∪ 𝑌 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) ) )
6		anandi	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
7	5 6	bitrdi	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑋 ∪ 𝑌 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) ) )
8		unss	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) ↔ ( 𝑋 ∪ 𝑌 ) ⊆ 𝐵 )
9		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
10	1 9 2	elcntz	⊢ ( ( 𝑋 ∪ 𝑌 ) ⊆ 𝐵 → ( 𝑥 ∈ ( 𝑍 ‘ ( 𝑋 ∪ 𝑌 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑋 ∪ 𝑌 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
11	8 10	sylbi	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑍 ‘ ( 𝑋 ∪ 𝑌 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑋 ∪ 𝑌 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
12	1 9 2	elcntz	⊢ ( 𝑋 ⊆ 𝐵 → ( 𝑥 ∈ ( 𝑍 ‘ 𝑋 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
13	1 9 2	elcntz	⊢ ( 𝑌 ⊆ 𝐵 → ( 𝑥 ∈ ( 𝑍 ‘ 𝑌 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
14	12 13	bi2anan9	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) → ( ( 𝑥 ∈ ( 𝑍 ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑌 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) ) ) )
15	7 11 14	3bitr4d	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑍 ‘ ( 𝑋 ∪ 𝑌 ) ) ↔ ( 𝑥 ∈ ( 𝑍 ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑌 ) ) ) )
16		elin	⊢ ( 𝑥 ∈ ( ( 𝑍 ‘ 𝑋 ) ∩ ( 𝑍 ‘ 𝑌 ) ) ↔ ( 𝑥 ∈ ( 𝑍 ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑌 ) ) )
17	15 16	bitr4di	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑍 ‘ ( 𝑋 ∪ 𝑌 ) ) ↔ 𝑥 ∈ ( ( 𝑍 ‘ 𝑋 ) ∩ ( 𝑍 ‘ 𝑌 ) ) ) )
18	17	eqrdv	⊢ ( ( 𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑍 ‘ ( 𝑋 ∪ 𝑌 ) ) = ( ( 𝑍 ‘ 𝑋 ) ∩ ( 𝑍 ‘ 𝑌 ) ) )