dmdprdsplit2lem

	Ref	Expression
Hypotheses	dprdsplit.2	$⊢ φ \to S : I ⟶ SubGrp (G)$
	dprdsplit.i	$⊢ φ \to C \cap D = \emptyset$
	dprdsplit.u	$⊢ φ \to I = C \cup D$
	dmdprdsplit.z	$⊢ Z = Cntz (G)$
	dmdprdsplit.0	$⊢ \underset{˙}{0} = 0_{G}$
	dmdprdsplit2.1	$⊢ φ \to G dom DProd ({S ↾}_{C})$
	dmdprdsplit2.2	$⊢ φ \to G dom DProd ({S ↾}_{D})$
	dmdprdsplit2.3	$⊢ φ \to G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D}))$
	dmdprdsplit2.4	$⊢ φ \to (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\}$
	dmdprdsplit2lem.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	dmdprdsplit2lem	$⊢ (φ \land X \in C) \to ((Y \in I \to (X \neq Y \to S (X) \subseteq Z (S (Y)))) \land S (X) \cap K (⋃ S [I ∖ \{X\}]) \subseteq \{\underset{˙}{0}\})$

Proof

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

Metamath Proof Explorer

Theorem dmdprdsplit2lem

Proof