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 ⊢ φ → G dom ⁡ DProd S
dpjfval.2 ⊢ φ → dom ⁡ S = I
dpjlem.3 ⊢ φ → X ∈ I
dpjlsm.s ⊢ ⊕ ˙ = LSSum ⁡ G
Assertion dpjlsm ⊢ φ → G DProd S = S ⁡ X ⊕ ˙ G DProd S ↾ I ∖ X

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ φ → G dom ⁡ DProd S
2 dpjfval.2 ⊢ φ → dom ⁡ S = I
3 dpjlem.3 ⊢ φ → X ∈ I
4 dpjlsm.s ⊢ ⊕ ˙ = LSSum ⁡ G
5 1 2 dprdf2 ⊢ φ → S : I ⟶ SubGrp ⁡ G
6 disjdif ⊢ X ∩ I ∖ X = ∅
7 6 a1i ⊢ φ → X ∩ I ∖ X = ∅
8 undif2 ⊢ X ∪ I ∖ X = X ∪ I
9 3 snssd ⊢ φ → X ⊆ I
10 ssequn1 ⊢ X ⊆ I ↔ X ∪ I = I
11 9 10 sylib ⊢ φ → X ∪ I = I
12 8 11 eqtr2id ⊢ φ → I = X ∪ I ∖ X
13 5 7 12 4 1 dprdsplit ⊢ φ → G DProd S = G DProd S ↾ X ⊕ ˙ G DProd S ↾ I ∖ X
14 1 2 3 dpjlem ⊢ φ → G DProd S ↾ X = S ⁡ X
15 14 oveq1d ⊢ φ → G DProd S ↾ X ⊕ ˙ G DProd S ↾ I ∖ X = S ⁡ X ⊕ ˙ G DProd S ↾ I ∖ X
16 13 15 eqtrd ⊢ φ → G DProd S = S ⁡ X ⊕ ˙ G DProd S ↾ I ∖ X