Step | Hyp | Ref
| Expression |
1 | | dprdcntz.3 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐼) |
2 | | dprdcntz.1 |
. . . . 5
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
3 | | dprdcntz.2 |
. . . . . . 7
⊢ (𝜑 → dom 𝑆 = 𝐼) |
4 | 2, 3 | dprddomcld 18223 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ V) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
6 | | dprddisj.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
7 | | dprddisj.k |
. . . . . . 7
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) |
8 | 5, 6, 7 | dmdprd 18220 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ dom 𝑆 = 𝐼) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })))) |
9 | 4, 3, 8 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })))) |
10 | 2, 9 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }))) |
11 | 10 | simp3d 1068 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })) |
12 | | simpr 476 |
. . . 4
⊢
((∀𝑦 ∈
(𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }) |
13 | 12 | ralimi 2936 |
. . 3
⊢
(∀𝑥 ∈
𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }) → ∀𝑥 ∈ 𝐼 ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }) |
14 | 11, 13 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }) |
15 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑆‘𝑥) = (𝑆‘𝑋)) |
16 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
17 | 16 | difeq2d 3690 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝐼 ∖ {𝑥}) = (𝐼 ∖ {𝑋})) |
18 | 17 | imaeq2d 5385 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑆 “ (𝐼 ∖ {𝑥})) = (𝑆 “ (𝐼 ∖ {𝑋}))) |
19 | 18 | unieqd 4382 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ∪ (𝑆 “ (𝐼 ∖ {𝑥})) = ∪ (𝑆 “ (𝐼 ∖ {𝑋}))) |
20 | 19 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) = (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) |
21 | 15, 20 | ineq12d 3777 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋}))))) |
22 | 21 | eqeq1d 2612 |
. . 3
⊢ (𝑥 = 𝑋 → (((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 } ↔ ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) = { 0 })) |
23 | 22 | rspcv 3278 |
. 2
⊢ (𝑋 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 } → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) = { 0 })) |
24 | 1, 14, 23 | sylc 63 |
1
⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) = { 0 }) |