Step |
Hyp |
Ref |
Expression |
1 |
|
dpjfval.1 |
⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 ) |
2 |
|
dpjfval.2 |
⊢ ( 𝜑 → dom 𝑆 = 𝐼 ) |
3 |
|
dpjfval.p |
⊢ 𝑃 = ( 𝐺 dProj 𝑆 ) |
4 |
|
dpjlid.3 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐼 ) |
5 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
6 |
|
eqid |
⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 ) |
7 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
8 |
|
eqid |
⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 ) |
9 |
1 2
|
dprdf2 |
⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ) |
10 |
9 4
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
11 |
|
difssd |
⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑋 } ) ⊆ 𝐼 ) |
12 |
1 2 11
|
dprdres |
⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) ) |
13 |
12
|
simpld |
⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) |
14 |
|
dprdsubg |
⊢ ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
15 |
13 14
|
syl |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
16 |
1 2 4 7
|
dpjdisj |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) |
17 |
1 2 4 8
|
dpjcntz |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) |
18 |
|
eqid |
⊢ ( proj1 ‘ 𝐺 ) = ( proj1 ‘ 𝐺 ) |
19 |
5 6 7 8 10 15 16 17 18
|
pj1ghm |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∈ ( ( 𝐺 ↾s ( ( 𝑆 ‘ 𝑋 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) GrpHom 𝐺 ) ) |
20 |
1 2 3 18 4
|
dpjval |
⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) |
21 |
1 2 4 6
|
dpjlsm |
⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( 𝑆 ‘ 𝑋 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) |
22 |
21
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) = ( 𝐺 ↾s ( ( 𝑆 ‘ 𝑋 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) ) |
23 |
22
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) = ( ( 𝐺 ↾s ( ( 𝑆 ‘ 𝑋 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) GrpHom 𝐺 ) ) |
24 |
19 20 23
|
3eltr4d |
⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) ) |