Theorem cntzfval

Description: First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzfval.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzfval.p	⊢ + = ( +g ‘ 𝑀 )
	cntzfval.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	cntzfval	⊢ ( 𝑀 ∈ 𝑉 → 𝑍 = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		cntzfval.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzfval.p	⊢ + = ( +g ‘ 𝑀 )
3		cntzfval.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
4		elex	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
5		fveq2	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
6	5 1	eqtr4di	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐵 )
7	6	pweqd	⊢ ( 𝑚 = 𝑀 → 𝒫 ( Base ‘ 𝑚 ) = 𝒫 𝐵 )
8		fveq2	⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
9	8 2	eqtr4di	⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = + )
10	9	oveqd	⊢ ( 𝑚 = 𝑀 → ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
11	9	oveqd	⊢ ( 𝑚 = 𝑀 → ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) = ( 𝑦 + 𝑥 ) )
12	10 11	eqeq12d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) ↔ ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
13	12	ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
14	6 13	rabeqbidv	⊢ ( 𝑚 = 𝑀 → { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
15	7 14	mpteq12dv	⊢ ( 𝑚 = 𝑀 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )
16		df-cntz	⊢ Cntz = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } ) )
17	1	fvexi	⊢ 𝐵 ∈ V
18	17	pwex	⊢ 𝒫 𝐵 ∈ V
19	18	mptex	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) ∈ V
20	15 16 19	fvmpt	⊢ ( 𝑀 ∈ V → ( Cntz ‘ 𝑀 ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )
21	4 20	syl	⊢ ( 𝑀 ∈ 𝑉 → ( Cntz ‘ 𝑀 ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )
22	3 21	syl5eq	⊢ ( 𝑀 ∈ 𝑉 → 𝑍 = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )