Metamath Proof Explorer


Theorem lsmdisj2

Description: Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 lsmcntz.p = ( LSSum ‘ 𝐺 )
2 lsmcntz.s ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
3 lsmcntz.t ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4 lsmcntz.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
5 lsmdisj.o 0 = ( 0g𝐺 )
6 lsmdisj.i ( 𝜑 → ( ( 𝑆 𝑇 ) ∩ 𝑈 ) = { 0 } )
7 lsmdisj2.i ( 𝜑 → ( 𝑆𝑇 ) = { 0 } )
8 eqid ( +g𝐺 ) = ( +g𝐺 )
9 8 1 lsmelval ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑆 𝑈 ) ↔ ∃ 𝑠𝑆𝑢𝑈 𝑥 = ( 𝑠 ( +g𝐺 ) 𝑢 ) ) )
10 2 4 9 syl2anc ( 𝜑 → ( 𝑥 ∈ ( 𝑆 𝑈 ) ↔ ∃ 𝑠𝑆𝑢𝑈 𝑥 = ( 𝑠 ( +g𝐺 ) 𝑢 ) ) )
11 simplrl ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑠𝑆 )
12 subgrcl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
13 2 12 syl ( 𝜑𝐺 ∈ Grp )
14 13 ad2antrr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝐺 ∈ Grp )
15 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
16 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
17 16 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
18 15 17 syl ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
19 18 11 sseldd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑠 ∈ ( Base ‘ 𝐺 ) )
20 eqid ( invg𝐺 ) = ( invg𝐺 )
21 16 8 5 20 grplinv ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) 𝑠 ) = 0 )
22 14 19 21 syl2anc ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) 𝑠 ) = 0 )
23 22 oveq1d ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) 𝑠 ) ( +g𝐺 ) 𝑢 ) = ( 0 ( +g𝐺 ) 𝑢 ) )
24 20 subginvcl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑠𝑆 ) → ( ( invg𝐺 ) ‘ 𝑠 ) ∈ 𝑆 )
25 15 11 24 syl2anc ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( ( invg𝐺 ) ‘ 𝑠 ) ∈ 𝑆 )
26 18 25 sseldd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( ( invg𝐺 ) ‘ 𝑠 ) ∈ ( Base ‘ 𝐺 ) )
27 4 ad2antrr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
28 16 subgss ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
29 27 28 syl ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
30 simplrr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑢𝑈 )
31 29 30 sseldd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑢 ∈ ( Base ‘ 𝐺 ) )
32 16 8 grpass ( ( 𝐺 ∈ Grp ∧ ( ( ( invg𝐺 ) ‘ 𝑠 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) 𝑠 ) ( +g𝐺 ) 𝑢 ) = ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) ( 𝑠 ( +g𝐺 ) 𝑢 ) ) )
33 14 26 19 31 32 syl13anc ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) 𝑠 ) ( +g𝐺 ) 𝑢 ) = ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) ( 𝑠 ( +g𝐺 ) 𝑢 ) ) )
34 16 8 5 grplid ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( 0 ( +g𝐺 ) 𝑢 ) = 𝑢 )
35 14 31 34 syl2anc ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 0 ( +g𝐺 ) 𝑢 ) = 𝑢 )
36 23 33 35 3eqtr3d ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) ( 𝑠 ( +g𝐺 ) 𝑢 ) ) = 𝑢 )
37 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
38 simpr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 )
39 8 1 lsmelvali ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( invg𝐺 ) ‘ 𝑠 ) ∈ 𝑆 ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) ) → ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) ( 𝑠 ( +g𝐺 ) 𝑢 ) ) ∈ ( 𝑆 𝑇 ) )
40 15 37 25 38 39 syl22anc ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( ( ( invg𝐺 ) ‘ 𝑠 ) ( +g𝐺 ) ( 𝑠 ( +g𝐺 ) 𝑢 ) ) ∈ ( 𝑆 𝑇 ) )
41 36 40 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑢 ∈ ( 𝑆 𝑇 ) )
42 41 30 elind ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑢 ∈ ( ( 𝑆 𝑇 ) ∩ 𝑈 ) )
43 6 ad2antrr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( ( 𝑆 𝑇 ) ∩ 𝑈 ) = { 0 } )
44 42 43 eleqtrd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑢 ∈ { 0 } )
45 elsni ( 𝑢 ∈ { 0 } → 𝑢 = 0 )
46 44 45 syl ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑢 = 0 )
47 46 oveq2d ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 𝑠 ( +g𝐺 ) 𝑢 ) = ( 𝑠 ( +g𝐺 ) 0 ) )
48 16 8 5 grprid ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑠 ( +g𝐺 ) 0 ) = 𝑠 )
49 14 19 48 syl2anc ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 𝑠 ( +g𝐺 ) 0 ) = 𝑠 )
50 47 49 eqtrd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 𝑠 ( +g𝐺 ) 𝑢 ) = 𝑠 )
51 50 38 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑠𝑇 )
52 11 51 elind ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑠 ∈ ( 𝑆𝑇 ) )
53 7 ad2antrr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 𝑆𝑇 ) = { 0 } )
54 52 53 eleqtrd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑠 ∈ { 0 } )
55 elsni ( 𝑠 ∈ { 0 } → 𝑠 = 0 )
56 54 55 syl ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → 𝑠 = 0 )
57 56 46 oveq12d ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 𝑠 ( +g𝐺 ) 𝑢 ) = ( 0 ( +g𝐺 ) 0 ) )
58 16 5 grpidcl ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
59 16 8 5 grplid ( ( 𝐺 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( 0 ( +g𝐺 ) 0 ) = 0 )
60 13 58 59 syl2anc2 ( 𝜑 → ( 0 ( +g𝐺 ) 0 ) = 0 )
61 60 ad2antrr ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 0 ( +g𝐺 ) 0 ) = 0 )
62 57 61 eqtrd ( ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) ∧ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) → ( 𝑠 ( +g𝐺 ) 𝑢 ) = 0 )
63 62 ex ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) → ( ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 → ( 𝑠 ( +g𝐺 ) 𝑢 ) = 0 ) )
64 eleq1 ( 𝑥 = ( 𝑠 ( +g𝐺 ) 𝑢 ) → ( 𝑥𝑇 ↔ ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 ) )
65 eqeq1 ( 𝑥 = ( 𝑠 ( +g𝐺 ) 𝑢 ) → ( 𝑥 = 0 ↔ ( 𝑠 ( +g𝐺 ) 𝑢 ) = 0 ) )
66 64 65 imbi12d ( 𝑥 = ( 𝑠 ( +g𝐺 ) 𝑢 ) → ( ( 𝑥𝑇𝑥 = 0 ) ↔ ( ( 𝑠 ( +g𝐺 ) 𝑢 ) ∈ 𝑇 → ( 𝑠 ( +g𝐺 ) 𝑢 ) = 0 ) ) )
67 63 66 syl5ibrcom ( ( 𝜑 ∧ ( 𝑠𝑆𝑢𝑈 ) ) → ( 𝑥 = ( 𝑠 ( +g𝐺 ) 𝑢 ) → ( 𝑥𝑇𝑥 = 0 ) ) )
68 67 rexlimdvva ( 𝜑 → ( ∃ 𝑠𝑆𝑢𝑈 𝑥 = ( 𝑠 ( +g𝐺 ) 𝑢 ) → ( 𝑥𝑇𝑥 = 0 ) ) )
69 10 68 sylbid ( 𝜑 → ( 𝑥 ∈ ( 𝑆 𝑈 ) → ( 𝑥𝑇𝑥 = 0 ) ) )
70 69 impcomd ( 𝜑 → ( ( 𝑥𝑇𝑥 ∈ ( 𝑆 𝑈 ) ) → 𝑥 = 0 ) )
71 elin ( 𝑥 ∈ ( 𝑇 ∩ ( 𝑆 𝑈 ) ) ↔ ( 𝑥𝑇𝑥 ∈ ( 𝑆 𝑈 ) ) )
72 velsn ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
73 70 71 72 3imtr4g ( 𝜑 → ( 𝑥 ∈ ( 𝑇 ∩ ( 𝑆 𝑈 ) ) → 𝑥 ∈ { 0 } ) )
74 73 ssrdv ( 𝜑 → ( 𝑇 ∩ ( 𝑆 𝑈 ) ) ⊆ { 0 } )
75 5 subg0cl ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 0𝑇 )
76 3 75 syl ( 𝜑0𝑇 )
77 1 lsmub1 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( 𝑆 𝑈 ) )
78 2 4 77 syl2anc ( 𝜑𝑆 ⊆ ( 𝑆 𝑈 ) )
79 5 subg0cl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0𝑆 )
80 2 79 syl ( 𝜑0𝑆 )
81 78 80 sseldd ( 𝜑0 ∈ ( 𝑆 𝑈 ) )
82 76 81 elind ( 𝜑0 ∈ ( 𝑇 ∩ ( 𝑆 𝑈 ) ) )
83 82 snssd ( 𝜑 → { 0 } ⊆ ( 𝑇 ∩ ( 𝑆 𝑈 ) ) )
84 74 83 eqssd ( 𝜑 → ( 𝑇 ∩ ( 𝑆 𝑈 ) ) = { 0 } )