Step | Hyp | Ref
| Expression |
1 | | dprd2d.5 |
. . . . . 6
⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
2 | | dprdgrp 18227 |
. . . . . 6
⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
5 | 4 | subgacs 17452 |
. . . . 5
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
6 | | acsmre 16136 |
. . . . 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 5961 |
. . . . . 6
⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → Fun 𝑆) |
11 | | funiunfv 6410 |
. . . . . 6
⊢ (Fun
𝑆 → ∪ 𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) = ∪ (𝑆 “ (𝐴 ↾ 𝐶))) |
12 | 9, 10, 11 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) = ∪ (𝑆 “ (𝐴 ↾ 𝐶))) |
13 | | resss 5342 |
. . . . . . . . . 10
⊢ (𝐴 ↾ 𝐶) ⊆ 𝐴 |
14 | 13 | sseli 3564 |
. . . . . . . . 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 18262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
19 | 14, 18 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
20 | | 1st2nd 7105 |
. . . . . . . . . . . . 13
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
21 | 15, 14, 20 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
22 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → 𝑥 ∈ (𝐴 ↾ 𝐶)) |
23 | 21, 22 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ 𝐶)) |
24 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(2nd ‘𝑥) ∈ V |
25 | 24 | opelres 5322 |
. . . . . . . . . . . 12
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ 𝐶) ↔ (〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐴 ∧ (1st ‘𝑥) ∈ 𝐶)) |
26 | 25 | simprbi 479 |
. . . . . . . . . . 11
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ 𝐶) → (1st ‘𝑥) ∈ 𝐶) |
27 | 23, 26 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (1st ‘𝑥) ∈ 𝐶) |
28 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ V |
29 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) |
30 | | sneq 4135 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (1st ‘𝑥) → {𝑖} = {(1st ‘𝑥)}) |
31 | 30 | imaeq2d 5385 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (1st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st ‘𝑥)})) |
32 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (1st ‘𝑥) → (𝑖𝑆𝑗) = ((1st ‘𝑥)𝑆𝑗)) |
33 | 31, 32 | mpteq12dv 4663 |
. . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
34 | 33 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
35 | 29, 34 | elrnmpt1s 5294 |
. . . . . . . . . 10
⊢
(((1st ‘𝑥) ∈ 𝐶 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ V) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
36 | 27, 28, 35 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
37 | | elssuni 4403 |
. . . . . . . . 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 3578 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ↾ 𝐶)) → (𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
40 | 39 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
41 | | iunss 4497 |
. . . . . 6
⊢ (∪ 𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↔ ∀𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
42 | 40, 41 | sylibr 223 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ (𝐴 ↾ 𝐶)(𝑆‘𝑥) ⊆ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
43 | 12, 42 | eqsstr3d 3603 |
. . . 4
⊢ (𝜑 → ∪ (𝑆
“ (𝐴 ↾ 𝐶)) ⊆ ∪ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
44 | | dprd2d.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ⊆ 𝐼) |
45 | 44 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ 𝐼) |
46 | 45, 17 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
47 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝑖𝑆𝑗) ∈ V |
48 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) |
49 | 47, 48 | dmmpti 5936 |
. . . . . . . . . . 11
⊢ dom
(𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖}) |
50 | 49 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})) |
51 | | imassrn 5396 |
. . . . . . . . . . . . . 14
⊢ (𝑆 “ (𝐴 ↾ 𝐶)) ⊆ ran 𝑆 |
52 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
53 | 9, 52 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
54 | | mresspw 16075 |
. . . . . . . . . . . . . . . 16
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
55 | 7, 54 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (SubGrp‘𝐺) ⊆ 𝒫
(Base‘𝐺)) |
56 | 53, 55 | sstrd 3578 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) |
57 | 51, 56 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 “ (𝐴 ↾ 𝐶)) ⊆ 𝒫 (Base‘𝐺)) |
58 | | sspwuni 4547 |
. . . . . . . . . . . . 13
⊢ ((𝑆 “ (𝐴 ↾ 𝐶)) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ (𝐴 ↾ 𝐶)) ⊆ (Base‘𝐺)) |
59 | 57, 58 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ (𝑆
“ (𝐴 ↾ 𝐶)) ⊆ (Base‘𝐺)) |
60 | 8 | mrccl 16094 |
. . . . . . . . . . . 12
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ 𝐶)) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∈ (SubGrp‘𝐺)) |
61 | 7, 59, 60 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∈ (SubGrp‘𝐺)) |
62 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∈ (SubGrp‘𝐺)) |
63 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → (𝑖𝑆𝑗) = (𝑖𝑆𝑘)) |
64 | 63, 48, 47 | fvmpt3i 6196 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐴 “ {𝑖}) → ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))‘𝑘) = (𝑖𝑆𝑘)) |
65 | 64 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))‘𝑘) = (𝑖𝑆𝑘)) |
66 | | df-ov 6552 |
. . . . . . . . . . . . . 14
⊢ (𝑖𝑆𝑘) = (𝑆‘〈𝑖, 𝑘〉) |
67 | | ffn 5958 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → 𝑆 Fn 𝐴) |
68 | 9, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆 Fn 𝐴) |
69 | 68 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 𝑆 Fn 𝐴) |
70 | 13 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝐴 ↾ 𝐶) ⊆ 𝐴) |
71 | | elrelimasn 5408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Rel
𝐴 → (𝑘 ∈ (𝐴 “ {𝑖}) ↔ 𝑖𝐴𝑘)) |
72 | 15, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑖}) ↔ 𝑖𝐴𝑘)) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → (𝑘 ∈ (𝐴 “ {𝑖}) ↔ 𝑖𝐴𝑘)) |
74 | 73 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 𝑖𝐴𝑘) |
75 | | df-br 4584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖𝐴𝑘 ↔ 〈𝑖, 𝑘〉 ∈ 𝐴) |
76 | 74, 75 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 〈𝑖, 𝑘〉 ∈ 𝐴) |
77 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 𝑖 ∈ 𝐶) |
78 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑘 ∈ V |
79 | 78 | opelres 5322 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑖, 𝑘〉 ∈ (𝐴 ↾ 𝐶) ↔ (〈𝑖, 𝑘〉 ∈ 𝐴 ∧ 𝑖 ∈ 𝐶)) |
80 | 76, 77, 79 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → 〈𝑖, 𝑘〉 ∈ (𝐴 ↾ 𝐶)) |
81 | | fnfvima 6400 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 Fn 𝐴 ∧ (𝐴 ↾ 𝐶) ⊆ 𝐴 ∧ 〈𝑖, 𝑘〉 ∈ (𝐴 ↾ 𝐶)) → (𝑆‘〈𝑖, 𝑘〉) ∈ (𝑆 “ (𝐴 ↾ 𝐶))) |
82 | 69, 70, 80, 81 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝑆‘〈𝑖, 𝑘〉) ∈ (𝑆 “ (𝐴 ↾ 𝐶))) |
83 | 66, 82 | syl5eqel 2692 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝑖𝑆𝑘) ∈ (𝑆 “ (𝐴 ↾ 𝐶))) |
84 | | elssuni 4403 |
. . . . . . . . . . . . 13
⊢ ((𝑖𝑆𝑘) ∈ (𝑆 “ (𝐴 ↾ 𝐶)) → (𝑖𝑆𝑘) ⊆ ∪ (𝑆 “ (𝐴 ↾ 𝐶))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝑖𝑆𝑘) ⊆ ∪ (𝑆 “ (𝐴 ↾ 𝐶))) |
86 | 7, 8, 59 | mrcssidd 16108 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ (𝑆
“ (𝐴 ↾ 𝐶)) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
87 | 86 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → ∪
(𝑆 “ (𝐴 ↾ 𝐶)) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
88 | 85, 87 | sstrd 3578 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → (𝑖𝑆𝑘) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
89 | 65, 88 | eqsstrd 3602 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐶) ∧ 𝑘 ∈ (𝐴 “ {𝑖})) → ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))‘𝑘) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
90 | 46, 50, 62, 89 | dprdlub 18248 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
91 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V |
92 | 91 | elpw 4114 |
. . . . . . . . 9
⊢ ((𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ↔ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
93 | 90, 92 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐶) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
94 | 93, 29 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))):𝐶⟶𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
95 | | frn 5966 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))):𝐶⟶𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) → ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
96 | 94, 95 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
97 | | sspwuni 4547 |
. . . . . 6
⊢ (ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ 𝒫 (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ↔ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
98 | 96, 97 | sylib 207 |
. . . . 5
⊢ (𝜑 → ∪ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
99 | 7, 8 | mrcssvd 16106 |
. . . . 5
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ⊆ (Base‘𝐺)) |
100 | 98, 99 | sstrd 3578 |
. . . 4
⊢ (𝜑 → ∪ ran (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ (Base‘𝐺)) |
101 | 7, 8, 43, 100 | mrcssd 16107 |
. . 3
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ⊆ (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
102 | 8 | mrcsscl 16103 |
. . . 4
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) ∈ (SubGrp‘𝐺)) → (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
103 | 7, 98, 61, 102 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶)))) |
104 | 101, 103 | eqssd 3585 |
. 2
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) = (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
105 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) |
106 | 91, 105 | dmmpti 5936 |
. . . . . . 7
⊢ dom
(𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼 |
107 | 106 | a1i 11 |
. . . . . 6
⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼) |
108 | 1, 107, 44 | dprdres 18250 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ 𝐶) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ 𝐶)) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))) |
109 | 108 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ 𝐶)) |
110 | 44 | resmptd 5371 |
. . . 4
⊢ (𝜑 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ 𝐶) = (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
111 | 109, 110 | breqtrd 4609 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
112 | 8 | dprdspan 18249 |
. . 3
⊢ (𝐺dom DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝐺 DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) = (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
113 | 111, 112 | syl 17 |
. 2
⊢ (𝜑 → (𝐺 DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) = (𝐾‘∪ ran
(𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
114 | 104, 113 | eqtr4d 2647 |
1
⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) = (𝐺 DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |