Step | Hyp | Ref
| Expression |
1 | | dprdcntz.4 |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐼) |
2 | | dprdcntz.5 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
3 | 2 | necomd 2849 |
. . 3
⊢ (𝜑 → 𝑌 ≠ 𝑋) |
4 | | eldifsn 4317 |
. . 3
⊢ (𝑌 ∈ (𝐼 ∖ {𝑋}) ↔ (𝑌 ∈ 𝐼 ∧ 𝑌 ≠ 𝑋)) |
5 | 1, 3, 4 | sylanbrc 698 |
. 2
⊢ (𝜑 → 𝑌 ∈ (𝐼 ∖ {𝑋})) |
6 | | dprdcntz.3 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐼) |
7 | | dprdcntz.1 |
. . . . . 6
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
8 | | dprdcntz.2 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑆 = 𝐼) |
9 | 7, 8 | dprddomcld 18400 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ V) |
10 | | dprdcntz.z |
. . . . . . . 8
⊢ 𝑍 = (Cntz‘𝐺) |
11 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
12 | | eqid 2622 |
. . . . . . . 8
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) |
13 | 10, 11, 12 | dmdprd 18397 |
. . . . . . 7
⊢ ((𝐼 ∈ V ∧ dom 𝑆 = 𝐼) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) =
{(0g‘𝐺)})))) |
14 | 9, 8, 13 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) =
{(0g‘𝐺)})))) |
15 | 7, 14 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) =
{(0g‘𝐺)}))) |
16 | 15 | simp3d 1075 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) =
{(0g‘𝐺)})) |
17 | | simpl 473 |
. . . . 5
⊢
((∀𝑦 ∈
(𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) =
{(0g‘𝐺)})
→ ∀𝑦 ∈
(𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) |
18 | 17 | ralimi 2952 |
. . . 4
⊢
(∀𝑥 ∈
𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) =
{(0g‘𝐺)})
→ ∀𝑥 ∈
𝐼 ∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) |
19 | 16, 18 | syl 17 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) |
20 | | sneq 4187 |
. . . . . 6
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
21 | 20 | difeq2d 3728 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐼 ∖ {𝑥}) = (𝐼 ∖ {𝑋})) |
22 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑆‘𝑥) = (𝑆‘𝑋)) |
23 | 22 | sseq1d 3632 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ↔ (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑦)))) |
24 | 21, 23 | raleqbidv 3152 |
. . . 4
⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ↔ ∀𝑦 ∈ (𝐼 ∖ {𝑋})(𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑦)))) |
25 | 24 | rspcv 3305 |
. . 3
⊢ (𝑋 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 ∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) → ∀𝑦 ∈ (𝐼 ∖ {𝑋})(𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑦)))) |
26 | 6, 19, 25 | sylc 65 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ (𝐼 ∖ {𝑋})(𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑦))) |
27 | | fveq2 6191 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑆‘𝑦) = (𝑆‘𝑌)) |
28 | 27 | fveq2d 6195 |
. . . 4
⊢ (𝑦 = 𝑌 → (𝑍‘(𝑆‘𝑦)) = (𝑍‘(𝑆‘𝑌))) |
29 | 28 | sseq2d 3633 |
. . 3
⊢ (𝑦 = 𝑌 → ((𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑦)) ↔ (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))) |
30 | 29 | rspcv 3305 |
. 2
⊢ (𝑌 ∈ (𝐼 ∖ {𝑋}) → (∀𝑦 ∈ (𝐼 ∖ {𝑋})(𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑦)) → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))) |
31 | 5, 26, 30 | sylc 65 |
1
⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))) |