Theorem dpjdisj

Description: The two subgroups that appear in dpjval are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dpjfval.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	dpjlem.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	dpjdisj.0	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	dpjdisj	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { 0 } )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2		dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3		dpjlem.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
4		dpjdisj.0	⊢ 0 = ( 0g ‘ 𝐺 )
5	1 2 3	dpjlem	⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) = ( 𝑆 ‘ 𝑋 ) )
6	5	ineq1d	⊢ ( 𝜑 → ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
7	1 2	dprdf2	⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
8		disjdif	⊢ ( { 𝑋 } ∩ ( 𝐼 ∖ { 𝑋 } ) ) = ∅
9	8	a1i	⊢ ( 𝜑 → ( { 𝑋 } ∩ ( 𝐼 ∖ { 𝑋 } ) ) = ∅ )
10		undif2	⊢ ( { 𝑋 } ∪ ( 𝐼 ∖ { 𝑋 } ) ) = ( { 𝑋 } ∪ 𝐼 )
11	3	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
12		ssequn1	⊢ ( { 𝑋 } ⊆ 𝐼 ↔ ( { 𝑋 } ∪ 𝐼 ) = 𝐼 )
13	11 12	sylib	⊢ ( 𝜑 → ( { 𝑋 } ∪ 𝐼 ) = 𝐼 )
14	10 13	syl5req	⊢ ( 𝜑 → 𝐼 = ( { 𝑋 } ∪ ( 𝐼 ∖ { 𝑋 } ) ) )
15		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
16	7 9 14 15 4	dmdprdsplit	⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( ( 𝐺 dom DProd ( 𝑆 ↾ { 𝑋 } ) ∧ 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { 0 } ) ) )
17	1 16	mpbid	⊢ ( 𝜑 → ( ( 𝐺 dom DProd ( 𝑆 ↾ { 𝑋 } ) ∧ 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { 0 } ) )
18	17	simp3d	⊢ ( 𝜑 → ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { 0 } )
19	6 18	eqtr3d	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { 0 } )