| Step | Hyp | Ref
| Expression |
| 1 | | dprdcntz2.1 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
| 2 | | dprdcntz2.2 |
. . . 4
⊢ (𝜑 → dom 𝑆 = 𝐼) |
| 3 | | dprdcntz2.c |
. . . 4
⊢ (𝜑 → 𝐶 ⊆ 𝐼) |
| 4 | 1, 2, 3 | dprdres 20048 |
. . 3
⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐶) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆))) |
| 5 | 4 | simpld 494 |
. 2
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶)) |
| 6 | | dmres 6030 |
. . 3
⊢ dom
(𝑆 ↾ 𝐶) = (𝐶 ∩ dom 𝑆) |
| 7 | 3, 2 | sseqtrrd 4021 |
. . . 4
⊢ (𝜑 → 𝐶 ⊆ dom 𝑆) |
| 8 | | dfss2 3969 |
. . . 4
⊢ (𝐶 ⊆ dom 𝑆 ↔ (𝐶 ∩ dom 𝑆) = 𝐶) |
| 9 | 7, 8 | sylib 218 |
. . 3
⊢ (𝜑 → (𝐶 ∩ dom 𝑆) = 𝐶) |
| 10 | 6, 9 | eqtrid 2789 |
. 2
⊢ (𝜑 → dom (𝑆 ↾ 𝐶) = 𝐶) |
| 11 | | dprdgrp 20025 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
| 12 | 1, 11 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 13 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 14 | 13 | dprdssv 20036 |
. . 3
⊢ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (Base‘𝐺) |
| 15 | | dprdcntz2.z |
. . . 4
⊢ 𝑍 = (Cntz‘𝐺) |
| 16 | 13, 15 | cntzsubg 19357 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (Base‘𝐺)) → (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺)) |
| 17 | 12, 14, 16 | sylancl 586 |
. 2
⊢ (𝜑 → (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺)) |
| 18 | | fvres 6925 |
. . . 4
⊢ (𝑥 ∈ 𝐶 → ((𝑆 ↾ 𝐶)‘𝑥) = (𝑆‘𝑥)) |
| 19 | 18 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑥) = (𝑆‘𝑥)) |
| 20 | | dprdcntz2.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ⊆ 𝐼) |
| 21 | 1, 2, 20 | dprdres 20048 |
. . . . . . 7
⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐷) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆))) |
| 22 | 21 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷)) |
| 23 | 22 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐺dom DProd (𝑆 ↾ 𝐷)) |
| 24 | | dprdsubg 20044 |
. . . . 5
⊢ (𝐺dom DProd (𝑆 ↾ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
| 25 | 23, 24 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
| 26 | 3 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐼) |
| 27 | 1, 2 | dprdf2 20027 |
. . . . . 6
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
| 28 | 27 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
| 29 | 26, 28 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
| 30 | | dmres 6030 |
. . . . . . 7
⊢ dom
(𝑆 ↾ 𝐷) = (𝐷 ∩ dom 𝑆) |
| 31 | 20, 2 | sseqtrrd 4021 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ⊆ dom 𝑆) |
| 32 | | dfss2 3969 |
. . . . . . . 8
⊢ (𝐷 ⊆ dom 𝑆 ↔ (𝐷 ∩ dom 𝑆) = 𝐷) |
| 33 | 31, 32 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝐷 ∩ dom 𝑆) = 𝐷) |
| 34 | 30, 33 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → dom (𝑆 ↾ 𝐷) = 𝐷) |
| 35 | 34 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → dom (𝑆 ↾ 𝐷) = 𝐷) |
| 36 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐺 ∈ Grp) |
| 37 | 13 | subgss 19145 |
. . . . . . 7
⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (𝑆‘𝑥) ⊆ (Base‘𝐺)) |
| 38 | 29, 37 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘𝑥) ⊆ (Base‘𝐺)) |
| 39 | 13, 15 | cntzsubg 19357 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑆‘𝑥) ⊆ (Base‘𝐺)) → (𝑍‘(𝑆‘𝑥)) ∈ (SubGrp‘𝐺)) |
| 40 | 36, 38, 39 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑍‘(𝑆‘𝑥)) ∈ (SubGrp‘𝐺)) |
| 41 | | fvres 6925 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐷 → ((𝑆 ↾ 𝐷)‘𝑦) = (𝑆‘𝑦)) |
| 42 | 41 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((𝑆 ↾ 𝐷)‘𝑦) = (𝑆‘𝑦)) |
| 43 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝐺dom DProd 𝑆) |
| 44 | 2 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → dom 𝑆 = 𝐼) |
| 45 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ⊆ 𝐼) |
| 46 | 45 | sselda 3983 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐼) |
| 47 | 26 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝑥 ∈ 𝐼) |
| 48 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
| 49 | | noel 4338 |
. . . . . . . . . . . 12
⊢ ¬
𝑥 ∈
∅ |
| 50 | | elin 3967 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐶 ∩ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐷)) |
| 51 | | dprdcntz2.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) |
| 52 | 51 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝐶 ∩ 𝐷) ↔ 𝑥 ∈ ∅)) |
| 53 | 50, 52 | bitr3id 285 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐷) ↔ 𝑥 ∈ ∅)) |
| 54 | 49, 53 | mtbiri 327 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐷)) |
| 55 | | imnan 399 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐶 → ¬ 𝑥 ∈ 𝐷) ↔ ¬ (𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐷)) |
| 56 | 54, 55 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐶 → ¬ 𝑥 ∈ 𝐷)) |
| 57 | 56 | imp 406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ¬ 𝑥 ∈ 𝐷) |
| 58 | 57 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ¬ 𝑥 ∈ 𝐷) |
| 59 | | nelne2 3040 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐷 ∧ ¬ 𝑥 ∈ 𝐷) → 𝑦 ≠ 𝑥) |
| 60 | 48, 58, 59 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝑦 ≠ 𝑥) |
| 61 | 43, 44, 46, 47, 60, 15 | dprdcntz 20028 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑥))) |
| 62 | 42, 61 | eqsstrd 4018 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((𝑆 ↾ 𝐷)‘𝑦) ⊆ (𝑍‘(𝑆‘𝑥))) |
| 63 | 23, 35, 40, 62 | dprdlub 20046 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝑍‘(𝑆‘𝑥))) |
| 64 | 15, 25, 29, 63 | cntzrecd 19696 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘𝑥) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) |
| 65 | 19, 64 | eqsstrd 4018 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑥) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) |
| 66 | 5, 10, 17, 65 | dprdlub 20046 |
1
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) |