lsmdisj - Metamath Proof Explorer

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

Theorem lsmdisj 19617

Description: Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)

**Hypotheses**
Ref	Expression
lsmcntz.p	⊢ ⊕ = (LSSum‘𝐺)
lsmcntz.s	⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))
lsmcntz.t	⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))
lsmcntz.u	⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))
lsmdisj.o	⊢ 0 = (0_g‘𝐺)
lsmdisj.i	⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 })

**Assertion**
Ref	Expression
lsmdisj	⊢ (𝜑 → ((𝑆 ∩ 𝑈) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 }))

**Proof of Theorem lsmdisj**
Step	Hyp	Ref	Expression
1		lsmcntz.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))
2		lsmcntz.t	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))
3		lsmcntz.p	. . . . . . 7 ⊢ ⊕ = (LSSum‘𝐺)
4	3	lsmub1 19593	. . . . . 6 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (𝑆 ⊕ 𝑇))
5	1, 2, 4	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ (𝑆 ⊕ 𝑇))
6	5	ssrind 4215	. . . 4 ⊢ (𝜑 → (𝑆 ∩ 𝑈) ⊆ ((𝑆 ⊕ 𝑇) ∩ 𝑈))
7		lsmdisj.i	. . . 4 ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 })
8	6, 7	sseqtrd 3991	. . 3 ⊢ (𝜑 → (𝑆 ∩ 𝑈) ⊆ { 0 })
9		lsmdisj.o	. . . . . . 7 ⊢ 0 = (0_g‘𝐺)
10	9	subg0cl 19072	. . . . . 6 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)
11	1, 10	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝑆)
12		lsmcntz.u	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))
13	9	subg0cl 19072	. . . . . 6 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑈)
14	12, 13	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝑈)
15	11, 14	elind 4171	. . . 4 ⊢ (𝜑 → 0 ∈ (𝑆 ∩ 𝑈))
16	15	snssd 4781	. . 3 ⊢ (𝜑 → { 0 } ⊆ (𝑆 ∩ 𝑈))
17	8, 16	eqssd 3972	. 2 ⊢ (𝜑 → (𝑆 ∩ 𝑈) = { 0 })
18	3	lsmub2 19594	. . . . . 6 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺)) → 𝑇 ⊆ (𝑆 ⊕ 𝑇))
19	1, 2, 18	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝑇 ⊆ (𝑆 ⊕ 𝑇))
20	19	ssrind 4215	. . . 4 ⊢ (𝜑 → (𝑇 ∩ 𝑈) ⊆ ((𝑆 ⊕ 𝑇) ∩ 𝑈))
21	20, 7	sseqtrd 3991	. . 3 ⊢ (𝜑 → (𝑇 ∩ 𝑈) ⊆ { 0 })
22	9	subg0cl 19072	. . . . . 6 ⊢ (𝑇 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑇)
23	2, 22	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝑇)
24	23, 14	elind 4171	. . . 4 ⊢ (𝜑 → 0 ∈ (𝑇 ∩ 𝑈))
25	24	snssd 4781	. . 3 ⊢ (𝜑 → { 0 } ⊆ (𝑇 ∩ 𝑈))
26	21, 25	eqssd 3972	. 2 ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })
27	17, 26	jca 511	1 ⊢ (𝜑 → ((𝑆 ∩ 𝑈) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 }))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∩ cin 3921 ⊆ wss 3922 {csn 4597 ‘cfv 6519 (class class class)co 7394 0_gc0g 17408 SubGrpcsubg 19058 LSSumclsm 19570

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5242 ax-sep 5259 ax-nul 5269 ax-pow 5328 ax-pr 5395 ax-un 7718 ax-cnex 11142 ax-resscn 11143 ax-1cn 11144 ax-icn 11145 ax-addcl 11146 ax-addrcl 11147 ax-mulcl 11148 ax-mulrcl 11149 ax-mulcom 11150 ax-addass 11151 ax-mulass 11152 ax-distr 11153 ax-i2m1 11154 ax-1ne0 11155 ax-1rid 11156 ax-rnegex 11157 ax-rrecex 11158 ax-cnre 11159 ax-pre-lttri 11160 ax-pre-lttrn 11161 ax-pre-ltadd 11162 ax-pre-mulgt0 11163

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2880 df-ne 2928 df-nel 3032 df-ral 3047 df-rex 3056 df-rmo 3357 df-reu 3358 df-rab 3412 df-v 3457 df-sbc 3762 df-csb 3871 df-dif 3925 df-un 3927 df-in 3929 df-ss 3939 df-pss 3942 df-nul 4305 df-if 4497 df-pw 4573 df-sn 4598 df-pr 4600 df-op 4604 df-uni 4880 df-iun 4965 df-br 5116 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5541 df-eprel 5546 df-po 5554 df-so 5555 df-fr 5599 df-we 5601 df-xp 5652 df-rel 5653 df-cnv 5654 df-co 5655 df-dm 5656 df-rn 5657 df-res 5658 df-ima 5659 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6472 df-fun 6521 df-fn 6522 df-f 6523 df-f1 6524 df-fo 6525 df-f1o 6526 df-fv 6527 df-riota 7351 df-ov 7397 df-oprab 7398 df-mpo 7399 df-om 7851 df-1st 7977 df-2nd 7978 df-frecs 8269 df-wrecs 8300 df-recs 8349 df-rdg 8387 df-er 8682 df-en 8923 df-dom 8924 df-sdom 8925 df-pnf 11228 df-mnf 11229 df-xr 11230 df-ltxr 11231 df-le 11232 df-sub 11425 df-neg 11426 df-nn 12198 df-2 12260 df-sets 17140 df-slot 17158 df-ndx 17170 df-base 17186 df-ress 17207 df-plusg 17239 df-0g 17410 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-submnd 18717 df-grp 18874 df-minusg 18875 df-subg 19061 df-lsm 19572

This theorem is referenced by: lsmdisjr 19620 lsmdisj2a 19623 lsmdisj2b 19624

W3C validator