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

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