Metamath Proof Explorer


Theorem dmdprdsplit2lem

Description: Lemma for dmdprdsplit . (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dprdsplit.2 φ S : I SubGrp G
dprdsplit.i φ C D =
dprdsplit.u φ I = C D
dmdprdsplit.z Z = Cntz G
dmdprdsplit.0 0 ˙ = 0 G
dmdprdsplit2.1 φ G dom DProd S C
dmdprdsplit2.2 φ G dom DProd S D
dmdprdsplit2.3 φ G DProd S C Z G DProd S D
dmdprdsplit2.4 φ G DProd S C G DProd S D = 0 ˙
dmdprdsplit2lem.k K = mrCls SubGrp G
Assertion dmdprdsplit2lem φ X C Y I X Y S X Z S Y S X K S I X 0 ˙

Proof

Step Hyp Ref Expression
1 dprdsplit.2 φ S : I SubGrp G
2 dprdsplit.i φ C D =
3 dprdsplit.u φ I = C D
4 dmdprdsplit.z Z = Cntz G
5 dmdprdsplit.0 0 ˙ = 0 G
6 dmdprdsplit2.1 φ G dom DProd S C
7 dmdprdsplit2.2 φ G dom DProd S D
8 dmdprdsplit2.3 φ G DProd S C Z G DProd S D
9 dmdprdsplit2.4 φ G DProd S C G DProd S D = 0 ˙
10 dmdprdsplit2lem.k K = mrCls SubGrp G
11 3 adantr φ X C I = C D
12 11 eleq2d φ X C Y I Y C D
13 elun Y C D Y C Y D
14 12 13 bitrdi φ X C Y I Y C Y D
15 6 ad2antrr φ X C Y C X Y G dom DProd S C
16 ssun1 C C D
17 16 3 sseqtrrid φ C I
18 1 17 fssresd φ S C : C SubGrp G
19 18 fdmd φ dom S C = C
20 19 ad2antrr φ X C Y C X Y dom S C = C
21 simplr φ X C Y C X Y X C
22 simprl φ X C Y C X Y Y C
23 simprr φ X C Y C X Y X Y
24 15 20 21 22 23 4 dprdcntz φ X C Y C X Y S C X Z S C Y
25 fvres X C S C X = S X
26 25 ad2antlr φ X C Y C X Y S C X = S X
27 fvres Y C S C Y = S Y
28 27 ad2antrl φ X C Y C X Y S C Y = S Y
29 28 fveq2d φ X C Y C X Y Z S C Y = Z S Y
30 24 26 29 3sstr3d φ X C Y C X Y S X Z S Y
31 30 exp32 φ X C Y C X Y S X Z S Y
32 25 ad2antlr φ X C Y D X Y S C X = S X
33 6 ad2antrr φ X C Y D X Y G dom DProd S C
34 19 ad2antrr φ X C Y D X Y dom S C = C
35 simplr φ X C Y D X Y X C
36 33 34 35 dprdub φ X C Y D X Y S C X G DProd S C
37 32 36 eqsstrrd φ X C Y D X Y S X G DProd S C
38 8 ad2antrr φ X C Y D X Y G DProd S C Z G DProd S D
39 eqid Base G = Base G
40 39 dprdssv G DProd S D Base G
41 fvres Y D S D Y = S Y
42 41 ad2antrl φ X C Y D X Y S D Y = S Y
43 7 ad2antrr φ X C Y D X Y G dom DProd S D
44 ssun2 D C D
45 44 3 sseqtrrid φ D I
46 1 45 fssresd φ S D : D SubGrp G
47 46 fdmd φ dom S D = D
48 47 ad2antrr φ X C Y D X Y dom S D = D
49 simprl φ X C Y D X Y Y D
50 43 48 49 dprdub φ X C Y D X Y S D Y G DProd S D
51 42 50 eqsstrrd φ X C Y D X Y S Y G DProd S D
52 39 4 cntz2ss G DProd S D Base G S Y G DProd S D Z G DProd S D Z S Y
53 40 51 52 sylancr φ X C Y D X Y Z G DProd S D Z S Y
54 38 53 sstrd φ X C Y D X Y G DProd S C Z S Y
55 37 54 sstrd φ X C Y D X Y S X Z S Y
56 55 exp32 φ X C Y D X Y S X Z S Y
57 31 56 jaod φ X C Y C Y D X Y S X Z S Y
58 14 57 sylbid φ X C Y I X Y S X Z S Y
59 dprdgrp G dom DProd S C G Grp
60 6 59 syl φ G Grp
61 60 adantr φ X C G Grp
62 39 subgacs G Grp SubGrp G ACS Base G
63 acsmre SubGrp G ACS Base G SubGrp G Moore Base G
64 61 62 63 3syl φ X C SubGrp G Moore Base G
65 difundir C D X = C X D X
66 11 difeq1d φ X C I X = C D X
67 simpr φ X C X C
68 67 snssd φ X C X C
69 sslin X C D X D C
70 68 69 syl φ X C D X D C
71 incom C D = D C
72 2 adantr φ X C C D =
73 71 72 eqtr3id φ X C D C =
74 sseq0 D X D C D C = D X =
75 70 73 74 syl2anc φ X C D X =
76 disj3 D X = D = D X
77 75 76 sylib φ X C D = D X
78 77 uneq2d φ X C C X D = C X D X
79 65 66 78 3eqtr4a φ X C I X = C X D
80 79 imaeq2d φ X C S I X = S C X D
81 imaundi S C X D = S C X S D
82 80 81 eqtrdi φ X C S I X = S C X S D
83 82 unieqd φ X C S I X = S C X S D
84 uniun S C X S D = S C X S D
85 83 84 eqtrdi φ X C S I X = S C X S D
86 difss C X C
87 imass2 C X C S C X S C
88 uniss S C X S C S C X S C
89 86 87 88 mp2b S C X S C
90 imassrn S C ran S
91 1 frnd φ ran S SubGrp G
92 91 adantr φ X C ran S SubGrp G
93 mresspw SubGrp G Moore Base G SubGrp G 𝒫 Base G
94 64 93 syl φ X C SubGrp G 𝒫 Base G
95 92 94 sstrd φ X C ran S 𝒫 Base G
96 90 95 sstrid φ X C S C 𝒫 Base G
97 sspwuni S C 𝒫 Base G S C Base G
98 96 97 sylib φ X C S C Base G
99 89 98 sstrid φ X C S C X Base G
100 64 10 99 mrcssidd φ X C S C X K S C X
101 imassrn S D ran S
102 101 95 sstrid φ X C S D 𝒫 Base G
103 sspwuni S D 𝒫 Base G S D Base G
104 102 103 sylib φ X C S D Base G
105 64 10 104 mrcssidd φ X C S D K S D
106 10 dprdspan G dom DProd S D G DProd S D = K ran S D
107 7 106 syl φ G DProd S D = K ran S D
108 df-ima S D = ran S D
109 108 unieqi S D = ran S D
110 109 fveq2i K S D = K ran S D
111 107 110 eqtr4di φ G DProd S D = K S D
112 111 adantr φ X C G DProd S D = K S D
113 105 112 sseqtrrd φ X C S D G DProd S D
114 unss12 S C X K S C X S D G DProd S D S C X S D K S C X G DProd S D
115 100 113 114 syl2anc φ X C S C X S D K S C X G DProd S D
116 10 mrccl SubGrp G Moore Base G S C X Base G K S C X SubGrp G
117 64 99 116 syl2anc φ X C K S C X SubGrp G
118 dprdsubg G dom DProd S D G DProd S D SubGrp G
119 7 118 syl φ G DProd S D SubGrp G
120 119 adantr φ X C G DProd S D SubGrp G
121 eqid LSSum G = LSSum G
122 121 lsmunss K S C X SubGrp G G DProd S D SubGrp G K S C X G DProd S D K S C X LSSum G G DProd S D
123 117 120 122 syl2anc φ X C K S C X G DProd S D K S C X LSSum G G DProd S D
124 115 123 sstrd φ X C S C X S D K S C X LSSum G G DProd S D
125 85 124 eqsstrd φ X C S I X K S C X LSSum G G DProd S D
126 89 a1i φ X C S C X S C
127 64 10 126 98 mrcssd φ X C K S C X K S C
128 10 dprdspan G dom DProd S C G DProd S C = K ran S C
129 6 128 syl φ G DProd S C = K ran S C
130 df-ima S C = ran S C
131 130 unieqi S C = ran S C
132 131 fveq2i K S C = K ran S C
133 129 132 eqtr4di φ G DProd S C = K S C
134 133 adantr φ X C G DProd S C = K S C
135 127 134 sseqtrrd φ X C K S C X G DProd S C
136 8 adantr φ X C G DProd S C Z G DProd S D
137 135 136 sstrd φ X C K S C X Z G DProd S D
138 121 4 lsmsubg K S C X SubGrp G G DProd S D SubGrp G K S C X Z G DProd S D K S C X LSSum G G DProd S D SubGrp G
139 117 120 137 138 syl3anc φ X C K S C X LSSum G G DProd S D SubGrp G
140 10 mrcsscl SubGrp G Moore Base G S I X K S C X LSSum G G DProd S D K S C X LSSum G G DProd S D SubGrp G K S I X K S C X LSSum G G DProd S D
141 64 125 139 140 syl3anc φ X C K S I X K S C X LSSum G G DProd S D
142 sslin K S I X K S C X LSSum G G DProd S D S X K S I X S X K S C X LSSum G G DProd S D
143 141 142 syl φ X C S X K S I X S X K S C X LSSum G G DProd S D
144 17 sselda φ X C X I
145 1 ffvelrnda φ X I S X SubGrp G
146 144 145 syldan φ X C S X SubGrp G
147 25 adantl φ X C S C X = S X
148 6 adantr φ X C G dom DProd S C
149 19 adantr φ X C dom S C = C
150 148 149 67 dprdub φ X C S C X G DProd S C
151 147 150 eqsstrrd φ X C S X G DProd S C
152 dprdsubg G dom DProd S C G DProd S C SubGrp G
153 6 152 syl φ G DProd S C SubGrp G
154 153 adantr φ X C G DProd S C SubGrp G
155 121 lsmlub S X SubGrp G K S C X SubGrp G G DProd S C SubGrp G S X G DProd S C K S C X G DProd S C S X LSSum G K S C X G DProd S C
156 146 117 154 155 syl3anc φ X C S X G DProd S C K S C X G DProd S C S X LSSum G K S C X G DProd S C
157 151 135 156 mpbi2and φ X C S X LSSum G K S C X G DProd S C
158 157 ssrind φ X C S X LSSum G K S C X G DProd S D G DProd S C G DProd S D
159 9 adantr φ X C G DProd S C G DProd S D = 0 ˙
160 158 159 sseqtrd φ X C S X LSSum G K S C X G DProd S D 0 ˙
161 121 lsmub1 S X SubGrp G K S C X SubGrp G S X S X LSSum G K S C X
162 146 117 161 syl2anc φ X C S X S X LSSum G K S C X
163 5 subg0cl S X SubGrp G 0 ˙ S X
164 146 163 syl φ X C 0 ˙ S X
165 162 164 sseldd φ X C 0 ˙ S X LSSum G K S C X
166 5 subg0cl G DProd S D SubGrp G 0 ˙ G DProd S D
167 120 166 syl φ X C 0 ˙ G DProd S D
168 165 167 elind φ X C 0 ˙ S X LSSum G K S C X G DProd S D
169 168 snssd φ X C 0 ˙ S X LSSum G K S C X G DProd S D
170 160 169 eqssd φ X C S X LSSum G K S C X G DProd S D = 0 ˙
171 resima2 C X C S C C X = S C X
172 86 171 mp1i φ X C S C C X = S C X
173 172 unieqd φ X C S C C X = S C X
174 173 fveq2d φ X C K S C C X = K S C X
175 147 174 ineq12d φ X C S C X K S C C X = S X K S C X
176 148 149 67 5 10 dprddisj φ X C S C X K S C C X = 0 ˙
177 175 176 eqtr3d φ X C S X K S C X = 0 ˙
178 1 adantr φ X C S : I SubGrp G
179 ffun S : I SubGrp G Fun S
180 funiunfv Fun S y C X S y = S C X
181 178 179 180 3syl φ X C y C X S y = S C X
182 6 ad2antrr φ X C y C X G dom DProd S C
183 19 ad2antrr φ X C y C X dom S C = C
184 eldifi y C X y C
185 184 adantl φ X C y C X y C
186 simplr φ X C y C X X C
187 eldifsni y C X y X
188 187 adantl φ X C y C X y X
189 182 183 185 186 188 4 dprdcntz φ X C y C X S C y Z S C X
190 185 fvresd φ X C y C X S C y = S y
191 25 ad2antlr φ X C y C X S C X = S X
192 191 fveq2d φ X C y C X Z S C X = Z S X
193 189 190 192 3sstr3d φ X C y C X S y Z S X
194 193 ralrimiva φ X C y C X S y Z S X
195 iunss y C X S y Z S X y C X S y Z S X
196 194 195 sylibr φ X C y C X S y Z S X
197 181 196 eqsstrrd φ X C S C X Z S X
198 39 subgss S X SubGrp G S X Base G
199 146 198 syl φ X C S X Base G
200 39 4 cntzsubg G Grp S X Base G Z S X SubGrp G
201 61 199 200 syl2anc φ X C Z S X SubGrp G
202 10 mrcsscl SubGrp G Moore Base G S C X Z S X Z S X SubGrp G K S C X Z S X
203 64 197 201 202 syl3anc φ X C K S C X Z S X
204 4 117 146 203 cntzrecd φ X C S X Z K S C X
205 121 146 117 120 5 170 177 4 204 lsmdisj3 φ X C S X K S C X LSSum G G DProd S D = 0 ˙
206 143 205 sseqtrd φ X C S X K S I X 0 ˙
207 58 206 jca φ X C Y I X Y S X Z S Y S X K S I X 0 ˙