Step |
Hyp |
Ref |
Expression |
1 |
|
dpjfval.1 |
⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 ) |
2 |
|
dpjfval.2 |
⊢ ( 𝜑 → dom 𝑆 = 𝐼 ) |
3 |
|
dpjlem.3 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐼 ) |
4 |
|
dpjcntz.z |
⊢ 𝑍 = ( Cntz ‘ 𝐺 ) |
5 |
1 2 3
|
dpjlem |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) = ( 𝑆 ‘ 𝑋 ) ) |
6 |
1 2
|
dprdf2 |
⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ) |
7 |
|
disjdif |
⊢ ( { 𝑋 } ∩ ( 𝐼 ∖ { 𝑋 } ) ) = ∅ |
8 |
7
|
a1i |
⊢ ( 𝜑 → ( { 𝑋 } ∩ ( 𝐼 ∖ { 𝑋 } ) ) = ∅ ) |
9 |
|
undif2 |
⊢ ( { 𝑋 } ∪ ( 𝐼 ∖ { 𝑋 } ) ) = ( { 𝑋 } ∪ 𝐼 ) |
10 |
3
|
snssd |
⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 ) |
11 |
|
ssequn1 |
⊢ ( { 𝑋 } ⊆ 𝐼 ↔ ( { 𝑋 } ∪ 𝐼 ) = 𝐼 ) |
12 |
10 11
|
sylib |
⊢ ( 𝜑 → ( { 𝑋 } ∪ 𝐼 ) = 𝐼 ) |
13 |
9 12
|
eqtr2id |
⊢ ( 𝜑 → 𝐼 = ( { 𝑋 } ∪ ( 𝐼 ∖ { 𝑋 } ) ) ) |
14 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
15 |
6 8 13 4 14
|
dmdprdsplit |
⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( ( 𝐺 dom DProd ( 𝑆 ↾ { 𝑋 } ) ∧ 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) |
16 |
1 15
|
mpbid |
⊢ ( 𝜑 → ( ( 𝐺 dom DProd ( 𝑆 ↾ { 𝑋 } ) ∧ 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) |
17 |
16
|
simp2d |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) |
18 |
5 17
|
eqsstrrd |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) |