Metamath Proof Explorer

Theorem resscntz

Description: Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses resscntz.p ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
resscntz.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
resscntz.y ⊢ 𝑌 = ( Cntz ‘ 𝐻 )
Assertion resscntz ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) → ( 𝑌 ‘ 𝑆 ) = ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 resscntz.p ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2 resscntz.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
3 resscntz.y ⊢ 𝑌 = ( Cntz ‘ 𝐻 )
4 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
5 4 3 cntzrcl ⊢ ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) → ( 𝐻 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝐻 ) ) )
6 5 simprd ⊢ ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐻 ) )
7 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 1 7 ressbasss ⊢ ( Base ‘ 𝐻 ) ⊆ ( Base ‘ 𝐺 )
9 6 8 sstrdi ⊢ ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
10 9 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) )
11 elinel1 ⊢ ( 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) → 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) )
12 7 2 cntzrcl ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝐺 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) )
13 12 simprd ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
14 11 13 syl ⊢ ( 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
15 14 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) → ( 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) )
16 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( Base ‘ 𝐺 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
17 1 7 ressbas ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐻 ) )
18 17 eleq2d ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( 𝐴 ∩ ( Base ‘ 𝐺 ) ) ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
19 16 18 bitr3id ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
20 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
21 1 20 ressplusg ⊢ ( 𝐴 ∈ 𝑉 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
22 21 oveqd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
23 21 oveqd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) )
24 22 23 eqeq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) )
25 24 ralbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) )
26 19 25 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) ) )
27 26 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) ) )
28 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
29 27 28 bitr3di ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) ) )
30 ssin ⊢ ( ( 𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) ↔ 𝑆 ⊆ ( 𝐴 ∩ ( Base ‘ 𝐺 ) ) )
31 17 sseq2d ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑆 ⊆ ( 𝐴 ∩ ( Base ‘ 𝐺 ) ) ↔ 𝑆 ⊆ ( Base ‘ 𝐻 ) ) )
32 30 31 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) ↔ 𝑆 ⊆ ( Base ‘ 𝐻 ) ) )
33 32 biimpd ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐻 ) ) )
34 33 impl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐻 ) )
35 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
36 4 35 3 elcntz ⊢ ( 𝑆 ⊆ ( Base ‘ 𝐻 ) → ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) ) )
37 34 36 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) ) )
38 elin ⊢ ( 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑥 ∈ 𝐴 ) )
39 38 biancomi ⊢ ( 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) )
40 7 20 2 elcntz ⊢ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) → ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
41 40 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
42 41 anbi2d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) ) )
43 39 42 bitrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) ) )
44 29 37 43 3bitr4d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) ) )
45 44 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) → ( 𝑆 ⊆ ( Base ‘ 𝐺 ) → ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) ) ) )
46 10 15 45 pm5.21ndd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝑌 ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) ) )
47 46 eqrdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴 ) → ( 𝑌 ‘ 𝑆 ) = ( ( 𝑍 ‘ 𝑆 ) ∩ 𝐴 ) )