Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
2 | | eqid 2610 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
3 | | eqid 2610 |
. . 3
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) |
4 | | dprdss.1 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
5 | | dprdgrp 18227 |
. . . 4
⊢ (𝐺dom DProd 𝑇 → 𝐺 ∈ Grp) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
7 | | dprdss.2 |
. . . 4
⊢ (𝜑 → dom 𝑇 = 𝐼) |
8 | 4, 7 | dprddomcld 18223 |
. . 3
⊢ (𝜑 → 𝐼 ∈ V) |
9 | | dprdss.3 |
. . 3
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
10 | | dprdss.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑆‘𝑘) ⊆ (𝑇‘𝑘)) |
11 | 10 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ 𝐼 (𝑆‘𝑘) ⊆ (𝑇‘𝑘)) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → (𝑆‘𝑘) = (𝑆‘𝑥)) |
13 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → (𝑇‘𝑘) = (𝑇‘𝑥)) |
14 | 12, 13 | sseq12d 3597 |
. . . . . . 7
⊢ (𝑘 = 𝑥 → ((𝑆‘𝑘) ⊆ (𝑇‘𝑘) ↔ (𝑆‘𝑥) ⊆ (𝑇‘𝑥))) |
15 | 14 | rspcv 3278 |
. . . . . 6
⊢ (𝑥 ∈ 𝐼 → (∀𝑘 ∈ 𝐼 (𝑆‘𝑘) ⊆ (𝑇‘𝑘) → (𝑆‘𝑥) ⊆ (𝑇‘𝑥))) |
16 | 11, 15 | mpan9 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ⊆ (𝑇‘𝑥)) |
17 | 16 | 3ad2antr1 1219 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ (𝑇‘𝑥)) |
18 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd 𝑇) |
19 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → dom 𝑇 = 𝐼) |
20 | | simpr1 1060 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ 𝐼) |
21 | | simpr2 1061 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐼) |
22 | | simpr3 1062 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ≠ 𝑦) |
23 | 18, 19, 20, 21, 22, 1 | dprdcntz 18230 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑇‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑇‘𝑦))) |
24 | 4, 7 | dprdf2 18229 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:𝐼⟶(SubGrp‘𝐺)) |
25 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → 𝑇:𝐼⟶(SubGrp‘𝐺)) |
26 | 25, 21 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑇‘𝑦) ∈ (SubGrp‘𝐺)) |
27 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) |
28 | 27 | subgss 17418 |
. . . . . . 7
⊢ ((𝑇‘𝑦) ∈ (SubGrp‘𝐺) → (𝑇‘𝑦) ⊆ (Base‘𝐺)) |
29 | 26, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑇‘𝑦) ⊆ (Base‘𝐺)) |
30 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → ∀𝑘 ∈ 𝐼 (𝑆‘𝑘) ⊆ (𝑇‘𝑘)) |
31 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (𝑆‘𝑘) = (𝑆‘𝑦)) |
32 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (𝑇‘𝑘) = (𝑇‘𝑦)) |
33 | 31, 32 | sseq12d 3597 |
. . . . . . . 8
⊢ (𝑘 = 𝑦 → ((𝑆‘𝑘) ⊆ (𝑇‘𝑘) ↔ (𝑆‘𝑦) ⊆ (𝑇‘𝑦))) |
34 | 33 | rspcv 3278 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐼 → (∀𝑘 ∈ 𝐼 (𝑆‘𝑘) ⊆ (𝑇‘𝑘) → (𝑆‘𝑦) ⊆ (𝑇‘𝑦))) |
35 | 21, 30, 34 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝑇‘𝑦)) |
36 | 27, 1 | cntz2ss 17588 |
. . . . . 6
⊢ (((𝑇‘𝑦) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑦) ⊆ (𝑇‘𝑦)) → ((Cntz‘𝐺)‘(𝑇‘𝑦)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
37 | 29, 35, 36 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘(𝑇‘𝑦)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
38 | 23, 37 | sstrd 3578 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑇‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
39 | 17, 38 | sstrd 3578 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
40 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ Grp) |
41 | 27 | subgacs 17452 |
. . . . . . 7
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
42 | | acsmre 16136 |
. . . . . . 7
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
43 | 40, 41, 42 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
44 | | difss 3699 |
. . . . . . . . 9
⊢ (𝐼 ∖ {𝑥}) ⊆ 𝐼 |
45 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∀𝑘 ∈ 𝐼 (𝑆‘𝑘) ⊆ (𝑇‘𝑘)) |
46 | | ssralv 3629 |
. . . . . . . . 9
⊢ ((𝐼 ∖ {𝑥}) ⊆ 𝐼 → (∀𝑘 ∈ 𝐼 (𝑆‘𝑘) ⊆ (𝑇‘𝑘) → ∀𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑘) ⊆ (𝑇‘𝑘))) |
47 | 44, 45, 46 | mpsyl 66 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∀𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑘) ⊆ (𝑇‘𝑘)) |
48 | | ss2iun 4472 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(𝐼 ∖ {𝑥})(𝑆‘𝑘) ⊆ (𝑇‘𝑘) → ∪
𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑘) ⊆ ∪
𝑘 ∈ (𝐼 ∖ {𝑥})(𝑇‘𝑘)) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪
𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑘) ⊆ ∪
𝑘 ∈ (𝐼 ∖ {𝑥})(𝑇‘𝑘)) |
50 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
51 | | ffun 5961 |
. . . . . . . 8
⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → Fun 𝑆) |
52 | | funiunfv 6410 |
. . . . . . . 8
⊢ (Fun
𝑆 → ∪ 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑘) = ∪ (𝑆 “ (𝐼 ∖ {𝑥}))) |
53 | 50, 51, 52 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪
𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑘) = ∪ (𝑆 “ (𝐼 ∖ {𝑥}))) |
54 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑇:𝐼⟶(SubGrp‘𝐺)) |
55 | | ffun 5961 |
. . . . . . . 8
⊢ (𝑇:𝐼⟶(SubGrp‘𝐺) → Fun 𝑇) |
56 | | funiunfv 6410 |
. . . . . . . 8
⊢ (Fun
𝑇 → ∪ 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑇‘𝑘) = ∪ (𝑇 “ (𝐼 ∖ {𝑥}))) |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪
𝑘 ∈ (𝐼 ∖ {𝑥})(𝑇‘𝑘) = ∪ (𝑇 “ (𝐼 ∖ {𝑥}))) |
58 | 49, 53, 57 | 3sstr3d 3610 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ ∪
(𝑇 “ (𝐼 ∖ {𝑥}))) |
59 | | imassrn 5396 |
. . . . . . . 8
⊢ (𝑇 “ (𝐼 ∖ {𝑥})) ⊆ ran 𝑇 |
60 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝑇:𝐼⟶(SubGrp‘𝐺) → ran 𝑇 ⊆ (SubGrp‘𝐺)) |
61 | 54, 60 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ran 𝑇 ⊆ (SubGrp‘𝐺)) |
62 | | mresspw 16075 |
. . . . . . . . . 10
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
63 | 43, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
64 | 61, 63 | sstrd 3578 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ran 𝑇 ⊆ 𝒫 (Base‘𝐺)) |
65 | 59, 64 | syl5ss 3579 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺)) |
66 | | sspwuni 4547 |
. . . . . . 7
⊢ ((𝑇 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑇
“ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
67 | 65, 66 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ (𝑇 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
68 | 43, 3, 58, 67 | mrcssd 16107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ⊆
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑇 “ (𝐼 ∖ {𝑥})))) |
69 | | ss2in 3802 |
. . . . 5
⊢ (((𝑆‘𝑥) ⊆ (𝑇‘𝑥) ∧ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ⊆
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑇 “ (𝐼 ∖ {𝑥})))) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ ((𝑇‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑇
“ (𝐼 ∖ {𝑥}))))) |
70 | 16, 68, 69 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ ((𝑇‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑇
“ (𝐼 ∖ {𝑥}))))) |
71 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺dom DProd 𝑇) |
72 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → dom 𝑇 = 𝐼) |
73 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
74 | 71, 72, 73, 2, 3 | dprddisj 18231 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑇‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑇
“ (𝐼 ∖ {𝑥})))) =
{(0g‘𝐺)}) |
75 | 70, 74 | sseqtrd 3604 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆
{(0g‘𝐺)}) |
76 | 1, 2, 3, 6, 8, 9, 39, 75 | dmdprdd 18221 |
. 2
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
77 | 4 | a1d 25 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd 𝑆 → 𝐺dom DProd 𝑇)) |
78 | | ss2ixp 7807 |
. . . . . . 7
⊢
(∀𝑘 ∈
𝐼 (𝑆‘𝑘) ⊆ (𝑇‘𝑘) → X𝑘 ∈ 𝐼 (𝑆‘𝑘) ⊆ X𝑘 ∈ 𝐼 (𝑇‘𝑘)) |
79 | 11, 78 | syl 17 |
. . . . . 6
⊢ (𝜑 → X𝑘 ∈
𝐼 (𝑆‘𝑘) ⊆ X𝑘 ∈ 𝐼 (𝑇‘𝑘)) |
80 | | rabss2 3648 |
. . . . . 6
⊢ (X𝑘 ∈
𝐼 (𝑆‘𝑘) ⊆ X𝑘 ∈ 𝐼 (𝑇‘𝑘) → {ℎ ∈ X𝑘 ∈ 𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)} ⊆ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}) |
81 | | ssrexv 3630 |
. . . . . 6
⊢ ({ℎ ∈ X𝑘 ∈
𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)} ⊆ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)} → (∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓) → ∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓))) |
82 | 79, 80, 81 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓) → ∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓))) |
83 | 77, 82 | anim12d 584 |
. . . 4
⊢ (𝜑 → ((𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓)) → (𝐺dom DProd 𝑇 ∧ ∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓)))) |
84 | | fdm 5964 |
. . . . 5
⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐼) |
85 | | eqid 2610 |
. . . . . 6
⊢ {ℎ ∈ X𝑘 ∈
𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)} = {ℎ ∈ X𝑘 ∈ 𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)} |
86 | 2, 85 | eldprd 18226 |
. . . . 5
⊢ (dom
𝑆 = 𝐼 → (𝑎 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓)))) |
87 | 9, 84, 86 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑆‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓)))) |
88 | | eqid 2610 |
. . . . . 6
⊢ {ℎ ∈ X𝑘 ∈
𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)} = {ℎ ∈ X𝑘 ∈ 𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)} |
89 | 2, 88 | eldprd 18226 |
. . . . 5
⊢ (dom
𝑇 = 𝐼 → (𝑎 ∈ (𝐺 DProd 𝑇) ↔ (𝐺dom DProd 𝑇 ∧ ∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓)))) |
90 | 7, 89 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ (𝐺 DProd 𝑇) ↔ (𝐺dom DProd 𝑇 ∧ ∃𝑓 ∈ {ℎ ∈ X𝑘 ∈ 𝐼 (𝑇‘𝑘) ∣ ℎ finSupp (0g‘𝐺)}𝑎 = (𝐺 Σg 𝑓)))) |
91 | 83, 87, 90 | 3imtr4d 282 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (𝐺 DProd 𝑆) → 𝑎 ∈ (𝐺 DProd 𝑇))) |
92 | 91 | ssrdv 3574 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑆) ⊆ (𝐺 DProd 𝑇)) |
93 | 76, 92 | jca 553 |
1
⊢ (𝜑 → (𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) ⊆ (𝐺 DProd 𝑇))) |