Metamath Proof Explorer


Theorem lsmdisjr

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

Ref Expression
Hypotheses lsmcntz.p = ( LSSum ‘ 𝐺 )
lsmcntz.s ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
lsmcntz.t ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
lsmcntz.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
lsmdisj.o 0 = ( 0g𝐺 )
lsmdisjr.i ( 𝜑 → ( 𝑆 ∩ ( 𝑇 𝑈 ) ) = { 0 } )
Assertion lsmdisjr ( 𝜑 → ( ( 𝑆𝑇 ) = { 0 } ∧ ( 𝑆𝑈 ) = { 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 lsmdisjr.i ( 𝜑 → ( 𝑆 ∩ ( 𝑇 𝑈 ) ) = { 0 } )
7 incom ( 𝑆 ∩ ( 𝑇 𝑈 ) ) = ( ( 𝑇 𝑈 ) ∩ 𝑆 )
8 7 6 eqtr3id ( 𝜑 → ( ( 𝑇 𝑈 ) ∩ 𝑆 ) = { 0 } )
9 1 3 4 2 5 8 lsmdisj ( 𝜑 → ( ( 𝑇𝑆 ) = { 0 } ∧ ( 𝑈𝑆 ) = { 0 } ) )
10 incom ( 𝑇𝑆 ) = ( 𝑆𝑇 )
11 10 eqeq1i ( ( 𝑇𝑆 ) = { 0 } ↔ ( 𝑆𝑇 ) = { 0 } )
12 incom ( 𝑈𝑆 ) = ( 𝑆𝑈 )
13 12 eqeq1i ( ( 𝑈𝑆 ) = { 0 } ↔ ( 𝑆𝑈 ) = { 0 } )
14 11 13 anbi12i ( ( ( 𝑇𝑆 ) = { 0 } ∧ ( 𝑈𝑆 ) = { 0 } ) ↔ ( ( 𝑆𝑇 ) = { 0 } ∧ ( 𝑆𝑈 ) = { 0 } ) )
15 9 14 sylib ( 𝜑 → ( ( 𝑆𝑇 ) = { 0 } ∧ ( 𝑆𝑈 ) = { 0 } ) )