Metamath Proof Explorer

Theorem dprddisj

Description: The function S is a family having trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdcntz.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdcntz.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdcntz.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
dprddisj.0 ⊢ 0 = ( 0g ‘ 𝐺 )
dprddisj.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion dprddisj ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 dprdcntz.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dprdcntz.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dprdcntz.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
4 dprddisj.0 ⊢ 0 = ( 0g ‘ 𝐺 )
5 dprddisj.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
6 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑋 ) )
7 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
8 7 difeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐼 ∖ { 𝑥 } ) = ( 𝐼 ∖ { 𝑋 } ) )
9 8 imaeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝑆 “ ( 𝐼 ∖ { 𝑋 } ) ) )
10 9 unieqd ⊢ ( 𝑥 = 𝑋 → ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) = ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑋 } ) ) )
11 10 fveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑋 } ) ) ) )
12 6 11 ineq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
13 12 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ↔ ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { 0 } ) )
14 1 2 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
15 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
16 15 4 5 dmdprd ⊢ ( ( 𝐼 ∈ V ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
17 14 2 16 syl2anc ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
18 1 17 mpbid ⊢ ( 𝜑 → ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) )
19 18 simp3d ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) )
20 simpr ⊢ ( ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } )
21 20 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } )
22 19 21 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } )
23 13 22 3 rspcdva ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { 0 } )