Metamath Proof Explorer

Theorem cntzval

Description: Definition 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 cntzval ( 𝑆 ⊆ 𝐵 → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 cntzfval.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntzfval.p ⊢ + = ( +g ‘ 𝑀 )
3 cntzfval.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
4 1 2 3 cntzfval ⊢ ( 𝑀 ∈ V → 𝑍 = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )
5 4 fveq1d ⊢ ( 𝑀 ∈ V → ( 𝑍 ‘ 𝑆 ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) ‘ 𝑆 ) )
6 1 fvexi ⊢ 𝐵 ∈ V
7 6 elpw2 ⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 )
8 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
9 8 rabbidv ⊢ ( 𝑠 = 𝑆 → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
10 eqid ⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
11 6 rabex ⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ∈ V
12 9 10 11 fvmpt ⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
13 7 12 sylbir ⊢ ( 𝑆 ⊆ 𝐵 → ( ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
14 5 13 sylan9eq ⊢ ( ( 𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
15 0fv ⊢ ( ∅ ‘ 𝑆 ) = ∅
16 fvprc ⊢ ( ¬ 𝑀 ∈ V → ( Cntz ‘ 𝑀 ) = ∅ )
17 3 16 eqtrid ⊢ ( ¬ 𝑀 ∈ V → 𝑍 = ∅ )
18 17 fveq1d ⊢ ( ¬ 𝑀 ∈ V → ( 𝑍 ‘ 𝑆 ) = ( ∅ ‘ 𝑆 ) )
19 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ⊆ 𝐵
20 fvprc ⊢ ( ¬ 𝑀 ∈ V → ( Base ‘ 𝑀 ) = ∅ )
21 1 20 eqtrid ⊢ ( ¬ 𝑀 ∈ V → 𝐵 = ∅ )
22 19 21 sseqtrid ⊢ ( ¬ 𝑀 ∈ V → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ⊆ ∅ )
23 ss0 ⊢ ( { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ⊆ ∅ → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } = ∅ )
24 22 23 syl ⊢ ( ¬ 𝑀 ∈ V → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } = ∅ )
25 15 18 24 3eqtr4a ⊢ ( ¬ 𝑀 ∈ V → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
26 25 adantr ⊢ ( ( ¬ 𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
27 14 26 pm2.61ian ⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )