Step | Hyp | Ref
| Expression |
1 | | dprdsplit.u |
. . . . . 6
β’ (π β πΌ = (πΆ βͺ π·)) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π β πΆ) β πΌ = (πΆ βͺ π·)) |
3 | 2 | eleq2d 2820 |
. . . 4
β’ ((π β§ π β πΆ) β (π β πΌ β π β (πΆ βͺ π·))) |
4 | | elun 4148 |
. . . 4
β’ (π β (πΆ βͺ π·) β (π β πΆ β¨ π β π·)) |
5 | 3, 4 | bitrdi 287 |
. . 3
β’ ((π β§ π β πΆ) β (π β πΌ β (π β πΆ β¨ π β π·))) |
6 | | dmdprdsplit2.1 |
. . . . . . . 8
β’ (π β πΊdom DProd (π βΎ πΆ)) |
7 | 6 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β πΊdom DProd (π βΎ πΆ)) |
8 | | dprdsplit.2 |
. . . . . . . . . 10
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
9 | | ssun1 4172 |
. . . . . . . . . . 11
β’ πΆ β (πΆ βͺ π·) |
10 | 9, 1 | sseqtrrid 4035 |
. . . . . . . . . 10
β’ (π β πΆ β πΌ) |
11 | 8, 10 | fssresd 6756 |
. . . . . . . . 9
β’ (π β (π βΎ πΆ):πΆβΆ(SubGrpβπΊ)) |
12 | 11 | fdmd 6726 |
. . . . . . . 8
β’ (π β dom (π βΎ πΆ) = πΆ) |
13 | 12 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β dom (π βΎ πΆ) = πΆ) |
14 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β π β πΆ) |
15 | | simprl 770 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β π β πΆ) |
16 | | simprr 772 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β π β π) |
17 | | dmdprdsplit.z |
. . . . . . 7
β’ π = (CntzβπΊ) |
18 | 7, 13, 14, 15, 16, 17 | dprdcntz 19873 |
. . . . . 6
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β ((π βΎ πΆ)βπ) β (πβ((π βΎ πΆ)βπ))) |
19 | | fvres 6908 |
. . . . . . 7
β’ (π β πΆ β ((π βΎ πΆ)βπ) = (πβπ)) |
20 | 19 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β ((π βΎ πΆ)βπ) = (πβπ)) |
21 | | fvres 6908 |
. . . . . . . 8
β’ (π β πΆ β ((π βΎ πΆ)βπ) = (πβπ)) |
22 | 21 | ad2antrl 727 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β ((π βΎ πΆ)βπ) = (πβπ)) |
23 | 22 | fveq2d 6893 |
. . . . . 6
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β (πβ((π βΎ πΆ)βπ)) = (πβ(πβπ))) |
24 | 18, 20, 23 | 3sstr3d 4028 |
. . . . 5
β’ (((π β§ π β πΆ) β§ (π β πΆ β§ π β π)) β (πβπ) β (πβ(πβπ))) |
25 | 24 | exp32 422 |
. . . 4
β’ ((π β§ π β πΆ) β (π β πΆ β (π β π β (πβπ) β (πβ(πβπ))))) |
26 | 19 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β ((π βΎ πΆ)βπ) = (πβπ)) |
27 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β πΊdom DProd (π βΎ πΆ)) |
28 | 12 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β dom (π βΎ πΆ) = πΆ) |
29 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β π β πΆ) |
30 | 27, 28, 29 | dprdub 19890 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β ((π βΎ πΆ)βπ) β (πΊ DProd (π βΎ πΆ))) |
31 | 26, 30 | eqsstrrd 4021 |
. . . . . 6
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β (πβπ) β (πΊ DProd (π βΎ πΆ))) |
32 | | dmdprdsplit2.3 |
. . . . . . . 8
β’ (π β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) |
33 | 32 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) |
34 | | eqid 2733 |
. . . . . . . . 9
β’
(BaseβπΊ) =
(BaseβπΊ) |
35 | 34 | dprdssv 19881 |
. . . . . . . 8
β’ (πΊ DProd (π βΎ π·)) β (BaseβπΊ) |
36 | | fvres 6908 |
. . . . . . . . . 10
β’ (π β π· β ((π βΎ π·)βπ) = (πβπ)) |
37 | 36 | ad2antrl 727 |
. . . . . . . . 9
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β ((π βΎ π·)βπ) = (πβπ)) |
38 | | dmdprdsplit2.2 |
. . . . . . . . . . 11
β’ (π β πΊdom DProd (π βΎ π·)) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β πΊdom DProd (π βΎ π·)) |
40 | | ssun2 4173 |
. . . . . . . . . . . . . 14
β’ π· β (πΆ βͺ π·) |
41 | 40, 1 | sseqtrrid 4035 |
. . . . . . . . . . . . 13
β’ (π β π· β πΌ) |
42 | 8, 41 | fssresd 6756 |
. . . . . . . . . . . 12
β’ (π β (π βΎ π·):π·βΆ(SubGrpβπΊ)) |
43 | 42 | fdmd 6726 |
. . . . . . . . . . 11
β’ (π β dom (π βΎ π·) = π·) |
44 | 43 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β dom (π βΎ π·) = π·) |
45 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β π β π·) |
46 | 39, 44, 45 | dprdub 19890 |
. . . . . . . . 9
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β ((π βΎ π·)βπ) β (πΊ DProd (π βΎ π·))) |
47 | 37, 46 | eqsstrrd 4021 |
. . . . . . . 8
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β (πβπ) β (πΊ DProd (π βΎ π·))) |
48 | 34, 17 | cntz2ss 19194 |
. . . . . . . 8
β’ (((πΊ DProd (π βΎ π·)) β (BaseβπΊ) β§ (πβπ) β (πΊ DProd (π βΎ π·))) β (πβ(πΊ DProd (π βΎ π·))) β (πβ(πβπ))) |
49 | 35, 47, 48 | sylancr 588 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β (πβ(πΊ DProd (π βΎ π·))) β (πβ(πβπ))) |
50 | 33, 49 | sstrd 3992 |
. . . . . 6
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β (πΊ DProd (π βΎ πΆ)) β (πβ(πβπ))) |
51 | 31, 50 | sstrd 3992 |
. . . . 5
β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π)) β (πβπ) β (πβ(πβπ))) |
52 | 51 | exp32 422 |
. . . 4
β’ ((π β§ π β πΆ) β (π β π· β (π β π β (πβπ) β (πβ(πβπ))))) |
53 | 25, 52 | jaod 858 |
. . 3
β’ ((π β§ π β πΆ) β ((π β πΆ β¨ π β π·) β (π β π β (πβπ) β (πβ(πβπ))))) |
54 | 5, 53 | sylbid 239 |
. 2
β’ ((π β§ π β πΆ) β (π β πΌ β (π β π β (πβπ) β (πβ(πβπ))))) |
55 | | dprdgrp 19870 |
. . . . . . . 8
β’ (πΊdom DProd (π βΎ πΆ) β πΊ β Grp) |
56 | 6, 55 | syl 17 |
. . . . . . 7
β’ (π β πΊ β Grp) |
57 | 56 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΆ) β πΊ β Grp) |
58 | 34 | subgacs 19036 |
. . . . . 6
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβ(BaseβπΊ))) |
59 | | acsmre 17593 |
. . . . . 6
β’
((SubGrpβπΊ)
β (ACSβ(BaseβπΊ)) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
60 | 57, 58, 59 | 3syl 18 |
. . . . 5
β’ ((π β§ π β πΆ) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
61 | | difundir 4280 |
. . . . . . . . . . 11
β’ ((πΆ βͺ π·) β {π}) = ((πΆ β {π}) βͺ (π· β {π})) |
62 | 2 | difeq1d 4121 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β (πΌ β {π}) = ((πΆ βͺ π·) β {π})) |
63 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β πΆ) β π β πΆ) |
64 | 63 | snssd 4812 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β πΆ) β {π} β πΆ) |
65 | | sslin 4234 |
. . . . . . . . . . . . . . 15
β’ ({π} β πΆ β (π· β© {π}) β (π· β© πΆ)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β (π· β© {π}) β (π· β© πΆ)) |
67 | | incom 4201 |
. . . . . . . . . . . . . . 15
β’ (πΆ β© π·) = (π· β© πΆ) |
68 | | dprdsplit.i |
. . . . . . . . . . . . . . . 16
β’ (π β (πΆ β© π·) = β
) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β πΆ) β (πΆ β© π·) = β
) |
70 | 67, 69 | eqtr3id 2787 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β (π· β© πΆ) = β
) |
71 | | sseq0 4399 |
. . . . . . . . . . . . . 14
β’ (((π· β© {π}) β (π· β© πΆ) β§ (π· β© πΆ) = β
) β (π· β© {π}) = β
) |
72 | 66, 70, 71 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β (π· β© {π}) = β
) |
73 | | disj3 4453 |
. . . . . . . . . . . . 13
β’ ((π· β© {π}) = β
β π· = (π· β {π})) |
74 | 72, 73 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β π· = (π· β {π})) |
75 | 74 | uneq2d 4163 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β ((πΆ β {π}) βͺ π·) = ((πΆ β {π}) βͺ (π· β {π}))) |
76 | 61, 62, 75 | 3eqtr4a 2799 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β (πΌ β {π}) = ((πΆ β {π}) βͺ π·)) |
77 | 76 | imaeq2d 6058 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (π β (πΌ β {π})) = (π β ((πΆ β {π}) βͺ π·))) |
78 | | imaundi 6147 |
. . . . . . . . 9
β’ (π β ((πΆ β {π}) βͺ π·)) = ((π β (πΆ β {π})) βͺ (π β π·)) |
79 | 77, 78 | eqtrdi 2789 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (π β (πΌ β {π})) = ((π β (πΆ β {π})) βͺ (π β π·))) |
80 | 79 | unieqd 4922 |
. . . . . . 7
β’ ((π β§ π β πΆ) β βͺ (π β (πΌ β {π})) = βͺ ((π β (πΆ β {π})) βͺ (π β π·))) |
81 | | uniun 4934 |
. . . . . . 7
β’ βͺ ((π
β (πΆ β {π})) βͺ (π β π·)) = (βͺ (π β (πΆ β {π})) βͺ βͺ
(π β π·)) |
82 | 80, 81 | eqtrdi 2789 |
. . . . . 6
β’ ((π β§ π β πΆ) β βͺ (π β (πΌ β {π})) = (βͺ (π β (πΆ β {π})) βͺ βͺ
(π β π·))) |
83 | | dmdprdsplit2lem.k |
. . . . . . . . 9
β’ πΎ =
(mrClsβ(SubGrpβπΊ)) |
84 | | difss 4131 |
. . . . . . . . . . 11
β’ (πΆ β {π}) β πΆ |
85 | | imass2 6099 |
. . . . . . . . . . 11
β’ ((πΆ β {π}) β πΆ β (π β (πΆ β {π})) β (π β πΆ)) |
86 | | uniss 4916 |
. . . . . . . . . . 11
β’ ((π β (πΆ β {π})) β (π β πΆ) β βͺ (π β (πΆ β {π})) β βͺ
(π β πΆ)) |
87 | 84, 85, 86 | mp2b 10 |
. . . . . . . . . 10
β’ βͺ (π
β (πΆ β {π})) β βͺ (π
β πΆ) |
88 | | imassrn 6069 |
. . . . . . . . . . . 12
β’ (π β πΆ) β ran π |
89 | 8 | frnd 6723 |
. . . . . . . . . . . . . 14
β’ (π β ran π β (SubGrpβπΊ)) |
90 | 89 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β ran π β (SubGrpβπΊ)) |
91 | | mresspw 17533 |
. . . . . . . . . . . . . 14
β’
((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β (SubGrpβπΊ) β π« (BaseβπΊ)) |
92 | 60, 91 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β (SubGrpβπΊ) β π« (BaseβπΊ)) |
93 | 90, 92 | sstrd 3992 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β ran π β π« (BaseβπΊ)) |
94 | 88, 93 | sstrid 3993 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β (π β πΆ) β π« (BaseβπΊ)) |
95 | | sspwuni 5103 |
. . . . . . . . . . 11
β’ ((π β πΆ) β π« (BaseβπΊ) β βͺ (π
β πΆ) β
(BaseβπΊ)) |
96 | 94, 95 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β βͺ (π β πΆ) β (BaseβπΊ)) |
97 | 87, 96 | sstrid 3993 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β βͺ (π β (πΆ β {π})) β (BaseβπΊ)) |
98 | 60, 83, 97 | mrcssidd 17566 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β βͺ (π β (πΆ β {π})) β (πΎββͺ (π β (πΆ β {π})))) |
99 | | imassrn 6069 |
. . . . . . . . . . . 12
β’ (π β π·) β ran π |
100 | 99, 93 | sstrid 3993 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β (π β π·) β π« (BaseβπΊ)) |
101 | | sspwuni 5103 |
. . . . . . . . . . 11
β’ ((π β π·) β π« (BaseβπΊ) β βͺ (π
β π·) β
(BaseβπΊ)) |
102 | 100, 101 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β βͺ (π β π·) β (BaseβπΊ)) |
103 | 60, 83, 102 | mrcssidd 17566 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β βͺ (π β π·) β (πΎββͺ (π β π·))) |
104 | 83 | dprdspan 19892 |
. . . . . . . . . . . 12
β’ (πΊdom DProd (π βΎ π·) β (πΊ DProd (π βΎ π·)) = (πΎββͺ ran
(π βΎ π·))) |
105 | 38, 104 | syl 17 |
. . . . . . . . . . 11
β’ (π β (πΊ DProd (π βΎ π·)) = (πΎββͺ ran
(π βΎ π·))) |
106 | | df-ima 5689 |
. . . . . . . . . . . . 13
β’ (π β π·) = ran (π βΎ π·) |
107 | 106 | unieqi 4921 |
. . . . . . . . . . . 12
β’ βͺ (π
β π·) = βͺ ran (π βΎ π·) |
108 | 107 | fveq2i 6892 |
. . . . . . . . . . 11
β’ (πΎββͺ (π
β π·)) = (πΎββͺ ran (π βΎ π·)) |
109 | 105, 108 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π β (πΊ DProd (π βΎ π·)) = (πΎββͺ (π β π·))) |
110 | 109 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (πΊ DProd (π βΎ π·)) = (πΎββͺ (π β π·))) |
111 | 103, 110 | sseqtrrd 4023 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β βͺ (π β π·) β (πΊ DProd (π βΎ π·))) |
112 | | unss12 4182 |
. . . . . . . 8
β’ ((βͺ (π
β (πΆ β {π})) β (πΎββͺ (π β (πΆ β {π}))) β§ βͺ
(π β π·) β (πΊ DProd (π βΎ π·))) β (βͺ
(π β (πΆ β {π})) βͺ βͺ
(π β π·)) β ((πΎββͺ (π β (πΆ β {π}))) βͺ (πΊ DProd (π βΎ π·)))) |
113 | 98, 111, 112 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β πΆ) β (βͺ
(π β (πΆ β {π})) βͺ βͺ
(π β π·)) β ((πΎββͺ (π β (πΆ β {π}))) βͺ (πΊ DProd (π βΎ π·)))) |
114 | 83 | mrccl 17552 |
. . . . . . . . 9
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ βͺ (π β (πΆ β {π})) β (BaseβπΊ)) β (πΎββͺ (π β (πΆ β {π}))) β (SubGrpβπΊ)) |
115 | 60, 97, 114 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πΎββͺ (π β (πΆ β {π}))) β (SubGrpβπΊ)) |
116 | | dprdsubg 19889 |
. . . . . . . . . 10
β’ (πΊdom DProd (π βΎ π·) β (πΊ DProd (π βΎ π·)) β (SubGrpβπΊ)) |
117 | 38, 116 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊ DProd (π βΎ π·)) β (SubGrpβπΊ)) |
118 | 117 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πΊ DProd (π βΎ π·)) β (SubGrpβπΊ)) |
119 | | eqid 2733 |
. . . . . . . . 9
β’
(LSSumβπΊ) =
(LSSumβπΊ) |
120 | 119 | lsmunss 19522 |
. . . . . . . 8
β’ (((πΎββͺ (π
β (πΆ β {π}))) β (SubGrpβπΊ) β§ (πΊ DProd (π βΎ π·)) β (SubGrpβπΊ)) β ((πΎββͺ (π β (πΆ β {π}))) βͺ (πΊ DProd (π βΎ π·))) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·)))) |
121 | 115, 118,
120 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β πΆ) β ((πΎββͺ (π β (πΆ β {π}))) βͺ (πΊ DProd (π βΎ π·))) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·)))) |
122 | 113, 121 | sstrd 3992 |
. . . . . 6
β’ ((π β§ π β πΆ) β (βͺ
(π β (πΆ β {π})) βͺ βͺ
(π β π·)) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·)))) |
123 | 82, 122 | eqsstrd 4020 |
. . . . 5
β’ ((π β§ π β πΆ) β βͺ (π β (πΌ β {π})) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·)))) |
124 | 87 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β βͺ (π β (πΆ β {π})) β βͺ
(π β πΆ)) |
125 | 60, 83, 124, 96 | mrcssd 17565 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πΎββͺ (π β (πΆ β {π}))) β (πΎββͺ (π β πΆ))) |
126 | 83 | dprdspan 19892 |
. . . . . . . . . . 11
β’ (πΊdom DProd (π βΎ πΆ) β (πΊ DProd (π βΎ πΆ)) = (πΎββͺ ran
(π βΎ πΆ))) |
127 | 6, 126 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΊ DProd (π βΎ πΆ)) = (πΎββͺ ran
(π βΎ πΆ))) |
128 | | df-ima 5689 |
. . . . . . . . . . . 12
β’ (π β πΆ) = ran (π βΎ πΆ) |
129 | 128 | unieqi 4921 |
. . . . . . . . . . 11
β’ βͺ (π
β πΆ) = βͺ ran (π βΎ πΆ) |
130 | 129 | fveq2i 6892 |
. . . . . . . . . 10
β’ (πΎββͺ (π
β πΆ)) = (πΎββͺ ran (π βΎ πΆ)) |
131 | 127, 130 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π β (πΊ DProd (π βΎ πΆ)) = (πΎββͺ (π β πΆ))) |
132 | 131 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πΊ DProd (π βΎ πΆ)) = (πΎββͺ (π β πΆ))) |
133 | 125, 132 | sseqtrrd 4023 |
. . . . . . 7
β’ ((π β§ π β πΆ) β (πΎββͺ (π β (πΆ β {π}))) β (πΊ DProd (π βΎ πΆ))) |
134 | 32 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β πΆ) β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) |
135 | 133, 134 | sstrd 3992 |
. . . . . 6
β’ ((π β§ π β πΆ) β (πΎββͺ (π β (πΆ β {π}))) β (πβ(πΊ DProd (π βΎ π·)))) |
136 | 119, 17 | lsmsubg 19517 |
. . . . . 6
β’ (((πΎββͺ (π
β (πΆ β {π}))) β (SubGrpβπΊ) β§ (πΊ DProd (π βΎ π·)) β (SubGrpβπΊ) β§ (πΎββͺ (π β (πΆ β {π}))) β (πβ(πΊ DProd (π βΎ π·)))) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·))) β (SubGrpβπΊ)) |
137 | 115, 118,
135, 136 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β πΆ) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·))) β (SubGrpβπΊ)) |
138 | 83 | mrcsscl 17561 |
. . . . 5
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ βͺ (π β (πΌ β {π})) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·))) β§ ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·))) β (SubGrpβπΊ)) β (πΎββͺ (π β (πΌ β {π}))) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·)))) |
139 | 60, 123, 137, 138 | syl3anc 1372 |
. . . 4
β’ ((π β§ π β πΆ) β (πΎββͺ (π β (πΌ β {π}))) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·)))) |
140 | | sslin 4234 |
. . . 4
β’ ((πΎββͺ (π
β (πΌ β {π}))) β ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·))) β ((πβπ) β© (πΎββͺ (π β (πΌ β {π})))) β ((πβπ) β© ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·))))) |
141 | 139, 140 | syl 17 |
. . 3
β’ ((π β§ π β πΆ) β ((πβπ) β© (πΎββͺ (π β (πΌ β {π})))) β ((πβπ) β© ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·))))) |
142 | 10 | sselda 3982 |
. . . . 5
β’ ((π β§ π β πΆ) β π β πΌ) |
143 | 8 | ffvelcdmda 7084 |
. . . . 5
β’ ((π β§ π β πΌ) β (πβπ) β (SubGrpβπΊ)) |
144 | 142, 143 | syldan 592 |
. . . 4
β’ ((π β§ π β πΆ) β (πβπ) β (SubGrpβπΊ)) |
145 | | dmdprdsplit.0 |
. . . 4
β’ 0 =
(0gβπΊ) |
146 | 19 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β ((π βΎ πΆ)βπ) = (πβπ)) |
147 | 6 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β πΊdom DProd (π βΎ πΆ)) |
148 | 12 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β dom (π βΎ πΆ) = πΆ) |
149 | 147, 148,
63 | dprdub 19890 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β ((π βΎ πΆ)βπ) β (πΊ DProd (π βΎ πΆ))) |
150 | 146, 149 | eqsstrrd 4021 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πβπ) β (πΊ DProd (π βΎ πΆ))) |
151 | | dprdsubg 19889 |
. . . . . . . . . . 11
β’ (πΊdom DProd (π βΎ πΆ) β (πΊ DProd (π βΎ πΆ)) β (SubGrpβπΊ)) |
152 | 6, 151 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΊ DProd (π βΎ πΆ)) β (SubGrpβπΊ)) |
153 | 152 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (πΊ DProd (π βΎ πΆ)) β (SubGrpβπΊ)) |
154 | 119 | lsmlub 19527 |
. . . . . . . . 9
β’ (((πβπ) β (SubGrpβπΊ) β§ (πΎββͺ (π β (πΆ β {π}))) β (SubGrpβπΊ) β§ (πΊ DProd (π βΎ πΆ)) β (SubGrpβπΊ)) β (((πβπ) β (πΊ DProd (π βΎ πΆ)) β§ (πΎββͺ (π β (πΆ β {π}))) β (πΊ DProd (π βΎ πΆ))) β ((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π})))) β (πΊ DProd (π βΎ πΆ)))) |
155 | 144, 115,
153, 154 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (((πβπ) β (πΊ DProd (π βΎ πΆ)) β§ (πΎββͺ (π β (πΆ β {π}))) β (πΊ DProd (π βΎ πΆ))) β ((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π})))) β (πΊ DProd (π βΎ πΆ)))) |
156 | 150, 133,
155 | mpbi2and 711 |
. . . . . . 7
β’ ((π β§ π β πΆ) β ((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π})))) β (πΊ DProd (π βΎ πΆ))) |
157 | 156 | ssrind 4235 |
. . . . . 6
β’ ((π β§ π β πΆ) β (((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π})))) β© (πΊ DProd (π βΎ π·))) β ((πΊ DProd (π βΎ πΆ)) β© (πΊ DProd (π βΎ π·)))) |
158 | | dmdprdsplit2.4 |
. . . . . . 7
β’ (π β ((πΊ DProd (π βΎ πΆ)) β© (πΊ DProd (π βΎ π·))) = { 0 }) |
159 | 158 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΆ) β ((πΊ DProd (π βΎ πΆ)) β© (πΊ DProd (π βΎ π·))) = { 0 }) |
160 | 157, 159 | sseqtrd 4022 |
. . . . 5
β’ ((π β§ π β πΆ) β (((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π})))) β© (πΊ DProd (π βΎ π·))) β { 0 }) |
161 | 119 | lsmub1 19520 |
. . . . . . . . 9
β’ (((πβπ) β (SubGrpβπΊ) β§ (πΎββͺ (π β (πΆ β {π}))) β (SubGrpβπΊ)) β (πβπ) β ((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π}))))) |
162 | 144, 115,
161 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πβπ) β ((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π}))))) |
163 | 145 | subg0cl 19009 |
. . . . . . . . 9
β’ ((πβπ) β (SubGrpβπΊ) β 0 β (πβπ)) |
164 | 144, 163 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β 0 β (πβπ)) |
165 | 162, 164 | sseldd 3983 |
. . . . . . 7
β’ ((π β§ π β πΆ) β 0 β ((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π}))))) |
166 | 145 | subg0cl 19009 |
. . . . . . . 8
β’ ((πΊ DProd (π βΎ π·)) β (SubGrpβπΊ) β 0 β (πΊ DProd (π βΎ π·))) |
167 | 118, 166 | syl 17 |
. . . . . . 7
β’ ((π β§ π β πΆ) β 0 β (πΊ DProd (π βΎ π·))) |
168 | 165, 167 | elind 4194 |
. . . . . 6
β’ ((π β§ π β πΆ) β 0 β (((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π})))) β© (πΊ DProd (π βΎ π·)))) |
169 | 168 | snssd 4812 |
. . . . 5
β’ ((π β§ π β πΆ) β { 0 } β (((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π})))) β© (πΊ DProd (π βΎ π·)))) |
170 | 160, 169 | eqssd 3999 |
. . . 4
β’ ((π β§ π β πΆ) β (((πβπ)(LSSumβπΊ)(πΎββͺ (π β (πΆ β {π})))) β© (πΊ DProd (π βΎ π·))) = { 0 }) |
171 | | resima2 6015 |
. . . . . . . . 9
β’ ((πΆ β {π}) β πΆ β ((π βΎ πΆ) β (πΆ β {π})) = (π β (πΆ β {π}))) |
172 | 84, 171 | mp1i 13 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β ((π βΎ πΆ) β (πΆ β {π})) = (π β (πΆ β {π}))) |
173 | 172 | unieqd 4922 |
. . . . . . 7
β’ ((π β§ π β πΆ) β βͺ
((π βΎ πΆ) β (πΆ β {π})) = βͺ (π β (πΆ β {π}))) |
174 | 173 | fveq2d 6893 |
. . . . . 6
β’ ((π β§ π β πΆ) β (πΎββͺ ((π βΎ πΆ) β (πΆ β {π}))) = (πΎββͺ (π β (πΆ β {π})))) |
175 | 146, 174 | ineq12d 4213 |
. . . . 5
β’ ((π β§ π β πΆ) β (((π βΎ πΆ)βπ) β© (πΎββͺ ((π βΎ πΆ) β (πΆ β {π})))) = ((πβπ) β© (πΎββͺ (π β (πΆ β {π}))))) |
176 | 147, 148,
63, 145, 83 | dprddisj 19874 |
. . . . 5
β’ ((π β§ π β πΆ) β (((π βΎ πΆ)βπ) β© (πΎββͺ ((π βΎ πΆ) β (πΆ β {π})))) = { 0 }) |
177 | 175, 176 | eqtr3d 2775 |
. . . 4
β’ ((π β§ π β πΆ) β ((πβπ) β© (πΎββͺ (π β (πΆ β {π})))) = { 0 }) |
178 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β π:πΌβΆ(SubGrpβπΊ)) |
179 | | ffun 6718 |
. . . . . . . 8
β’ (π:πΌβΆ(SubGrpβπΊ) β Fun π) |
180 | | funiunfv 7244 |
. . . . . . . 8
β’ (Fun
π β βͺ π¦ β (πΆ β {π})(πβπ¦) = βͺ (π β (πΆ β {π}))) |
181 | 178, 179,
180 | 3syl 18 |
. . . . . . 7
β’ ((π β§ π β πΆ) β βͺ
π¦ β (πΆ β {π})(πβπ¦) = βͺ (π β (πΆ β {π}))) |
182 | 6 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β πΊdom DProd (π βΎ πΆ)) |
183 | 12 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β dom (π βΎ πΆ) = πΆ) |
184 | | eldifi 4126 |
. . . . . . . . . . . 12
β’ (π¦ β (πΆ β {π}) β π¦ β πΆ) |
185 | 184 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β π¦ β πΆ) |
186 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β π β πΆ) |
187 | | eldifsni 4793 |
. . . . . . . . . . . 12
β’ (π¦ β (πΆ β {π}) β π¦ β π) |
188 | 187 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β π¦ β π) |
189 | 182, 183,
185, 186, 188, 17 | dprdcntz 19873 |
. . . . . . . . . 10
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β ((π βΎ πΆ)βπ¦) β (πβ((π βΎ πΆ)βπ))) |
190 | 185 | fvresd 6909 |
. . . . . . . . . 10
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β ((π βΎ πΆ)βπ¦) = (πβπ¦)) |
191 | 19 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β ((π βΎ πΆ)βπ) = (πβπ)) |
192 | 191 | fveq2d 6893 |
. . . . . . . . . 10
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β (πβ((π βΎ πΆ)βπ)) = (πβ(πβπ))) |
193 | 189, 190,
192 | 3sstr3d 4028 |
. . . . . . . . 9
β’ (((π β§ π β πΆ) β§ π¦ β (πΆ β {π})) β (πβπ¦) β (πβ(πβπ))) |
194 | 193 | ralrimiva 3147 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β βπ¦ β (πΆ β {π})(πβπ¦) β (πβ(πβπ))) |
195 | | iunss 5048 |
. . . . . . . 8
β’ (βͺ π¦ β (πΆ β {π})(πβπ¦) β (πβ(πβπ)) β βπ¦ β (πΆ β {π})(πβπ¦) β (πβ(πβπ))) |
196 | 194, 195 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β πΆ) β βͺ
π¦ β (πΆ β {π})(πβπ¦) β (πβ(πβπ))) |
197 | 181, 196 | eqsstrrd 4021 |
. . . . . 6
β’ ((π β§ π β πΆ) β βͺ (π β (πΆ β {π})) β (πβ(πβπ))) |
198 | 34 | subgss 19002 |
. . . . . . . 8
β’ ((πβπ) β (SubGrpβπΊ) β (πβπ) β (BaseβπΊ)) |
199 | 144, 198 | syl 17 |
. . . . . . 7
β’ ((π β§ π β πΆ) β (πβπ) β (BaseβπΊ)) |
200 | 34, 17 | cntzsubg 19198 |
. . . . . . 7
β’ ((πΊ β Grp β§ (πβπ) β (BaseβπΊ)) β (πβ(πβπ)) β (SubGrpβπΊ)) |
201 | 57, 199, 200 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β πΆ) β (πβ(πβπ)) β (SubGrpβπΊ)) |
202 | 83 | mrcsscl 17561 |
. . . . . 6
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ βͺ (π β (πΆ β {π})) β (πβ(πβπ)) β§ (πβ(πβπ)) β (SubGrpβπΊ)) β (πΎββͺ (π β (πΆ β {π}))) β (πβ(πβπ))) |
203 | 60, 197, 201, 202 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β πΆ) β (πΎββͺ (π β (πΆ β {π}))) β (πβ(πβπ))) |
204 | 17, 115, 144, 203 | cntzrecd 19541 |
. . . 4
β’ ((π β§ π β πΆ) β (πβπ) β (πβ(πΎββͺ (π β (πΆ β {π}))))) |
205 | 119, 144,
115, 118, 145, 170, 177, 17, 204 | lsmdisj3 19546 |
. . 3
β’ ((π β§ π β πΆ) β ((πβπ) β© ((πΎββͺ (π β (πΆ β {π})))(LSSumβπΊ)(πΊ DProd (π βΎ π·)))) = { 0 }) |
206 | 141, 205 | sseqtrd 4022 |
. 2
β’ ((π β§ π β πΆ) β ((πβπ) β© (πΎββͺ (π β (πΌ β {π})))) β { 0 }) |
207 | 54, 206 | jca 513 |
1
β’ ((π β§ π β πΆ) β ((π β πΌ β (π β π β (πβπ) β (πβ(πβπ)))) β§ ((πβπ) β© (πΎββͺ (π β (πΌ β {π})))) β { 0 })) |