Step | Hyp | Ref
| Expression |
1 | | dprd2d.5 |
. . . . . 6
⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
2 | | dprdgrp 19364 |
. . . . . 6
⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | eqid 2734 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
5 | 4 | subgacs 18549 |
. . . . 5
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
6 | | acsmre 17127 |
. . . . 5
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
7 | 3, 5, 6 | 3syl 18 |
. . . 4
⊢ (𝜑 → (SubGrp‘𝐺) ∈
(Moore‘(Base‘𝐺))) |
8 | | dprd2d.k |
. . . 4
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) |
9 | | dprd2d.2 |
. . . . . 6
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
10 | | ffun 6537 |
. . . . . 6
⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → Fun 𝑆) |
11 | | funiunfv 7050 |
. . . . . 6
⊢ (Fun
𝑆 → ∪ 𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) = ∪ (𝑆 “ (𝐴 ↾ 𝐶))) |
12 | 9, 10, 11 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) = ∪ (𝑆 “ (𝐴 ↾ 𝐶))) |
13 | | resss 5865 |
. . . . . . . . . 10
⊢ (𝐴 ↾ 𝐶) ⊆ 𝐴 |
14 | 13 | sseli 3887 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ↾ 𝐶) → 𝑥 ∈ 𝐴) |
15 | | dprd2d.1 |
. . . . . . . . . 10
⊢ (𝜑 → Rel 𝐴) |
16 | | dprd2d.3 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐴 ⊆ 𝐼) |
17 | | dprd2d.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
18 | 15, 9, 16, 17, 1, 8 | dprd2dlem2 19399 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
19 | 14, 18 | sylan2 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
20 | | 1st2nd 7799 |
. . . . . . . . . . . . 13
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
21 | 15, 14, 20 | syl2an 599 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
22 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → 𝑥 ∈ (𝐴 ↾ 𝐶)) |
23 | 21, 22 | eqeltrrd 2835 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ 𝐶)) |
24 | | fvex 6719 |
. . . . . . . . . . . . 13
⊢
(2nd ‘𝑥) ∈ V |
25 | 24 | opelresi 5848 |
. . . . . . . . . . . 12
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ 𝐶) ↔ ((1st ‘𝑥) ∈ 𝐶 ∧ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐴)) |
26 | 25 | simplbi 501 |
. . . . . . . . . . 11
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ 𝐶) → (1st ‘𝑥) ∈ 𝐶) |
27 | 23, 26 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (1st ‘𝑥) ∈ 𝐶) |
28 | | ovex 7235 |
. . . . . . . . . 10
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ V |
29 | | eqid 2734 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) |
30 | | sneq 4541 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (1st ‘𝑥) → {𝑖} = {(1st ‘𝑥)}) |
31 | 30 | imaeq2d 5918 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (1st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st ‘𝑥)})) |
32 | | oveq1 7209 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (1st ‘𝑥) → (𝑖𝑆𝑗) = ((1st ‘𝑥)𝑆𝑗)) |
33 | 31, 32 | mpteq12dv 5129 |
. . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
34 | 33 | oveq2d 7218 |
. . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
35 | 29, 34 | elrnmpt1s 5815 |
. . . . . . . . . 10
⊢
(((1st ‘𝑥) ∈ 𝐶 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ V) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
36 | 27, 28, 35 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
37 | | elssuni 4841 |
. . . . . . . . 9
⊢ ((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
39 | 19, 38 | sstrd 3901 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
40 | 39 | ralrimiva 3098 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
41 | | iunss 4944 |
. . . . . 6
⊢ (∪ 𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↔ ∀𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
42 | 40, 41 | sylibr 237 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
43 | 12, 42 | eqsstrrd 3930 |
. . . 4
⊢ (𝜑 → ∪ (𝑆
“ (𝐴 ↾ 𝐶)) ⊆ ∪ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
44 | | dprd2d.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ⊆ 𝐼) |
45 | 44 | sselda 3891 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ 𝐼) |
46 | 45, 17 | syldan 594 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
47 | | ovex 7235 |
. . . . . . . . . . . 12
⊢ (𝑖𝑆𝑗) ∈ V |
48 | | eqid 2734 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) |
49 | 47, 48 | dmmpti 6511 |
. . . . . . . . . . 11
⊢ dom
(𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖}) |
50 | 49 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})) |
51 | | imassrn 5929 |
. . . . . . . . . . . . . 14
⊢ (𝑆 “ (𝐴 ↾ 𝐶)) ⊆ ran 𝑆 |
52 | 9 | frnd 6542 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
53 | | mresspw 17067 |
. . . . . . . . . . . . . . . 16
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
54 | 7, 53 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (SubGrp‘𝐺) ⊆ 𝒫
(Base‘𝐺)) |
55 | 52, 54 | sstrd 3901 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) |
56 | 51, 55 | sstrid 3902 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 “ (𝐴 ↾ 𝐶)) ⊆ 𝒫 (Base‘𝐺)) |
57 | | sspwuni 4998 |
. . . . . . . . . . . . 13
⊢ ((𝑆 “ (𝐴 ↾ 𝐶)) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ (𝐴 ↾ 𝐶)) ⊆ (Base‘𝐺)) |
58 | 56, 57 | sylib 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ (𝑆
“ (𝐴 ↾ 𝐶)) ⊆ (Base‘𝐺)) |
59 | 8 | mrccl 17086 |
. . . . . . . . . . . 12
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ 𝐶)) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∈ (SubGrp‘𝐺)) |
60 | 7, 58, 59 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∈ (SubGrp‘𝐺)) |
61 | 60 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∈ (SubGrp‘𝐺)) |
62 | | oveq2 7210 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → (𝑖𝑆𝑗) = (𝑖𝑆𝑘)) |
63 | 62, 48, 47 | fvmpt3i 6812 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐴 “ {𝑖}) → ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))‘𝑘) = (𝑖𝑆𝑘)) |
64 | 63 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))‘𝑘) = (𝑖𝑆𝑘)) |
65 | | df-ov 7205 |
. . . . . . . . . . . . . 14
⊢ (𝑖𝑆𝑘) = (𝑆‘〈𝑖, 𝑘〉) |
66 | 9 | ffnd 6535 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆 Fn 𝐴) |
67 | 66 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 𝑆 Fn 𝐴) |
68 | 13 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝐴 ↾ 𝐶) ⊆ 𝐴) |
69 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 𝑖 ∈ 𝐶) |
70 | | elrelimasn 5942 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Rel
𝐴 → (𝑘 ∈ (𝐴 “ {𝑖}) ↔ 𝑖𝐴𝑘)) |
71 | 15, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑖}) ↔ 𝑖𝐴𝑘)) |
72 | 71 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → (𝑘 ∈ (𝐴 “ {𝑖}) ↔ 𝑖𝐴𝑘)) |
73 | 72 | biimpa 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 𝑖𝐴𝑘) |
74 | | df-br 5044 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖𝐴𝑘 ↔ 〈𝑖, 𝑘〉 ∈ 𝐴) |
75 | 73, 74 | sylib 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 〈𝑖, 𝑘〉 ∈ 𝐴) |
76 | | vex 3405 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑘 ∈ V |
77 | 76 | opelresi 5848 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑖, 𝑘〉 ∈ (𝐴 ↾ 𝐶) ↔ (𝑖 ∈ 𝐶 ∧ 〈𝑖, 𝑘〉 ∈ 𝐴)) |
78 | 69, 75, 77 | sylanbrc 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 〈𝑖, 𝑘〉 ∈ (𝐴 ↾ 𝐶)) |
79 | | fnfvima 7038 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 Fn 𝐴 ∧ (𝐴 ↾ 𝐶) ⊆ 𝐴 ∧ 〈𝑖, 𝑘〉 ∈ (𝐴 ↾ 𝐶)) → (𝑆‘〈𝑖, 𝑘〉) ∈ (𝑆 “ (𝐴 ↾ 𝐶))) |
80 | 67, 68, 78, 79 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝑆‘〈𝑖, 𝑘〉) ∈ (𝑆 “ (𝐴 ↾ 𝐶))) |
81 | 65, 80 | eqeltrid 2838 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝑖𝑆𝑘) ∈ (𝑆 “ (𝐴 ↾ 𝐶))) |
82 | | elssuni 4841 |
. . . . . . . . . . . . 13
⊢ ((𝑖𝑆𝑘) ∈ (𝑆 “ (𝐴 ↾ 𝐶)) → (𝑖𝑆𝑘) ⊆ ∪ (𝑆 “ (𝐴 ↾ 𝐶))) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝑖𝑆𝑘) ⊆ ∪ (𝑆 “ (𝐴 ↾ 𝐶))) |
84 | 7, 8, 58 | mrcssidd 17100 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ (𝑆
“ (𝐴 ↾ 𝐶)) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
85 | 84 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → ∪
(𝑆 “ (𝐴 ↾ 𝐶)) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
86 | 83, 85 | sstrd 3901 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝑖𝑆𝑘) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
87 | 64, 86 | eqsstrd 3929 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))‘𝑘) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
88 | 46, 50, 61, 87 | dprdlub 19385 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
89 | | ovex 7235 |
. . . . . . . . . 10
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V |
90 | 89 | elpw 4507 |
. . . . . . . . 9
⊢ ((𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ↔ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
91 | 88, 90 | sylibr 237 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
92 | 91 | fmpttd 6921 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))):𝐶⟶𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
93 | 92 | frnd 6542 |
. . . . . 6
⊢ (𝜑 → ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
94 | | sspwuni 4998 |
. . . . . 6
⊢ (ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ↔ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
95 | 93, 94 | sylib 221 |
. . . . 5
⊢ (𝜑 → ∪ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
96 | 7, 8 | mrcssvd 17098 |
. . . . 5
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ⊆ (Base‘𝐺)) |
97 | 95, 96 | sstrd 3901 |
. . . 4
⊢ (𝜑 → ∪ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ (Base‘𝐺)) |
98 | 7, 8, 43, 97 | mrcssd 17099 |
. . 3
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ⊆ (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
99 | 8 | mrcsscl 17095 |
. . . 4
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∈ (SubGrp‘𝐺)) → (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
100 | 7, 95, 60, 99 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
101 | 98, 100 | eqssd 3908 |
. 2
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) = (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
102 | | eqid 2734 |
. . . . . . . 8
⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) |
103 | 89, 102 | dmmpti 6511 |
. . . . . . 7
⊢ dom
(𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼 |
104 | 103 | a1i 11 |
. . . . . 6
⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼) |
105 | 1, 104, 44 | dprdres 19387 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ 𝐶) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ 𝐶)) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))) |
106 | 105 | simpld 498 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ 𝐶)) |
107 | 44 | resmptd 5897 |
. . . 4
⊢ (𝜑 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ 𝐶) = (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
108 | 106, 107 | breqtrd 5069 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
109 | 8 | dprdspan 19386 |
. . 3
⊢ (𝐺dom DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝐺 DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) = (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
110 | 108, 109 | syl 17 |
. 2
⊢ (𝜑 → (𝐺 DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) = (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
111 | 101, 110 | eqtr4d 2777 |
1
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) = (𝐺 DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |