Metamath Proof Explorer

Theorem lsmmod2

Description: Modular law dual for subgroup sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 8-Jan-2015) (Revised by Mario Carneiro, 21-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 lsmmod.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 simpl3 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
3 eqid ⊢ ( oppg ‘ 𝐺 ) = ( oppg ‘ 𝐺 )
4 3 oppgsubg ⊢ ( SubGrp ‘ 𝐺 ) = ( SubGrp ‘ ( oppg ‘ 𝐺 ) )
5 2 4 eleqtrdi ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ ( oppg ‘ 𝐺 ) ) )
6 simpl2 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
7 6 4 eleqtrdi ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → 𝑇 ∈ ( SubGrp ‘ ( oppg ‘ 𝐺 ) ) )
8 simpl1 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
9 8 4 eleqtrdi ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ ( oppg ‘ 𝐺 ) ) )
10 simpr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → 𝑈 ⊆ 𝑆 )
11 eqid ⊢ ( LSSum ‘ ( oppg ‘ 𝐺 ) ) = ( LSSum ‘ ( oppg ‘ 𝐺 ) )
12 11 lsmmod ⊢ ( ( ( 𝑈 ∈ ( SubGrp ‘ ( oppg ‘ 𝐺 ) ) ∧ 𝑇 ∈ ( SubGrp ‘ ( oppg ‘ 𝐺 ) ) ∧ 𝑆 ∈ ( SubGrp ‘ ( oppg ‘ 𝐺 ) ) ) ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) ( 𝑇 ∩ 𝑆 ) ) = ( ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) 𝑇 ) ∩ 𝑆 ) )
13 5 7 9 10 12 syl31anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) ( 𝑇 ∩ 𝑆 ) ) = ( ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) 𝑇 ) ∩ 𝑆 ) )
14 13 eqcomd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → ( ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) 𝑇 ) ∩ 𝑆 ) = ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) ( 𝑇 ∩ 𝑆 ) ) )
15 incom ⊢ ( ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) 𝑇 ) ∩ 𝑆 ) = ( 𝑆 ∩ ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) 𝑇 ) )
16 incom ⊢ ( 𝑇 ∩ 𝑆 ) = ( 𝑆 ∩ 𝑇 )
17 16 oveq2i ⊢ ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) ( 𝑇 ∩ 𝑆 ) ) = ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) ( 𝑆 ∩ 𝑇 ) )
18 14 15 17 3eqtr3g ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑆 ∩ ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) 𝑇 ) ) = ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) ( 𝑆 ∩ 𝑇 ) ) )
19 3 1 oppglsm ⊢ ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) 𝑇 ) = ( 𝑇 ⊕ 𝑈 )
20 19 ineq2i ⊢ ( 𝑆 ∩ ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) 𝑇 ) ) = ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) )
21 3 1 oppglsm ⊢ ( 𝑈 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) ( 𝑆 ∩ 𝑇 ) ) = ( ( 𝑆 ∩ 𝑇 ) ⊕ 𝑈 )
22 18 20 21 3eqtr3g ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = ( ( 𝑆 ∩ 𝑇 ) ⊕ 𝑈 ) )