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 ( 𝜑𝐺 dom DProd 𝑆 )
dpjfval.2 ( 𝜑 → dom 𝑆 = 𝐼 )
dpjlem.3 ( 𝜑𝑋𝐼 )
dpjlsm.s = ( LSSum ‘ 𝐺 )
Assertion dpjlsm ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( 𝑆𝑋 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 ( 𝜑𝐺 dom DProd 𝑆 )
2 dpjfval.2 ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjlem.3 ( 𝜑𝑋𝐼 )
4 dpjlsm.s = ( LSSum ‘ 𝐺 )
5 1 2 dprdf2 ( 𝜑𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
6 disjdif ( { 𝑋 } ∩ ( 𝐼 ∖ { 𝑋 } ) ) = ∅
7 6 a1i ( 𝜑 → ( { 𝑋 } ∩ ( 𝐼 ∖ { 𝑋 } ) ) = ∅ )
8 undif2 ( { 𝑋 } ∪ ( 𝐼 ∖ { 𝑋 } ) ) = ( { 𝑋 } ∪ 𝐼 )
9 3 snssd ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
10 ssequn1 ( { 𝑋 } ⊆ 𝐼 ↔ ( { 𝑋 } ∪ 𝐼 ) = 𝐼 )
11 9 10 sylib ( 𝜑 → ( { 𝑋 } ∪ 𝐼 ) = 𝐼 )
12 8 11 eqtr2id ( 𝜑𝐼 = ( { 𝑋 } ∪ ( 𝐼 ∖ { 𝑋 } ) ) )
13 5 7 12 4 1 dprdsplit ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
14 1 2 3 dpjlem ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) = ( 𝑆𝑋 ) )
15 14 oveq1d ( 𝜑 → ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = ( ( 𝑆𝑋 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
16 13 15 eqtrd ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( 𝑆𝑋 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )