This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } )