Theorem dpjlsm

Description: The two subgroups that appear in dpjval add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dpjfval.1	|- ( ph -> G dom DProd S )
	dpjfval.2	|- ( ph -> dom S = I )
	dpjlem.3	|- ( ph -> X e. I )
	dpjlsm.s	|- .(+) = ( LSSum ` G )
Assertion	dpjlsm	|- ( ph -> ( G DProd S ) = ( ( S ` X ) .(+) ( G DProd ( S |` ( I \ { X } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	|- ( ph -> G dom DProd S )
2		dpjfval.2	|- ( ph -> dom S = I )
3		dpjlem.3	|- ( ph -> X e. I )
4		dpjlsm.s	|- .(+) = ( LSSum ` G )
5	1 2	dprdf2	|- ( ph -> S : I --> ( SubGrp ` G ) )
6		disjdif	|- ( { X } i^i ( I \ { X } ) ) = (/)
7	6	a1i	|- ( ph -> ( { X } i^i ( I \ { X } ) ) = (/) )
8		undif2	|- ( { X } u. ( I \ { X } ) ) = ( { X } u. I )
9	3	snssd	|- ( ph -> { X } C_ I )
10		ssequn1	|- ( { X } C_ I <-> ( { X } u. I ) = I )
11	9 10	sylib	|- ( ph -> ( { X } u. I ) = I )
12	8 11	eqtr2id	|- ( ph -> I = ( { X } u. ( I \ { X } ) ) )
13	5 7 12 4 1	dprdsplit	|- ( ph -> ( G DProd S ) = ( ( G DProd ( S |` { X } ) ) .(+) ( G DProd ( S |` ( I \ { X } ) ) ) ) )
14	1 2 3	dpjlem	|- ( ph -> ( G DProd ( S |` { X } ) ) = ( S ` X ) )
15	14	oveq1d	|- ( ph -> ( ( G DProd ( S |` { X } ) ) .(+) ( G DProd ( S |` ( I \ { X } ) ) ) ) = ( ( S ` X ) .(+) ( G DProd ( S |` ( I \ { X } ) ) ) ) )
16	13 15	eqtrd	|- ( ph -> ( G DProd S ) = ( ( S ` X ) .(+) ( G DProd ( S |` ( I \ { X } ) ) ) ) )