Theorem psrridm

Description: The identity element of the ring of power series is a right identity. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof shortened by AV, 8-Jul-2019)

	Ref	Expression
Hypotheses	psrring.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrring.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	psrring.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	psr1cl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	psr1cl.z	⊢ 0 = ( 0g ‘ 𝑅 )
	psr1cl.o	⊢ 1 = ( 1r ‘ 𝑅 )
	psr1cl.u	⊢ 𝑈 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
	psr1cl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psrlidm.t	⊢ · = ( .r ‘ 𝑆 )
	psrlidm.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	psrridm	⊢ ( 𝜑 → ( 𝑋 · 𝑈 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		psrring.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrring.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		psrring.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		psr1cl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5		psr1cl.z	⊢ 0 = ( 0g ‘ 𝑅 )
6		psr1cl.o	⊢ 1 = ( 1r ‘ 𝑅 )
7		psr1cl.u	⊢ 𝑈 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
8		psr1cl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
9		psrlidm.t	⊢ · = ( .r ‘ 𝑆 )
10		psrlidm.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12	1 2 3 4 5 6 7 8	psr1cl	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
13	1 8 9 3 10 12	psrmulcl	⊢ ( 𝜑 → ( 𝑋 · 𝑈 ) ∈ 𝐵 )
14	1 11 4 8 13	psrelbas	⊢ ( 𝜑 → ( 𝑋 · 𝑈 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
15	14	ffnd	⊢ ( 𝜑 → ( 𝑋 · 𝑈 ) Fn 𝐷 )
16	1 11 4 8 10	psrelbas	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
17	16	ffnd	⊢ ( 𝜑 → 𝑋 Fn 𝐷 )
18		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
19	10	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑋 ∈ 𝐵 )
20	12	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑈 ∈ 𝐵 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
22	1 8 18 9 4 19 20 21	psrmulval	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 · 𝑈 ) ‘ 𝑦 ) = ( 𝑅 Σg ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) )
23		breq1	⊢ ( 𝑔 = 𝑦 → ( 𝑔 ∘r ≤ 𝑦 ↔ 𝑦 ∘r ≤ 𝑦 ) )
24	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
25	4	psrbagf	⊢ ( 𝑦 ∈ 𝐷 → 𝑦 : 𝐼 ⟶ ℕ0 )
26	25	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 : 𝐼 ⟶ ℕ0 )
27		nn0re	⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ∈ ℝ )
28	27	leidd	⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ≤ 𝑧 )
29	28	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ℕ0 ) → 𝑧 ≤ 𝑧 )
30	24 26 29	caofref	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∘r ≤ 𝑦 )
31	23 21 30	elrabd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } )
32	31	snssd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → { 𝑦 } ⊆ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } )
33	32	resmptd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ↾ { 𝑦 } ) = ( 𝑧 ∈ { 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) )
34	33	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ↾ { 𝑦 } ) ) = ( 𝑅 Σg ( 𝑧 ∈ { 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) )
35		ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
36	3 35	syl	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
38		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
39	4 38	rab2ex	⊢ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∈ V
40	39	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∈ V )
41	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑅 ∈ Ring )
42	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
43		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } )
44		breq1	⊢ ( 𝑔 = 𝑧 → ( 𝑔 ∘r ≤ 𝑦 ↔ 𝑧 ∘r ≤ 𝑦 ) )
45	44	elrab	⊢ ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↔ ( 𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦 ) )
46	43 45	sylib	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( 𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦 ) )
47	46	simpld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 ∈ 𝐷 )
48	42 47	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
49	1 11 4 8 20	psrelbas	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑈 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
50	49	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑈 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
51	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑦 ∈ 𝐷 )
52	4	psrbagf	⊢ ( 𝑧 ∈ 𝐷 → 𝑧 : 𝐼 ⟶ ℕ0 )
53	47 52	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 : 𝐼 ⟶ ℕ0 )
54	46	simprd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 ∘r ≤ 𝑦 )
55	4	psrbagcon	⊢ ( ( 𝑦 ∈ 𝐷 ∧ 𝑧 : 𝐼 ⟶ ℕ0 ∧ 𝑧 ∘r ≤ 𝑦 ) → ( ( 𝑦 ∘f − 𝑧 ) ∈ 𝐷 ∧ ( 𝑦 ∘f − 𝑧 ) ∘r ≤ 𝑦 ) )
56	51 53 54 55	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( ( 𝑦 ∘f − 𝑧 ) ∈ 𝐷 ∧ ( 𝑦 ∘f − 𝑧 ) ∘r ≤ 𝑦 ) )
57	56	simpld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( 𝑦 ∘f − 𝑧 ) ∈ 𝐷 )
58	50 57	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
59	11 18	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ∈ ( Base ‘ 𝑅 ) )
60	41 48 58 59	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ∈ ( Base ‘ 𝑅 ) )
61	60	fmpttd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) : { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ⟶ ( Base ‘ 𝑅 ) )
62		eldifi	⊢ ( 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) → 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } )
63	62 57	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ( 𝑦 ∘f − 𝑧 ) ∈ 𝐷 )
64		eqeq1	⊢ ( 𝑥 = ( 𝑦 ∘f − 𝑧 ) → ( 𝑥 = ( 𝐼 × { 0 } ) ↔ ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) ) )
65	64	ifbid	⊢ ( 𝑥 = ( 𝑦 ∘f − 𝑧 ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) = if ( ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) , 1 , 0 ) )
66	6	fvexi	⊢ 1 ∈ V
67	5	fvexi	⊢ 0 ∈ V
68	66 67	ifex	⊢ if ( ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) , 1 , 0 ) ∈ V
69	65 7 68	fvmpt	⊢ ( ( 𝑦 ∘f − 𝑧 ) ∈ 𝐷 → ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) = if ( ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) , 1 , 0 ) )
70	63 69	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) = if ( ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) , 1 , 0 ) )
71		eldifsni	⊢ ( 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) → 𝑧 ≠ 𝑦 )
72	71	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → 𝑧 ≠ 𝑦 )
73	72	necomd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → 𝑦 ≠ 𝑧 )
74	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝐼 ∈ 𝑉 )
75		nn0sscn	⊢ ℕ0 ⊆ ℂ
76		fss	⊢ ( ( 𝑦 : 𝐼 ⟶ ℕ0 ∧ ℕ0 ⊆ ℂ ) → 𝑦 : 𝐼 ⟶ ℂ )
77	26 75 76	sylancl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 : 𝐼 ⟶ ℂ )
78	77	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑦 : 𝐼 ⟶ ℂ )
79		fss	⊢ ( ( 𝑧 : 𝐼 ⟶ ℕ0 ∧ ℕ0 ⊆ ℂ ) → 𝑧 : 𝐼 ⟶ ℂ )
80	53 75 79	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 : 𝐼 ⟶ ℂ )
81		ofsubeq0	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 : 𝐼 ⟶ ℂ ∧ 𝑧 : 𝐼 ⟶ ℂ ) → ( ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) ↔ 𝑦 = 𝑧 ) )
82	74 78 80 81	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) ↔ 𝑦 = 𝑧 ) )
83	62 82	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ( ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) ↔ 𝑦 = 𝑧 ) )
84	83	necon3bbid	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ( ¬ ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) ↔ 𝑦 ≠ 𝑧 ) )
85	73 84	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ¬ ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) )
86	85	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → if ( ( 𝑦 ∘f − 𝑧 ) = ( 𝐼 × { 0 } ) , 1 , 0 ) = 0 )
87	70 86	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) = 0 )
88	87	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) = ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) )
89	11 18 5	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
90	41 48 89	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
91	62 90	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
92	88 91	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { 𝑦 } ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) = 0 )
93	92 40	suppss2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) supp 0 ) ⊆ { 𝑦 } )
94	40	mptexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ∈ V )
95		funmpt	⊢ Fun ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) )
96	95	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → Fun ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) )
97	67	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 0 ∈ V )
98		snfi	⊢ { 𝑦 } ∈ Fin
99	98	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → { 𝑦 } ∈ Fin )
100		suppssfifsupp	⊢ ( ( ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ∈ V ∧ Fun ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ∧ 0 ∈ V ) ∧ ( { 𝑦 } ∈ Fin ∧ ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) supp 0 ) ⊆ { 𝑦 } ) ) → ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) finSupp 0 )
101	94 96 97 99 93 100	syl32anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) finSupp 0 )
102	11 5 37 40 61 93 101	gsumres	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ↾ { 𝑦 } ) ) = ( 𝑅 Σg ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) )
103	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ Ring )
104		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
105	103 104	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ Mnd )
106		eqid	⊢ 𝑦 = 𝑦
107		ofsubeq0	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 : 𝐼 ⟶ ℂ ∧ 𝑦 : 𝐼 ⟶ ℂ ) → ( ( 𝑦 ∘f − 𝑦 ) = ( 𝐼 × { 0 } ) ↔ 𝑦 = 𝑦 ) )
108	24 77 77 107	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑦 ∘f − 𝑦 ) = ( 𝐼 × { 0 } ) ↔ 𝑦 = 𝑦 ) )
109	106 108	mpbiri	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑦 ∘f − 𝑦 ) = ( 𝐼 × { 0 } ) )
110	109	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) = ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) )
111		fconstmpt	⊢ ( 𝐼 × { 0 } ) = ( 𝑤 ∈ 𝐼 ↦ 0 )
112	4	fczpsrbag	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑤 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )
113	2 112	syl	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )
114	111 113	eqeltrid	⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐷 )
115	114	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐼 × { 0 } ) ∈ 𝐷 )
116		iftrue	⊢ ( 𝑥 = ( 𝐼 × { 0 } ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) = 1 )
117	116 7 66	fvmpt	⊢ ( ( 𝐼 × { 0 } ) ∈ 𝐷 → ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) = 1 )
118	115 117	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) = 1 )
119	110 118	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) = 1 )
120	119	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) ) = ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) 1 ) )
121	16	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
122	11 18 6	ringridm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑦 ) )
123	103 121 122	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑦 ) )
124	120 123	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) ) = ( 𝑋 ‘ 𝑦 ) )
125	124 121	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) ) ∈ ( Base ‘ 𝑅 ) )
126		fveq2	⊢ ( 𝑧 = 𝑦 → ( 𝑋 ‘ 𝑧 ) = ( 𝑋 ‘ 𝑦 ) )
127		oveq2	⊢ ( 𝑧 = 𝑦 → ( 𝑦 ∘f − 𝑧 ) = ( 𝑦 ∘f − 𝑦 ) )
128	127	fveq2d	⊢ ( 𝑧 = 𝑦 → ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) = ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) )
129	126 128	oveq12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) = ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) ) )
130	11 129	gsumsn	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑦 ∈ 𝐷 ∧ ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑧 ∈ { 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) = ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) ) )
131	105 21 125 130	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑧 ∈ { 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) = ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) ) )
132	34 102 131	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) = ( ( 𝑋 ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑈 ‘ ( 𝑦 ∘f − 𝑦 ) ) ) )
133	22 132 124	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 · 𝑈 ) ‘ 𝑦 ) = ( 𝑋 ‘ 𝑦 ) )
134	15 17 133	eqfnfvd	⊢ ( 𝜑 → ( 𝑋 · 𝑈 ) = 𝑋 )