dpjlid

Description: The X -th index projection acts as the identity on elements of the X -th factor. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dpjfval.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
	dpjlid.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	dpjlid.4	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) )
Assertion	dpjlid	⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑋 ) ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2		dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3		dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4		dpjlid.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5		dpjlid.4	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) )
6		eqid	⊢ ( proj₁ ‘ 𝐺 ) = ( proj₁ ‘ 𝐺 )
7	1 2 3 6 4	dpjval	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) ( proj₁ ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
8	7	fveq1d	⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑋 ) ‘ 𝐴 ) = ( ( ( 𝑆 ‘ 𝑋 ) ( proj₁ ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ‘ 𝐴 ) )
9		eqid	⊢ ( +_g ‘ 𝐺 ) = ( +_g ‘ 𝐺 )
10		eqid	⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
11		eqid	⊢ ( 0_g ‘ 𝐺 ) = ( 0_g ‘ 𝐺 )
12		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
13	1 2	dprdf2	⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
14	13 4	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) )
15		difssd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑋 } ) ⊆ 𝐼 )
16	1 2 15	dprdres	⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
17	16	simpld	⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) )
18		dprdsubg	⊢ ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
19	17 18	syl	⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
20	1 2 4 11	dpjdisj	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { ( 0_g ‘ 𝐺 ) } )
21	1 2 4 12	dpjcntz	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
22	9 10 11 12 14 19 20 21 6	pj1lid	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) ) → ( ( ( 𝑆 ‘ 𝑋 ) ( proj₁ ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ‘ 𝐴 ) = 𝐴 )
23	5 22	mpdan	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ( proj₁ ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ‘ 𝐴 ) = 𝐴 )
24	8 23	eqtrd	⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑋 ) ‘ 𝐴 ) = 𝐴 )

Metamath Proof Explorer

Theorem dpjlid

Proof