Theorem cntzrcl

Description: Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	cntzrcl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzrcl.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	cntzrcl	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cntzrcl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzrcl.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3		noel	⊢ ¬ 𝑋 ∈ ∅
4		fvprc	⊢ ( ¬ 𝑀 ∈ V → ( Cntz ‘ 𝑀 ) = ∅ )
5	2 4	syl5eq	⊢ ( ¬ 𝑀 ∈ V → 𝑍 = ∅ )
6	5	fveq1d	⊢ ( ¬ 𝑀 ∈ V → ( 𝑍 ‘ 𝑆 ) = ( ∅ ‘ 𝑆 ) )
7		0fv	⊢ ( ∅ ‘ 𝑆 ) = ∅
8	6 7	eqtrdi	⊢ ( ¬ 𝑀 ∈ V → ( 𝑍 ‘ 𝑆 ) = ∅ )
9	8	eleq2d	⊢ ( ¬ 𝑀 ∈ V → ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) ↔ 𝑋 ∈ ∅ ) )
10	3 9	mtbiri	⊢ ( ¬ 𝑀 ∈ V → ¬ 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) )
11	10	con4i	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → 𝑀 ∈ V )
12		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
13	1 12 2	cntzfval	⊢ ( 𝑀 ∈ V → 𝑍 = ( 𝑥 ∈ 𝒫 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑀 ) 𝑦 ) } ) )
14	11 13	syl	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → 𝑍 = ( 𝑥 ∈ 𝒫 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑀 ) 𝑦 ) } ) )
15	14	dmeqd	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → dom 𝑍 = dom ( 𝑥 ∈ 𝒫 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑀 ) 𝑦 ) } ) )
16		eqid	⊢ ( 𝑥 ∈ 𝒫 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑀 ) 𝑦 ) } ) = ( 𝑥 ∈ 𝒫 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑀 ) 𝑦 ) } )
17	16	dmmptss	⊢ dom ( 𝑥 ∈ 𝒫 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑀 ) 𝑦 ) } ) ⊆ 𝒫 𝐵
18	15 17	eqsstrdi	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → dom 𝑍 ⊆ 𝒫 𝐵 )
19		elfvdm	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → 𝑆 ∈ dom 𝑍 )
20	18 19	sseldd	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → 𝑆 ∈ 𝒫 𝐵 )
21	20	elpwid	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → 𝑆 ⊆ 𝐵 )
22	11 21	jca	⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵 ) )