This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psd1

Description: The derivative of one is zero. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses psd1.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psd1.u ⊢ 1 = ( 1r ‘ 𝑆 )
psd1.z ⊢ 0 = ( 0g ‘ 𝑆 )
psd1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psd1.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
psd1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion psd1 ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) = 0 )

Proof

Step Hyp Ref Expression
1 psd1.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psd1.u ⊢ 1 = ( 1r ‘ 𝑆 )
3 psd1.z ⊢ 0 = ( 0g ‘ 𝑆 )
4 psd1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 psd1.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 psd1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
7 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
9 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
10 1 4 5 psrcrng ⊢ ( 𝜑 → 𝑆 ∈ CRing )
11 10 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
12 7 2 ringidcl ⊢ ( 𝑆 ∈ Ring → 1 ∈ ( Base ‘ 𝑆 ) )
13 11 12 syl ⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑆 ) )
14 1 7 8 9 5 6 13 13 psdmul ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 1 ( .r ‘ 𝑆 ) 1 ) ) = ( ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ( .r ‘ 𝑆 ) 1 ) ( +g ‘ 𝑆 ) ( 1 ( .r ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) ) )
15 7 9 2 11 13 ringlidmd ⊢ ( 𝜑 → ( 1 ( .r ‘ 𝑆 ) 1 ) = 1 )
16 15 fveq2d ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 1 ( .r ‘ 𝑆 ) 1 ) ) = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) )
17 5 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
18 17 grpmgmd ⊢ ( 𝜑 → 𝑅 ∈ Mgm )
19 1 7 18 6 13 psdcl ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ∈ ( Base ‘ 𝑆 ) )
20 7 9 2 11 19 ringridmd ⊢ ( 𝜑 → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ( .r ‘ 𝑆 ) 1 ) = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) )
21 7 9 2 11 19 ringlidmd ⊢ ( 𝜑 → ( 1 ( .r ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) )
22 20 21 oveq12d ⊢ ( 𝜑 → ( ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ( .r ‘ 𝑆 ) 1 ) ( +g ‘ 𝑆 ) ( 1 ( .r ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) ) = ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ( +g ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) )
23 14 16 22 3eqtr3rd ⊢ ( 𝜑 → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ( +g ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) )
24 10 crnggrpd ⊢ ( 𝜑 → 𝑆 ∈ Grp )
25 7 8 3 grpid ⊢ ( ( 𝑆 ∈ Grp ∧ ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ( +g ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ↔ 0 = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) )
26 24 19 25 syl2anc ⊢ ( 𝜑 → ( ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ( +g ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ↔ 0 = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) ) )
27 23 26 mpbid ⊢ ( 𝜑 → 0 = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) )
28 27 eqcomd ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 1 ) = 0 )