| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 2 |  | resscntz.y | . . . . . . 7
⊢ 𝑌 = (Cntz‘𝐻) | 
| 3 | 1, 2 | cntzrcl 19345 | . . . . . 6
⊢ (𝑥 ∈ (𝑌‘𝑆) → (𝐻 ∈ V ∧ 𝑆 ⊆ (Base‘𝐻))) | 
| 4 | 3 | simprd 495 | . . . . 5
⊢ (𝑥 ∈ (𝑌‘𝑆) → 𝑆 ⊆ (Base‘𝐻)) | 
| 5 |  | resscntz.p | . . . . . 6
⊢ 𝐻 = (𝐺 ↾s 𝐴) | 
| 6 |  | eqid 2737 | . . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 7 | 5, 6 | ressbasss 17284 | . . . . 5
⊢
(Base‘𝐻)
⊆ (Base‘𝐺) | 
| 8 | 4, 7 | sstrdi 3996 | . . . 4
⊢ (𝑥 ∈ (𝑌‘𝑆) → 𝑆 ⊆ (Base‘𝐺)) | 
| 9 | 8 | a1i 11 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ (𝑌‘𝑆) → 𝑆 ⊆ (Base‘𝐺))) | 
| 10 |  | elinel1 4201 | . . . . 5
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑥 ∈ (𝑍‘𝑆)) | 
| 11 |  | resscntz.z | . . . . . . 7
⊢ 𝑍 = (Cntz‘𝐺) | 
| 12 | 6, 11 | cntzrcl 19345 | . . . . . 6
⊢ (𝑥 ∈ (𝑍‘𝑆) → (𝐺 ∈ V ∧ 𝑆 ⊆ (Base‘𝐺))) | 
| 13 | 12 | simprd 495 | . . . . 5
⊢ (𝑥 ∈ (𝑍‘𝑆) → 𝑆 ⊆ (Base‘𝐺)) | 
| 14 | 10, 13 | syl 17 | . . . 4
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑆 ⊆ (Base‘𝐺)) | 
| 15 | 14 | a1i 11 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑆 ⊆ (Base‘𝐺))) | 
| 16 |  | elin 3967 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∩ (Base‘𝐺)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺))) | 
| 17 | 5, 6 | ressbas 17280 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ (Base‘𝐺)) = (Base‘𝐻)) | 
| 18 | 17 | eleq2d 2827 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝐴 ∩ (Base‘𝐺)) ↔ 𝑥 ∈ (Base‘𝐻))) | 
| 19 | 16, 18 | bitr3id 285 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ↔ 𝑥 ∈ (Base‘𝐻))) | 
| 20 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 21 | 5, 20 | ressplusg 17334 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) = (+g‘𝐻)) | 
| 22 | 21 | oveqd 7448 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) | 
| 23 | 21 | oveqd 7448 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑦(+g‘𝐺)𝑥) = (𝑦(+g‘𝐻)𝑥)) | 
| 24 | 22, 23 | eqeq12d 2753 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ((𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥))) | 
| 25 | 24 | ralbidv 3178 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥))) | 
| 26 | 19, 25 | anbi12d 632 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))) | 
| 27 | 26 | ad2antrr 726 | . . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))) | 
| 28 |  | anass 468 | . . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) | 
| 29 | 27, 28 | bitr3di 286 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))) | 
| 30 |  | ssin 4239 | . . . . . . . . 9
⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ (Base‘𝐺)) ↔ 𝑆 ⊆ (𝐴 ∩ (Base‘𝐺))) | 
| 31 | 17 | sseq2d 4016 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝑆 ⊆ (𝐴 ∩ (Base‘𝐺)) ↔ 𝑆 ⊆ (Base‘𝐻))) | 
| 32 | 30, 31 | bitrid 283 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ (Base‘𝐺)) ↔ 𝑆 ⊆ (Base‘𝐻))) | 
| 33 | 32 | biimpd 229 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ (Base‘𝐺)) → 𝑆 ⊆ (Base‘𝐻))) | 
| 34 | 33 | impl 455 | . . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → 𝑆 ⊆ (Base‘𝐻)) | 
| 35 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝐻) = (+g‘𝐻) | 
| 36 | 1, 35, 2 | elcntz 19340 | . . . . . 6
⊢ (𝑆 ⊆ (Base‘𝐻) → (𝑥 ∈ (𝑌‘𝑆) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))) | 
| 37 | 34, 36 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ (𝑌‘𝑆) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))) | 
| 38 |  | elin 3967 | . . . . . . 7
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ (𝑍‘𝑆) ∧ 𝑥 ∈ 𝐴)) | 
| 39 | 38 | biancomi 462 | . . . . . 6
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝑍‘𝑆))) | 
| 40 | 6, 20, 11 | elcntz 19340 | . . . . . . . 8
⊢ (𝑆 ⊆ (Base‘𝐺) → (𝑥 ∈ (𝑍‘𝑆) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) | 
| 41 | 40 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ (𝑍‘𝑆) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) | 
| 42 | 41 | anbi2d 630 | . . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝑍‘𝑆)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))) | 
| 43 | 39, 42 | bitrid 283 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))) | 
| 44 | 29, 37, 43 | 3bitr4d 311 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴))) | 
| 45 | 44 | ex 412 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑆 ⊆ (Base‘𝐺) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)))) | 
| 46 | 9, 15, 45 | pm5.21ndd 379 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴))) | 
| 47 | 46 | eqrdv 2735 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴)) |