dprdsplit - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dprdsplit		Structured version Visualization version GIF version

Theorem dprdsplit 20269

Description: The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016.)

**Hypotheses**
Ref	Expression
dprdsplit.2	⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))
dprdsplit.i	⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)
dprdsplit.u	⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷))
dprdsplit.s	⊢ ⊕ = (LSSum‘𝐺)
dprdsplit.1	⊢ (𝜑 → 𝐺dom DProd 𝑆)

**Assertion**
Ref	Expression
dprdsplit	⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))

Proof of Theorem dprdsplit Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dprdsplit.1	. . 3 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
2		dprdsplit.2	. . . 4 ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))
3	2	fdmd 6720	. . 3 ⊢ (𝜑 → dom 𝑆 = 𝐼)
4		ssun1 4176	. . . . . . . 8 ⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷)
5		dprdsplit.u	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷))
6	4, 5	sseqtrrid 3951	. . . . . . 7 ⊢ (𝜑 → 𝐶 ⊆ 𝐼)
7	1, 3, 6	dprdres 20249	. . . . . 6 ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐶) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆)))
8	7	simpld 500	. . . . 5 ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶))
9		dprdsubg 20245	. . . . 5 ⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺))
10	8, 9	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺))
11		ssun2 4177	. . . . . . . 8 ⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷)
12	11, 5	sseqtrrid 3951	. . . . . . 7 ⊢ (𝜑 → 𝐷 ⊆ 𝐼)
13	1, 3, 12	dprdres 20249	. . . . . 6 ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐷) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆)))
14	13	simpld 500	. . . . 5 ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷))
15		dprdsubg 20245	. . . . 5 ⊢ (𝐺dom DProd (𝑆 ↾ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
16	14, 15	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
17		dprdsplit.i	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)
18		eqid 2760	. . . . . . 7 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
19		eqid 2760	. . . . . . 7 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
20	2, 17, 5, 18, 19	dmdprdsplit 20268	. . . . . 6 ⊢ (𝜑 → (𝐺dom DProd 𝑆 ↔ ((𝐺dom DProd (𝑆 ↾ 𝐶) ∧ 𝐺dom DProd (𝑆 ↾ 𝐷)) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ 𝐷))) ∧ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = {(0_g‘𝐺)})))
21	1, 20	mpbid 235	. . . . 5 ⊢ (𝜑 → ((𝐺dom DProd (𝑆 ↾ 𝐶) ∧ 𝐺dom DProd (𝑆 ↾ 𝐷)) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ 𝐷))) ∧ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = {(0_g‘𝐺)}))
22	21	simp2d 1161	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ 𝐷))))
23		dprdsplit.s	. . . . 5 ⊢ ⊕ = (LSSum‘𝐺)
24	23, 18	lsmsubg 19873	. . . 4 ⊢ (((𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ 𝐷)))) → ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺))
25	10, 16, 22, 24	syl3anc 1398	. . 3 ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺))
26	5	eleq2d 2846	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↔ 𝑥 ∈ (𝐶 ∪ 𝐷)))
27		elun 4152	. . . . . 6 ⊢ (𝑥 ∈ (𝐶 ∪ 𝐷) ↔ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷))
28	26, 27	bitrdi 290	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↔ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)))
29	28	biimpa 482	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷))
30		fvres 6904	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐶 → ((𝑆 ↾ 𝐶)‘𝑥) = (𝑆‘𝑥))
31	30	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑥) = (𝑆‘𝑥))
32	8	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐺dom DProd (𝑆 ↾ 𝐶))
33	2, 6	fssresd 6749	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ↾ 𝐶):𝐶⟶(SubGrp‘𝐺))
34	33	fdmd 6720	. . . . . . . . 9 ⊢ (𝜑 → dom (𝑆 ↾ 𝐶) = 𝐶)
35	34	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → dom (𝑆 ↾ 𝐶) = 𝐶)
36		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶)
37	32, 35, 36	dprdub 20246	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑥) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))
38	31, 37	eqsstrrd 3943	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))
39	23	lsmub1 19876	. . . . . . . 8 ⊢ (((𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
40	10, 16, 39	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
41	40	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
42	38, 41	sstrd 3918	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘𝑥) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
43		fvres 6904	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ((𝑆 ↾ 𝐷)‘𝑥) = (𝑆‘𝑥))
44	43	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑆 ↾ 𝐷)‘𝑥) = (𝑆‘𝑥))
45	14	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐺dom DProd (𝑆 ↾ 𝐷))
46	2, 12	fssresd 6749	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺))
47	46	fdmd 6720	. . . . . . . . 9 ⊢ (𝜑 → dom (𝑆 ↾ 𝐷) = 𝐷)
48	47	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → dom (𝑆 ↾ 𝐷) = 𝐷)
49		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
50	45, 48, 49	dprdub 20246	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑆 ↾ 𝐷)‘𝑥) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷)))
51	44, 50	eqsstrrd 3943	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷)))
52	23	lsmub2 19877	. . . . . . . 8 ⊢ (((𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
53	10, 16, 52	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
54	53	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
55	51, 54	sstrd 3918	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑆‘𝑥) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
56	42, 55	jaodan 972	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) → (𝑆‘𝑥) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
57	29, 56	syldan 603	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
58	1, 3, 25, 57	dprdlub 20247	. 2 ⊢ (𝜑 → (𝐺 DProd 𝑆) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
59	7	simprd 501	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆))
60	13	simprd 501	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆))
61		dprdsubg 20245	. . . . 5 ⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺))
62	1, 61	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺))
63	23	lsmlub 19883	. . . 4 ⊢ (((𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) → (((𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆)) ↔ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝐺 DProd 𝑆)))
64	10, 16, 62, 63	syl3anc 1398	. . 3 ⊢ (𝜑 → (((𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆)) ↔ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝐺 DProd 𝑆)))
65	59, 60, 64	mpbi2and 725	. 2 ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝐺 DProd 𝑆))
66	58, 65	eqssd 3925	1 ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ⊆ wss 3895 ∩ cin 4089 ∪ cun 4149 ∅c0 4278 {csn 4584 class class class wbr 5102 dom cdm 5650 ↾ cres 5652 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 0_gc0g 17615 SubGrpcsubg 19335 Cntzccntz 19534 LSSumclsm 19853 DProd cdprd 20214

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8180 df-tpos 8246 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-er 8720 df-map 8852 df-ixp 8929 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-fsupp 9357 df-oi 9507 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-nn 12339 df-2 12408 df-n0 12610 df-z 12697 df-uz 12969 df-fz 13643 df-fzo 13792 df-seq 14148 df-hash 14478 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-ress 17414 df-plusg 17446 df-0g 17617 df-gsum 17618 df-mre 17761 df-mrc 17762 df-acs 17764 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-mhm 18983 df-submnd 18984 df-grp 19152 df-minusg 19153 df-sbg 19154 df-mulg 19283 df-subg 19338 df-ghm 19433 df-gim 19478 df-cntz 19536 df-oppg 19565 df-lsm 19855 df-cmn 20001 df-dprd 20216

This theorem is used by: dprdpr 20271 dpjlsm 20275 ablfac1eulem 20293 ablfac1eu 20294 pgpfaclem1 20302

W3C validator