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

Metamath Proof Explorer

Theorem lsmmod

Description: The modular law holds for subgroup sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmmod.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmmod ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) = ( ( 𝑆 ⊕ 𝑇 ) ∩ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lsmmod.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 simpl1 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
3 simpl2 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4 inss1 ⊢ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑇
5 4 a1i ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑇 ∩ 𝑈 ) ⊆ 𝑇 )
6 1 lsmless2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑇 ) → ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ⊆ ( 𝑆 ⊕ 𝑇 ) )
7 2 3 5 6 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ⊆ ( 𝑆 ⊕ 𝑇 ) )
8 simpr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → 𝑆 ⊆ 𝑈 )
9 inss2 ⊢ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈
10 9 a1i ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 )
11 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
12 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
13 12 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
14 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
15 2 11 13 14 4syl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
16 simpl3 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
17 mreincl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )
18 15 3 16 17 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )
19 1 lsmlub ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 ⊆ 𝑈 ∧ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 ) ↔ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ⊆ 𝑈 ) )
20 2 18 16 19 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( ( 𝑆 ⊆ 𝑈 ∧ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 ) ↔ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ⊆ 𝑈 ) )
21 8 10 20 mpbi2and ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ⊆ 𝑈 )
22 7 21 ssind ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ⊆ ( ( 𝑆 ⊕ 𝑇 ) ∩ 𝑈 ) )
23 elin ⊢ ( 𝑥 ∈ ( ( 𝑆 ⊕ 𝑇 ) ∩ 𝑈 ) ↔ ( 𝑥 ∈ ( 𝑆 ⊕ 𝑇 ) ∧ 𝑥 ∈ 𝑈 ) )
24 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
25 24 1 lsmelval ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑆 ⊕ 𝑇 ) ↔ ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑇 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
26 2 3 25 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑥 ∈ ( 𝑆 ⊕ 𝑇 ) ↔ ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑇 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
27 2 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
28 18 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )
29 simprll ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑦 ∈ 𝑆 )
30 simprlr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑧 ∈ 𝑇 )
31 27 11 syl ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝐺 ∈ Grp )
32 16 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
33 12 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
34 32 33 syl ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
35 8 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑆 ⊆ 𝑈 )
36 35 29 sseldd ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
37 34 36 sseldd ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
38 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
39 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
40 12 24 38 39 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) )
41 31 37 40 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) )
42 41 oveq1d ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑧 ) )
43 39 subginvcl ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦 ∈ 𝑈 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑈 )
44 32 36 43 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑈 )
45 34 44 sseldd ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
46 simpll2 ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
47 12 subgss ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
48 46 47 syl ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
49 48 30 sseldd ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
50 12 24 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
51 31 45 37 49 50 syl13anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
52 12 24 38 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑧 ) = 𝑧 )
53 31 49 52 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑧 ) = 𝑧 )
54 42 51 53 3eqtr3d ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = 𝑧 )
55 simprr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 )
56 24 subgcl ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑈 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑈 )
57 32 44 55 56 syl3anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑈 )
58 54 57 eqeltrrd ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑧 ∈ 𝑈 )
59 30 58 elind ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → 𝑧 ∈ ( 𝑇 ∩ 𝑈 ) )
60 24 1 lsmelvali ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( 𝑇 ∩ 𝑈 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) )
61 27 28 29 59 60 syl22anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) )
62 61 expr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) )
63 eleq1 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( 𝑥 ∈ 𝑈 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 ) )
64 eleq1 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( 𝑥 ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) )
65 63 64 imbi12d ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) ↔ ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑈 → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) ) )
66 62 65 syl5ibrcom ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) ) )
67 66 rexlimdvva ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑇 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) ) )
68 26 67 sylbid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑥 ∈ ( 𝑆 ⊕ 𝑇 ) → ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) ) )
69 68 impd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( ( 𝑥 ∈ ( 𝑆 ⊕ 𝑇 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) )
70 23 69 biimtrid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑥 ∈ ( ( 𝑆 ⊕ 𝑇 ) ∩ 𝑈 ) → 𝑥 ∈ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) ) )
71 70 ssrdv ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( ( 𝑆 ⊕ 𝑇 ) ∩ 𝑈 ) ⊆ ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) )
72 22 71 eqssd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑈 ) → ( 𝑆 ⊕ ( 𝑇 ∩ 𝑈 ) ) = ( ( 𝑆 ⊕ 𝑇 ) ∩ 𝑈 ) )