Theorem dmdprdsplit2lem 18267

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

Hypotheses

Ref	Expression
dprdsplit.2	⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))
dprdsplit.i	⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)
dprdsplit.u	⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷))
dmdprdsplit.z	⊢ 𝑍 = (Cntz‘𝐺)
dmdprdsplit.0	⊢ 0 = (0g‘𝐺)
dmdprdsplit2.1	⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶))
dmdprdsplit2.2	⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷))
dmdprdsplit2.3	⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))
dmdprdsplit2.4	⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 })
dmdprdsplit2lem.k	⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))

Assertion

Ref	Expression
dmdprdsplit2lem	⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑌 ∈ 𝐼 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))) ∧ ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 }))

Proof of Theorem dmdprdsplit2lem

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dprdsplit.u	. . . . . 6 ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷))
2	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐼 = (𝐶 ∪ 𝐷))
3	2	eleq2d 2673	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐼 ↔ 𝑌 ∈ (𝐶 ∪ 𝐷)))
4		elun 3715	. . . 4 ⊢ (𝑌 ∈ (𝐶 ∪ 𝐷) ↔ (𝑌 ∈ 𝐶 ∨ 𝑌 ∈ 𝐷))
5	3, 4	syl6bb 275	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐼 ↔ (𝑌 ∈ 𝐶 ∨ 𝑌 ∈ 𝐷)))
6		dmdprdsplit2.1	. . . . . . . 8 ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶))
7	6	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → 𝐺dom DProd (𝑆 ↾ 𝐶))
8		dprdsplit.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))
9		ssun1 3738	. . . . . . . . . . 11 ⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷)
10	9, 1	syl5sseqr 3617	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ⊆ 𝐼)
11	8, 10	fssresd 5984	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ↾ 𝐶):𝐶⟶(SubGrp‘𝐺))
12		fdm 5964	. . . . . . . . 9 ⊢ ((𝑆 ↾ 𝐶):𝐶⟶(SubGrp‘𝐺) → dom (𝑆 ↾ 𝐶) = 𝐶)
13	11, 12	syl 17	. . . . . . . 8 ⊢ (𝜑 → dom (𝑆 ↾ 𝐶) = 𝐶)
14	13	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → dom (𝑆 ↾ 𝐶) = 𝐶)
15		simplr 788	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ 𝐶)
16		simprl 790	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ 𝐶)
17		simprr 792	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ≠ 𝑌)
18		dmdprdsplit.z	. . . . . . 7 ⊢ 𝑍 = (Cntz‘𝐺)
19	7, 14, 15, 16, 17, 18	dprdcntz 18230	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑋) ⊆ (𝑍‘((𝑆 ↾ 𝐶)‘𝑌)))
20		fvres 6117	. . . . . . 7 ⊢ (𝑋 ∈ 𝐶 → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋))
21	20	ad2antlr 759	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋))
22		fvres 6117	. . . . . . . 8 ⊢ (𝑌 ∈ 𝐶 → ((𝑆 ↾ 𝐶)‘𝑌) = (𝑆‘𝑌))
23	22	ad2antrl 760	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑌) = (𝑆‘𝑌))
24	23	fveq2d 6107	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → (𝑍‘((𝑆 ↾ 𝐶)‘𝑌)) = (𝑍‘(𝑆‘𝑌)))
25	19, 21, 24	3sstr3d 3610	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))
26	25	exp32 629	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐶 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))))
27	20	ad2antlr 759	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋))
28	6	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝐺dom DProd (𝑆 ↾ 𝐶))
29	13	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → dom (𝑆 ↾ 𝐶) = 𝐶)
30		simplr 788	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ 𝐶)
31	28, 29, 30	dprdub 18247	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))
32	27, 31	eqsstr3d 3603	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝑆‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))
33		dmdprdsplit2.3	. . . . . . . 8 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))
34	33	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))
35		eqid 2610	. . . . . . . . 9 ⊢ (Base‘𝐺) = (Base‘𝐺)
36	35	dprdssv 18238	. . . . . . . 8 ⊢ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (Base‘𝐺)
37		fvres 6117	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝐷 → ((𝑆 ↾ 𝐷)‘𝑌) = (𝑆‘𝑌))
38	37	ad2antrl 760	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐷)‘𝑌) = (𝑆‘𝑌))
39		dmdprdsplit2.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷))
40	39	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝐺dom DProd (𝑆 ↾ 𝐷))
41		ssun2 3739	. . . . . . . . . . . . . 14 ⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷)
42	41, 1	syl5sseqr 3617	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ⊆ 𝐼)
43	8, 42	fssresd 5984	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺))
44		fdm 5964	. . . . . . . . . . . 12 ⊢ ((𝑆 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺) → dom (𝑆 ↾ 𝐷) = 𝐷)
45	43, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑆 ↾ 𝐷) = 𝐷)
46	45	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → dom (𝑆 ↾ 𝐷) = 𝐷)
47		simprl 790	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ 𝐷)
48	40, 46, 47	dprdub 18247	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐷)‘𝑌) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷)))
49	38, 48	eqsstr3d 3603	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝑆‘𝑌) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷)))
50	35, 18	cntz2ss 17588	. . . . . . . 8 ⊢ (((𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑌) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) → (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝑍‘(𝑆‘𝑌)))
51	36, 49, 50	sylancr 694	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝑍‘(𝑆‘𝑌)))
52	34, 51	sstrd 3578	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝑆‘𝑌)))
53	32, 52	sstrd 3578	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))
54	53	exp32 629	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐷 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))))
55	26, 54	jaod 394	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑌 ∈ 𝐶 ∨ 𝑌 ∈ 𝐷) → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))))
56	5, 55	sylbid 229	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐼 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))))
57		dprdgrp 18227	. . . . . . . 8 ⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → 𝐺 ∈ Grp)
58	6, 57	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Grp)
59	58	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐺 ∈ Grp)
60	35	subgacs 17452	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
61		acsmre 16136	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
62	59, 60, 61	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
63		difundir 3839	. . . . . . . . . . 11 ⊢ ((𝐶 ∪ 𝐷) ∖ {𝑋}) = ((𝐶 ∖ {𝑋}) ∪ (𝐷 ∖ {𝑋}))
64	2	difeq1d 3689	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐼 ∖ {𝑋}) = ((𝐶 ∪ 𝐷) ∖ {𝑋}))
65		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝐶)
66	65	snssd 4281	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → {𝑋} ⊆ 𝐶)
67		sslin 3801	. . . . . . . . . . . . . . 15 ⊢ ({𝑋} ⊆ 𝐶 → (𝐷 ∩ {𝑋}) ⊆ (𝐷 ∩ 𝐶))
68	66, 67	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐷 ∩ {𝑋}) ⊆ (𝐷 ∩ 𝐶))
69		incom 3767	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∩ 𝐷) = (𝐷 ∩ 𝐶)
70		dprdsplit.i	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)
71	70	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐶 ∩ 𝐷) = ∅)
72	69, 71	syl5eqr 2658	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐷 ∩ 𝐶) = ∅)
73		sseq0 3927	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∩ {𝑋}) ⊆ (𝐷 ∩ 𝐶) ∧ (𝐷 ∩ 𝐶) = ∅) → (𝐷 ∩ {𝑋}) = ∅)
74	68, 72, 73	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐷 ∩ {𝑋}) = ∅)
75		disj3 3973	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∩ {𝑋}) = ∅ ↔ 𝐷 = (𝐷 ∖ {𝑋}))
76	74, 75	sylib 207	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐷 = (𝐷 ∖ {𝑋}))
77	76	uneq2d 3729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐶 ∖ {𝑋}) ∪ 𝐷) = ((𝐶 ∖ {𝑋}) ∪ (𝐷 ∖ {𝑋})))
78	63, 64, 77	3eqtr4a 2670	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐼 ∖ {𝑋}) = ((𝐶 ∖ {𝑋}) ∪ 𝐷))
79	78	imaeq2d 5385	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) = (𝑆 “ ((𝐶 ∖ {𝑋}) ∪ 𝐷)))
80		imaundi 5464	. . . . . . . . 9 ⊢ (𝑆 “ ((𝐶 ∖ {𝑋}) ∪ 𝐷)) = ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆 “ 𝐷))
81	79, 80	syl6eq 2660	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) = ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆 “ 𝐷)))
82	81	unieqd 4382	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐼 ∖ {𝑋})) = ∪ ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆 “ 𝐷)))
83		uniun 4392	. . . . . . 7 ⊢ ∪ ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆 “ 𝐷)) = (∪ (𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪ (𝑆 “ 𝐷))
84	82, 83	syl6eq 2660	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐼 ∖ {𝑋})) = (∪ (𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪ (𝑆 “ 𝐷)))
85		dmdprdsplit2lem.k	. . . . . . . . 9 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))
86		difss 3699	. . . . . . . . . . 11 ⊢ (𝐶 ∖ {𝑋}) ⊆ 𝐶
87		imass2 5420	. . . . . . . . . . 11 ⊢ ((𝐶 ∖ {𝑋}) ⊆ 𝐶 → (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆 “ 𝐶))
88		uniss 4394	. . . . . . . . . . 11 ⊢ ((𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆 “ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ ∪ (𝑆 “ 𝐶))
89	86, 87, 88	mp2b 10	. . . . . . . . . 10 ⊢ ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ ∪ (𝑆 “ 𝐶)
90		imassrn 5396	. . . . . . . . . . . 12 ⊢ (𝑆 “ 𝐶) ⊆ ran 𝑆
91		frn 5966	. . . . . . . . . . . . . . 15 ⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺))
92	8, 91	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
93	92	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ran 𝑆 ⊆ (SubGrp‘𝐺))
94		mresspw 16075	. . . . . . . . . . . . . 14 ⊢ ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
95	62, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
96	93, 95	sstrd 3578	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
97	90, 96	syl5ss 3579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆 “ 𝐶) ⊆ 𝒫 (Base‘𝐺))
98		sspwuni 4547	. . . . . . . . . . 11 ⊢ ((𝑆 “ 𝐶) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ 𝐶) ⊆ (Base‘𝐺))
99	97, 98	sylib 207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ 𝐶) ⊆ (Base‘𝐺))
100	89, 99	syl5ss 3579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (Base‘𝐺))
101	62, 85, 100	mrcssidd 16108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))))
102		imassrn 5396	. . . . . . . . . . . 12 ⊢ (𝑆 “ 𝐷) ⊆ ran 𝑆
103	102, 96	syl5ss 3579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆 “ 𝐷) ⊆ 𝒫 (Base‘𝐺))
104		sspwuni 4547	. . . . . . . . . . 11 ⊢ ((𝑆 “ 𝐷) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ 𝐷) ⊆ (Base‘𝐺))
105	103, 104	sylib 207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ 𝐷) ⊆ (Base‘𝐺))
106	62, 85, 105	mrcssidd 16108	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ 𝐷) ⊆ (𝐾‘∪ (𝑆 “ 𝐷)))
107	85	dprdspan 18249	. . . . . . . . . . . 12 ⊢ (𝐺dom DProd (𝑆 ↾ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) = (𝐾‘∪ ran (𝑆 ↾ 𝐷)))
108	39, 107	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) = (𝐾‘∪ ran (𝑆 ↾ 𝐷)))
109		df-ima 5051	. . . . . . . . . . . . 13 ⊢ (𝑆 “ 𝐷) = ran (𝑆 ↾ 𝐷)
110	109	unieqi 4381	. . . . . . . . . . . 12 ⊢ ∪ (𝑆 “ 𝐷) = ∪ ran (𝑆 ↾ 𝐷)
111	110	fveq2i 6106	. . . . . . . . . . 11 ⊢ (𝐾‘∪ (𝑆 “ 𝐷)) = (𝐾‘∪ ran (𝑆 ↾ 𝐷))
112	108, 111	syl6eqr 2662	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) = (𝐾‘∪ (𝑆 “ 𝐷)))
113	112	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐷)) = (𝐾‘∪ (𝑆 “ 𝐷)))
114	106, 113	sseqtr4d 3605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ 𝐷) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷)))
115		unss12 3747	. . . . . . . 8 ⊢ ((∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∧ ∪ (𝑆 “ 𝐷) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) → (∪ (𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪ (𝑆 “ 𝐷)) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆 ↾ 𝐷))))
116	101, 114, 115	syl2anc 691	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (∪ (𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪ (𝑆 “ 𝐷)) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆 ↾ 𝐷))))
117	85	mrccl 16094	. . . . . . . . 9 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺))
118	62, 100, 117	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺))
119		dprdsubg 18246	. . . . . . . . . 10 ⊢ (𝐺dom DProd (𝑆 ↾ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
120	39, 119	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
121	120	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
122		eqid 2610	. . . . . . . . 9 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
123	122	lsmunss 17896	. . . . . . . 8 ⊢ (((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) → ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))))
124	118, 121, 123	syl2anc 691	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))))
125	116, 124	sstrd 3578	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (∪ (𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪ (𝑆 “ 𝐷)) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))))
126	84, 125	eqsstrd 3602	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐼 ∖ {𝑋})) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))))
127	89	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ ∪ (𝑆 “ 𝐶))
128	62, 85, 127, 99	mrcssd 16107	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐾‘∪ (𝑆 “ 𝐶)))
129	85	dprdspan 18249	. . . . . . . . . . 11 ⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) = (𝐾‘∪ ran (𝑆 ↾ 𝐶)))
130	6, 129	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) = (𝐾‘∪ ran (𝑆 ↾ 𝐶)))
131		df-ima 5051	. . . . . . . . . . . 12 ⊢ (𝑆 “ 𝐶) = ran (𝑆 ↾ 𝐶)
132	131	unieqi 4381	. . . . . . . . . . 11 ⊢ ∪ (𝑆 “ 𝐶) = ∪ ran (𝑆 ↾ 𝐶)
133	132	fveq2i 6106	. . . . . . . . . 10 ⊢ (𝐾‘∪ (𝑆 “ 𝐶)) = (𝐾‘∪ ran (𝑆 ↾ 𝐶))
134	130, 133	syl6eqr 2662	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) = (𝐾‘∪ (𝑆 “ 𝐶)))
135	134	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) = (𝐾‘∪ (𝑆 “ 𝐶)))
136	128, 135	sseqtr4d 3605	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))
137	33	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))
138	136, 137	sstrd 3578	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))
139	122, 18	lsmsubg 17892	. . . . . 6 ⊢ (((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) → ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺))
140	118, 121, 138, 139	syl3anc 1318	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺))
141	85	mrcsscl 16103	. . . . 5 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐼 ∖ {𝑋})) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) ∧ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))))
142	62, 126, 140, 141	syl3anc 1318	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))))
143		sslin 3801	. . . 4 ⊢ ((𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ ((𝑆‘𝑋) ∩ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))))
144	142, 143	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ ((𝑆‘𝑋) ∩ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))))
145	10	sselda 3568	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝐼)
146	8	ffvelrnda 6267	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐼) → (𝑆‘𝑋) ∈ (SubGrp‘𝐺))
147	145, 146	syldan 486	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ∈ (SubGrp‘𝐺))
148		dmdprdsplit.0	. . . 4 ⊢ 0 = (0g‘𝐺)
149	20	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋))
150	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐺dom DProd (𝑆 ↾ 𝐶))
151	13	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → dom (𝑆 ↾ 𝐶) = 𝐶)
152	150, 151, 65	dprdub 18247	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))
153	149, 152	eqsstr3d 3603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))
154		dprdsubg 18246	. . . . . . . . . . 11 ⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺))
155	6, 154	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺))
156	155	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺))
157	122	lsmlub 17901	. . . . . . . . 9 ⊢ (((𝑆‘𝑋) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) → (((𝑆‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) ↔ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))))
158	147, 118, 156, 157	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) ↔ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))))
159	153, 136, 158	mpbi2and 958	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))
160		ssrin 3800	. . . . . . 7 ⊢ (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)) → (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))))
161	159, 160	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))))
162		dmdprdsplit2.4	. . . . . . 7 ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 })
163	162	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 })
164	161, 163	sseqtrd 3604	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ { 0 })
165	122	lsmub1 17894	. . . . . . . . 9 ⊢ (((𝑆‘𝑋) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑋) ⊆ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))))
166	147, 118, 165	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ⊆ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))))
167	148	subg0cl 17425	. . . . . . . . 9 ⊢ ((𝑆‘𝑋) ∈ (SubGrp‘𝐺) → 0 ∈ (𝑆‘𝑋))
168	147, 167	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 0 ∈ (𝑆‘𝑋))
169	166, 168	sseldd 3569	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 0 ∈ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))))
170	148	subg0cl 17425	. . . . . . . 8 ⊢ ((𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → 0 ∈ (𝐺 DProd (𝑆 ↾ 𝐷)))
171	121, 170	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 0 ∈ (𝐺 DProd (𝑆 ↾ 𝐷)))
172	169, 171	elind 3760	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 0 ∈ (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))))
173	172	snssd 4281	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → { 0 } ⊆ (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))))
174	164, 173	eqssd 3585	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 })
175		resima2 5352	. . . . . . . . 9 ⊢ ((𝐶 ∖ {𝑋}) ⊆ 𝐶 → ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})) = (𝑆 “ (𝐶 ∖ {𝑋})))
176	86, 175	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})) = (𝑆 “ (𝐶 ∖ {𝑋})))
177	176	unieqd 4382	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})) = ∪ (𝑆 “ (𝐶 ∖ {𝑋})))
178	177	fveq2d 6107	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋}))) = (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))))
179	149, 178	ineq12d 3777	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆 ↾ 𝐶)‘𝑋) ∩ (𝐾‘∪ ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})))) = ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))))
180	150, 151, 65, 148, 85	dprddisj 18231	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆 ↾ 𝐶)‘𝑋) ∩ (𝐾‘∪ ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})))) = { 0 })
181	179, 180	eqtr3d 2646	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) = { 0 })
182	8	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑆:𝐼⟶(SubGrp‘𝐺))
183		ffun 5961	. . . . . . . 8 ⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → Fun 𝑆)
184		funiunfv 6410	. . . . . . . 8 ⊢ (Fun 𝑆 → ∪ 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) = ∪ (𝑆 “ (𝐶 ∖ {𝑋})))
185	182, 183, 184	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) = ∪ (𝑆 “ (𝐶 ∖ {𝑋})))
186	6	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝐺dom DProd (𝑆 ↾ 𝐶))
187	13	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → dom (𝑆 ↾ 𝐶) = 𝐶)
188		eldifi 3694	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐶 ∖ {𝑋}) → 𝑦 ∈ 𝐶)
189	188	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑦 ∈ 𝐶)
190		simplr 788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑋 ∈ 𝐶)
191		eldifsni 4261	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐶 ∖ {𝑋}) → 𝑦 ≠ 𝑋)
192	191	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑦 ≠ 𝑋)
193	186, 187, 189, 190, 192, 18	dprdcntz 18230	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆 ↾ 𝐶)‘𝑦) ⊆ (𝑍‘((𝑆 ↾ 𝐶)‘𝑋)))
194		fvres 6117	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐶 → ((𝑆 ↾ 𝐶)‘𝑦) = (𝑆‘𝑦))
195	189, 194	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆 ↾ 𝐶)‘𝑦) = (𝑆‘𝑦))
196	20	ad2antlr 759	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋))
197	196	fveq2d 6107	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → (𝑍‘((𝑆 ↾ 𝐶)‘𝑋)) = (𝑍‘(𝑆‘𝑋)))
198	193, 195, 197	3sstr3d 3610	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → (𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋)))
199	198	ralrimiva 2949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∀𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋)))
200		iunss 4497	. . . . . . . 8 ⊢ (∪ 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋)) ↔ ∀𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋)))
201	199, 200	sylibr 223	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋)))
202	185, 201	eqsstr3d 3603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑍‘(𝑆‘𝑋)))
203	35	subgss 17418	. . . . . . . 8 ⊢ ((𝑆‘𝑋) ∈ (SubGrp‘𝐺) → (𝑆‘𝑋) ⊆ (Base‘𝐺))
204	147, 203	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ⊆ (Base‘𝐺))
205	35, 18	cntzsubg 17592	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑆‘𝑋) ⊆ (Base‘𝐺)) → (𝑍‘(𝑆‘𝑋)) ∈ (SubGrp‘𝐺))
206	59, 204, 205	syl2anc 691	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑍‘(𝑆‘𝑋)) ∈ (SubGrp‘𝐺))
207	85	mrcsscl 16103	. . . . . 6 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑍‘(𝑆‘𝑋)) ∧ (𝑍‘(𝑆‘𝑋)) ∈ (SubGrp‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝑆‘𝑋)))
208	62, 202, 206, 207	syl3anc 1318	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝑆‘𝑋)))
209	18, 118, 147, 208	cntzrecd 17914	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ⊆ (𝑍‘(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))))
210	122, 147, 118, 121, 148, 174, 181, 18, 209	lsmdisj3 17919	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋) ∩ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))) = { 0 })
211	144, 210	sseqtrd 3604	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 })
212	56, 211	jca 553	1 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑌 ∈ 𝐼 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))) ∧ ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 }))

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∪ ciun 4455   class class class wbr 4583  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041  Fun wfun 5798  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  0_gc0g 15923  Moorecmre 16065  mrClscmrc 16066  ACScacs 16068  Grpcgrp 17245  SubGrpcsubg 17411  Cntzccntz 17571  LSSumclsm 17872   DProd cdprd 18215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-submnd 17159  df-grp 17248  df-minusg 17249  df-sbg 17250  df-mulg 17364  df-subg 17414  df-ghm 17481  df-gim 17524  df-cntz 17573  df-oppg 17599  df-lsm 17874  df-cmn 18018  df-dprd 18217

This theorem is referenced by:  dmdprdsplit2  18268