Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝐻) =
(Base‘𝐻) |
2 | | resscntz.y |
. . . . . . 7
⊢ 𝑌 = (Cntz‘𝐻) |
3 | 1, 2 | cntzrcl 17583 |
. . . . . 6
⊢ (𝑥 ∈ (𝑌‘𝑆) → (𝐻 ∈ V ∧ 𝑆 ⊆ (Base‘𝐻))) |
4 | 3 | simprd 478 |
. . . . 5
⊢ (𝑥 ∈ (𝑌‘𝑆) → 𝑆 ⊆ (Base‘𝐻)) |
5 | | resscntz.p |
. . . . . 6
⊢ 𝐻 = (𝐺 ↾s 𝐴) |
6 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
7 | 5, 6 | ressbasss 15759 |
. . . . 5
⊢
(Base‘𝐻)
⊆ (Base‘𝐺) |
8 | 4, 7 | syl6ss 3580 |
. . . 4
⊢ (𝑥 ∈ (𝑌‘𝑆) → 𝑆 ⊆ (Base‘𝐺)) |
9 | 8 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ (𝑌‘𝑆) → 𝑆 ⊆ (Base‘𝐺))) |
10 | | inss1 3795 |
. . . . . 6
⊢ ((𝑍‘𝑆) ∩ 𝐴) ⊆ (𝑍‘𝑆) |
11 | 10 | sseli 3564 |
. . . . 5
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑥 ∈ (𝑍‘𝑆)) |
12 | | resscntz.z |
. . . . . . 7
⊢ 𝑍 = (Cntz‘𝐺) |
13 | 6, 12 | cntzrcl 17583 |
. . . . . 6
⊢ (𝑥 ∈ (𝑍‘𝑆) → (𝐺 ∈ V ∧ 𝑆 ⊆ (Base‘𝐺))) |
14 | 13 | simprd 478 |
. . . . 5
⊢ (𝑥 ∈ (𝑍‘𝑆) → 𝑆 ⊆ (Base‘𝐺)) |
15 | 11, 14 | syl 17 |
. . . 4
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑆 ⊆ (Base‘𝐺)) |
16 | 15 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑆 ⊆ (Base‘𝐺))) |
17 | | anass 679 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
18 | | elin 3758 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∩ (Base‘𝐺)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺))) |
19 | 5, 6 | ressbas 15757 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ (Base‘𝐺)) = (Base‘𝐻)) |
20 | 19 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝐴 ∩ (Base‘𝐺)) ↔ 𝑥 ∈ (Base‘𝐻))) |
21 | 18, 20 | syl5bbr 273 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ↔ 𝑥 ∈ (Base‘𝐻))) |
22 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
23 | 5, 22 | ressplusg 15818 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) = (+g‘𝐻)) |
24 | 23 | oveqd 6566 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
25 | 23 | oveqd 6566 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑦(+g‘𝐺)𝑥) = (𝑦(+g‘𝐻)𝑥)) |
26 | 24, 25 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ((𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥))) |
27 | 26 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥))) |
28 | 21, 27 | anbi12d 743 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))) |
29 | 28 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))) |
30 | 17, 29 | syl5rbbr 274 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))) |
31 | | ssin 3797 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ (Base‘𝐺)) ↔ 𝑆 ⊆ (𝐴 ∩ (Base‘𝐺))) |
32 | 19 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝑆 ⊆ (𝐴 ∩ (Base‘𝐺)) ↔ 𝑆 ⊆ (Base‘𝐻))) |
33 | 31, 32 | syl5bb 271 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ (Base‘𝐺)) ↔ 𝑆 ⊆ (Base‘𝐻))) |
34 | 33 | biimpd 218 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ (Base‘𝐺)) → 𝑆 ⊆ (Base‘𝐻))) |
35 | 34 | impl 648 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → 𝑆 ⊆ (Base‘𝐻)) |
36 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝐻) = (+g‘𝐻) |
37 | 1, 36, 2 | elcntz 17578 |
. . . . . 6
⊢ (𝑆 ⊆ (Base‘𝐻) → (𝑥 ∈ (𝑌‘𝑆) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))) |
38 | 35, 37 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ (𝑌‘𝑆) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))) |
39 | | elin 3758 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ (𝑍‘𝑆) ∧ 𝑥 ∈ 𝐴)) |
40 | | ancom 465 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑍‘𝑆) ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝑍‘𝑆))) |
41 | 39, 40 | bitri 263 |
. . . . . 6
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝑍‘𝑆))) |
42 | 6, 22, 12 | elcntz 17578 |
. . . . . . . 8
⊢ (𝑆 ⊆ (Base‘𝐺) → (𝑥 ∈ (𝑍‘𝑆) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
43 | 42 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ (𝑍‘𝑆) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
44 | 43 | anbi2d 736 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝑍‘𝑆)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))) |
45 | 41, 44 | syl5bb 271 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))) |
46 | 30, 38, 45 | 3bitr4d 299 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴))) |
47 | 46 | ex 449 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑆 ⊆ (Base‘𝐺) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)))) |
48 | 9, 16, 47 | pm5.21ndd 368 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴))) |
49 | 48 | eqrdv 2608 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴)) |