Metamath Proof Explorer

Theorem lsmdisj2b

Description: Association of the disjointness constraint in 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 ‘ 𝐺 )
Assertion lsmdisj2b ( 𝜑 → ( ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ↔ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 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 incom ⊢ ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = ( ( 𝑇 ⊕ 𝑈 ) ∩ 𝑆 )
7 3 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
8 2 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
9 4 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
10 incom ⊢ ( 𝑇 ∩ ( 𝑆 ⊕ 𝑈 ) ) = ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 )
11 simprl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } )
12 10 11 syl5eq ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( 𝑇 ∩ ( 𝑆 ⊕ 𝑈 ) ) = { 0 } )
13 simprr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( 𝑆 ∩ 𝑈 ) = { 0 } )
14 1 7 8 9 5 12 13 lsmdisj2r ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( ( 𝑇 ⊕ 𝑈 ) ∩ 𝑆 ) = { 0 } )
15 6 14 syl5eq ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } )
16 incom ⊢ ( 𝑇 ∩ 𝑈 ) = ( 𝑈 ∩ 𝑇 )
17 1 8 9 7 5 11 lsmdisj ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( ( 𝑆 ∩ 𝑇 ) = { 0 } ∧ ( 𝑈 ∩ 𝑇 ) = { 0 } ) )
18 17 simprd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( 𝑈 ∩ 𝑇 ) = { 0 } )
19 16 18 syl5eq ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( 𝑇 ∩ 𝑈 ) = { 0 } )
20 15 19 jca ⊢ ( ( 𝜑 ∧ ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ) → ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) )
21 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
22 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
23 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
24 simprl ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } )
25 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → ( 𝑇 ∩ 𝑈 ) = { 0 } )
26 1 21 22 23 5 24 25 lsmdisj2r ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } )
27 1 21 22 23 5 24 lsmdisjr ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → ( ( 𝑆 ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) )
28 27 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → ( 𝑆 ∩ 𝑈 ) = { 0 } )
29 26 28 jca ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) → ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) )
30 20 29 impbida ⊢ ( 𝜑 → ( ( ( ( 𝑆 ⊕ 𝑈 ) ∩ 𝑇 ) = { 0 } ∧ ( 𝑆 ∩ 𝑈 ) = { 0 } ) ↔ ( ( 𝑆 ∩ ( 𝑇 ⊕ 𝑈 ) ) = { 0 } ∧ ( 𝑇 ∩ 𝑈 ) = { 0 } ) ) )