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 ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) |