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

Metamath Proof Explorer

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