Step | Hyp | Ref
| Expression |
1 | | dprdres.1 |
. . . 4
β’ (π β πΊdom DProd π) |
2 | | dprdgrp 19874 |
. . . 4
β’ (πΊdom DProd π β πΊ β Grp) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β πΊ β Grp) |
4 | | dprdres.2 |
. . . . 5
β’ (π β dom π = πΌ) |
5 | 1, 4 | dprdf2 19876 |
. . . 4
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
6 | | dprdres.3 |
. . . 4
β’ (π β π΄ β πΌ) |
7 | 5, 6 | fssresd 6758 |
. . 3
β’ (π β (π βΎ π΄):π΄βΆ(SubGrpβπΊ)) |
8 | 1 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β πΊdom DProd π) |
9 | 4 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β dom π = πΌ) |
10 | 6 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β π΄ β πΌ) |
11 | | simplr 767 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β π₯ β π΄) |
12 | 10, 11 | sseldd 3983 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β π₯ β πΌ) |
13 | | eldifi 4126 |
. . . . . . . . . 10
β’ (π¦ β (π΄ β {π₯}) β π¦ β π΄) |
14 | 13 | adantl 482 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β π¦ β π΄) |
15 | 10, 14 | sseldd 3983 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β π¦ β πΌ) |
16 | | eldifsni 4793 |
. . . . . . . . . 10
β’ (π¦ β (π΄ β {π₯}) β π¦ β π₯) |
17 | 16 | adantl 482 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β π¦ β π₯) |
18 | 17 | necomd 2996 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β π₯ β π¦) |
19 | | eqid 2732 |
. . . . . . . 8
β’
(CntzβπΊ) =
(CntzβπΊ) |
20 | 8, 9, 12, 15, 18, 19 | dprdcntz 19877 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β (πβπ₯) β ((CntzβπΊ)β(πβπ¦))) |
21 | 11 | fvresd 6911 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β ((π βΎ π΄)βπ₯) = (πβπ₯)) |
22 | 14 | fvresd 6911 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β ((π βΎ π΄)βπ¦) = (πβπ¦)) |
23 | 22 | fveq2d 6895 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β ((CntzβπΊ)β((π βΎ π΄)βπ¦)) = ((CntzβπΊ)β(πβπ¦))) |
24 | 20, 21, 23 | 3sstr4d 4029 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ π¦ β (π΄ β {π₯})) β ((π βΎ π΄)βπ₯) β ((CntzβπΊ)β((π βΎ π΄)βπ¦))) |
25 | 24 | ralrimiva 3146 |
. . . . 5
β’ ((π β§ π₯ β π΄) β βπ¦ β (π΄ β {π₯})((π βΎ π΄)βπ₯) β ((CntzβπΊ)β((π βΎ π΄)βπ¦))) |
26 | | fvres 6910 |
. . . . . . . 8
β’ (π₯ β π΄ β ((π βΎ π΄)βπ₯) = (πβπ₯)) |
27 | 26 | adantl 482 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β ((π βΎ π΄)βπ₯) = (πβπ₯)) |
28 | 27 | ineq1d 4211 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (((π βΎ π΄)βπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) = ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯}))))) |
29 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(BaseβπΊ) =
(BaseβπΊ) |
30 | 29 | subgacs 19040 |
. . . . . . . . . . . 12
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβ(BaseβπΊ))) |
31 | | acsmre 17595 |
. . . . . . . . . . . 12
β’
((SubGrpβπΊ)
β (ACSβ(BaseβπΊ)) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
32 | 3, 30, 31 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β (SubGrpβπΊ) β
(Mooreβ(BaseβπΊ))) |
33 | 32 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
34 | | eqid 2732 |
. . . . . . . . . 10
β’
(mrClsβ(SubGrpβπΊ)) = (mrClsβ(SubGrpβπΊ)) |
35 | | resss 6006 |
. . . . . . . . . . . . 13
β’ (π βΎ π΄) β π |
36 | | imass1 6100 |
. . . . . . . . . . . . 13
β’ ((π βΎ π΄) β π β ((π βΎ π΄) β (π΄ β {π₯})) β (π β (π΄ β {π₯}))) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π βΎ π΄) β (π΄ β {π₯})) β (π β (π΄ β {π₯})) |
38 | 6 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β π΄ β πΌ) |
39 | | ssdif 4139 |
. . . . . . . . . . . . 13
β’ (π΄ β πΌ β (π΄ β {π₯}) β (πΌ β {π₯})) |
40 | | imass2 6101 |
. . . . . . . . . . . . 13
β’ ((π΄ β {π₯}) β (πΌ β {π₯}) β (π β (π΄ β {π₯})) β (π β (πΌ β {π₯}))) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (π β (π΄ β {π₯})) β (π β (πΌ β {π₯}))) |
42 | 37, 41 | sstrid 3993 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β ((π βΎ π΄) β (π΄ β {π₯})) β (π β (πΌ β {π₯}))) |
43 | 42 | unissd 4918 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β βͺ
((π βΎ π΄) β (π΄ β {π₯})) β βͺ
(π β (πΌ β {π₯}))) |
44 | | imassrn 6070 |
. . . . . . . . . . . 12
β’ (π β (πΌ β {π₯})) β ran π |
45 | 5 | frnd 6725 |
. . . . . . . . . . . . . 14
β’ (π β ran π β (SubGrpβπΊ)) |
46 | 29 | subgss 19006 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (SubGrpβπΊ) β π₯ β (BaseβπΊ)) |
47 | | velpw 4607 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π«
(BaseβπΊ) β π₯ β (BaseβπΊ)) |
48 | 46, 47 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (SubGrpβπΊ) β π₯ β π« (BaseβπΊ)) |
49 | 48 | ssriv 3986 |
. . . . . . . . . . . . . 14
β’
(SubGrpβπΊ)
β π« (BaseβπΊ) |
50 | 45, 49 | sstrdi 3994 |
. . . . . . . . . . . . 13
β’ (π β ran π β π« (BaseβπΊ)) |
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β ran π β π« (BaseβπΊ)) |
52 | 44, 51 | sstrid 3993 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (π β (πΌ β {π₯})) β π« (BaseβπΊ)) |
53 | | sspwuni 5103 |
. . . . . . . . . . 11
β’ ((π β (πΌ β {π₯})) β π« (BaseβπΊ) β βͺ (π
β (πΌ β {π₯})) β (BaseβπΊ)) |
54 | 52, 53 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β βͺ (π β (πΌ β {π₯})) β (BaseβπΊ)) |
55 | 33, 34, 43, 54 | mrcssd 17567 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯}))) β
((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯})))) |
56 | | sslin 4234 |
. . . . . . . . 9
β’
(((mrClsβ(SubGrpβπΊ))ββͺ
((π βΎ π΄) β (π΄ β {π₯}))) β
((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯}))) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))))) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))))) |
58 | 1 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β πΊdom DProd π) |
59 | 4 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β dom π = πΌ) |
60 | 6 | sselda 3982 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π₯ β πΌ) |
61 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβπΊ) = (0gβπΊ) |
62 | 58, 59, 60, 61, 34 | dprddisj 19878 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) =
{(0gβπΊ)}) |
63 | 57, 62 | sseqtrd 4022 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) β {(0gβπΊ)}) |
64 | 5 | ffvelcdmda 7086 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΌ) β (πβπ₯) β (SubGrpβπΊ)) |
65 | 60, 64 | syldan 591 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (πβπ₯) β (SubGrpβπΊ)) |
66 | 61 | subg0cl 19013 |
. . . . . . . . . 10
β’ ((πβπ₯) β (SubGrpβπΊ) β (0gβπΊ) β (πβπ₯)) |
67 | 65, 66 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (0gβπΊ) β (πβπ₯)) |
68 | 43, 54 | sstrd 3992 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β βͺ
((π βΎ π΄) β (π΄ β {π₯})) β (BaseβπΊ)) |
69 | 34 | mrccl 17554 |
. . . . . . . . . . 11
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ βͺ
((π βΎ π΄) β (π΄ β {π₯})) β (BaseβπΊ)) β ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯}))) β (SubGrpβπΊ)) |
70 | 33, 68, 69 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯}))) β (SubGrpβπΊ)) |
71 | 61 | subg0cl 19013 |
. . . . . . . . . 10
β’
(((mrClsβ(SubGrpβπΊ))ββͺ
((π βΎ π΄) β (π΄ β {π₯}))) β (SubGrpβπΊ) β (0gβπΊ) β
((mrClsβ(SubGrpβπΊ))ββͺ
((π βΎ π΄) β (π΄ β {π₯})))) |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (0gβπΊ) β
((mrClsβ(SubGrpβπΊ))ββͺ
((π βΎ π΄) β (π΄ β {π₯})))) |
73 | 67, 72 | elind 4194 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (0gβπΊ) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯}))))) |
74 | 73 | snssd 4812 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β {(0gβπΊ)} β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯}))))) |
75 | 63, 74 | eqssd 3999 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) = {(0gβπΊ)}) |
76 | 28, 75 | eqtrd 2772 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (((π βΎ π΄)βπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) = {(0gβπΊ)}) |
77 | 25, 76 | jca 512 |
. . . 4
β’ ((π β§ π₯ β π΄) β (βπ¦ β (π΄ β {π₯})((π βΎ π΄)βπ₯) β ((CntzβπΊ)β((π βΎ π΄)βπ¦)) β§ (((π βΎ π΄)βπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) = {(0gβπΊ)})) |
78 | 77 | ralrimiva 3146 |
. . 3
β’ (π β βπ₯ β π΄ (βπ¦ β (π΄ β {π₯})((π βΎ π΄)βπ₯) β ((CntzβπΊ)β((π βΎ π΄)βπ¦)) β§ (((π βΎ π΄)βπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) = {(0gβπΊ)})) |
79 | 1, 4 | dprddomcld 19870 |
. . . . 5
β’ (π β πΌ β V) |
80 | 79, 6 | ssexd 5324 |
. . . 4
β’ (π β π΄ β V) |
81 | 7 | fdmd 6728 |
. . . 4
β’ (π β dom (π βΎ π΄) = π΄) |
82 | 19, 61, 34 | dmdprd 19867 |
. . . 4
β’ ((π΄ β V β§ dom (π βΎ π΄) = π΄) β (πΊdom DProd (π βΎ π΄) β (πΊ β Grp β§ (π βΎ π΄):π΄βΆ(SubGrpβπΊ) β§ βπ₯ β π΄ (βπ¦ β (π΄ β {π₯})((π βΎ π΄)βπ₯) β ((CntzβπΊ)β((π βΎ π΄)βπ¦)) β§ (((π βΎ π΄)βπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) = {(0gβπΊ)})))) |
83 | 80, 81, 82 | syl2anc 584 |
. . 3
β’ (π β (πΊdom DProd (π βΎ π΄) β (πΊ β Grp β§ (π βΎ π΄):π΄βΆ(SubGrpβπΊ) β§ βπ₯ β π΄ (βπ¦ β (π΄ β {π₯})((π βΎ π΄)βπ₯) β ((CntzβπΊ)β((π βΎ π΄)βπ¦)) β§ (((π βΎ π΄)βπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ ((π
βΎ π΄) β (π΄ β {π₯})))) = {(0gβπΊ)})))) |
84 | 3, 7, 78, 83 | mpbir3and 1342 |
. 2
β’ (π β πΊdom DProd (π βΎ π΄)) |
85 | | rnss 5938 |
. . . . . 6
β’ ((π βΎ π΄) β π β ran (π βΎ π΄) β ran π) |
86 | | uniss 4916 |
. . . . . 6
β’ (ran
(π βΎ π΄) β ran π β βͺ ran
(π βΎ π΄) β βͺ ran π) |
87 | 35, 85, 86 | mp2b 10 |
. . . . 5
β’ βͺ ran (π βΎ π΄) β βͺ ran
π |
88 | 87 | a1i 11 |
. . . 4
β’ (π β βͺ ran (π βΎ π΄) β βͺ ran
π) |
89 | | sspwuni 5103 |
. . . . 5
β’ (ran
π β π«
(BaseβπΊ) β βͺ ran π β (BaseβπΊ)) |
90 | 50, 89 | sylib 217 |
. . . 4
β’ (π β βͺ ran π β (BaseβπΊ)) |
91 | 32, 34, 88, 90 | mrcssd 17567 |
. . 3
β’ (π β
((mrClsβ(SubGrpβπΊ))ββͺ ran
(π βΎ π΄)) β
((mrClsβ(SubGrpβπΊ))ββͺ ran
π)) |
92 | 34 | dprdspan 19896 |
. . . 4
β’ (πΊdom DProd (π βΎ π΄) β (πΊ DProd (π βΎ π΄)) = ((mrClsβ(SubGrpβπΊ))ββͺ ran (π βΎ π΄))) |
93 | 84, 92 | syl 17 |
. . 3
β’ (π β (πΊ DProd (π βΎ π΄)) = ((mrClsβ(SubGrpβπΊ))ββͺ ran (π βΎ π΄))) |
94 | 34 | dprdspan 19896 |
. . . 4
β’ (πΊdom DProd π β (πΊ DProd π) = ((mrClsβ(SubGrpβπΊ))ββͺ ran π)) |
95 | 1, 94 | syl 17 |
. . 3
β’ (π β (πΊ DProd π) = ((mrClsβ(SubGrpβπΊ))ββͺ ran π)) |
96 | 91, 93, 95 | 3sstr4d 4029 |
. 2
β’ (π β (πΊ DProd (π βΎ π΄)) β (πΊ DProd π)) |
97 | 84, 96 | jca 512 |
1
β’ (π β (πΊdom DProd (π βΎ π΄) β§ (πΊ DProd (π βΎ π΄)) β (πΊ DProd π))) |