Metamath Proof Explorer

Theorem psrlidm

Description: The identity element of the ring of power series is a left 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 psrlidm ( 𝜑 → ( 𝑈 · 𝑋 ) = 𝑋 )

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 12 10 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 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑈 ∈ 𝐵 )
20 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑋 ∈ 𝐵 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
22 1 8 18 9 4 19 20 21 psrmulval ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑈 · 𝑋 ) ‘ 𝑦 ) = ( 𝑅 Σg ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) )
23 breq1 ⊢ ( 𝑔 = ( 𝐼 × { 0 } ) → ( 𝑔 ∘r ≤ 𝑦 ↔ ( 𝐼 × { 0 } ) ∘r ≤ 𝑦 ) )
24 fconstmpt ⊢ ( 𝐼 × { 0 } ) = ( 𝑥 ∈ 𝐼 ↦ 0 )
25 4 fczpsrbag ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )
26 2 25 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )
27 24 26 eqeltrid ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐷 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐼 × { 0 } ) ∈ 𝐷 )
29 4 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 : 𝐼 ⟶ ℕ0 )
30 2 29 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 : 𝐼 ⟶ ℕ0 )
31 30 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ℕ0 )
32 31 nn0ge0d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( 𝑦 ‘ 𝑥 ) )
33 32 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ∀ 𝑥 ∈ 𝐼 0 ≤ ( 𝑦 ‘ 𝑥 ) )
34 0nn0 ⊢ 0 ∈ ℕ0
35 34 fconst6 ⊢ ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℕ0
36 ffn ⊢ ( ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℕ0 → ( 𝐼 × { 0 } ) Fn 𝐼 )
37 35 36 mp1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐼 × { 0 } ) Fn 𝐼 )
38 30 ffnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 Fn 𝐼 )
39 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
40 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
41 34 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 0 ∈ ℕ0 )
42 fvconst2g ⊢ ( ( 0 ∈ ℕ0 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) = 0 )
43 41 42 sylan ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) = 0 )
44 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) = ( 𝑦 ‘ 𝑥 ) )
45 37 38 39 39 40 43 44 ofrfval ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐼 × { 0 } ) ∘r ≤ 𝑦 ↔ ∀ 𝑥 ∈ 𝐼 0 ≤ ( 𝑦 ‘ 𝑥 ) ) )
46 33 45 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐼 × { 0 } ) ∘r ≤ 𝑦 )
47 23 28 46 elrabd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐼 × { 0 } ) ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } )
48 47 snssd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → { ( 𝐼 × { 0 } ) } ⊆ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } )
49 48 resmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ↾ { ( 𝐼 × { 0 } ) } ) = ( 𝑧 ∈ { ( 𝐼 × { 0 } ) } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) )
50 49 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ↾ { ( 𝐼 × { 0 } ) } ) ) = ( 𝑅 Σg ( 𝑧 ∈ { ( 𝐼 × { 0 } ) } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) )
51 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
52 3 51 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
54 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
55 4 54 rab2ex ⊢ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∈ V
56 55 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∈ V )
57 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑅 ∈ Ring )
58 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } )
59 breq1 ⊢ ( 𝑔 = 𝑧 → ( 𝑔 ∘r ≤ 𝑦 ↔ 𝑧 ∘r ≤ 𝑦 ) )
60 59 elrab ⊢ ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↔ ( 𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦 ) )
61 58 60 sylib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( 𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦 ) )
62 61 simpld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 ∈ 𝐷 )
63 1 11 4 8 19 psrelbas ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑈 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
64 63 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝑈 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
65 62 64 syldan ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( 𝑈 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
66 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
67 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝐼 ∈ 𝑉 )
68 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑦 ∈ 𝐷 )
69 4 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐷 ) → 𝑧 : 𝐼 ⟶ ℕ0 )
70 67 62 69 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 : 𝐼 ⟶ ℕ0 )
71 61 simprd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → 𝑧 ∘r ≤ 𝑦 )
72 4 psrbagcon ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐷 ∧ 𝑧 : 𝐼 ⟶ ℕ0 ∧ 𝑧 ∘r ≤ 𝑦 ) ) → ( ( 𝑦 ∘f − 𝑧 ) ∈ 𝐷 ∧ ( 𝑦 ∘f − 𝑧 ) ∘r ≤ 𝑦 ) )
73 67 68 70 71 72 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( ( 𝑦 ∘f − 𝑧 ) ∈ 𝐷 ∧ ( 𝑦 ∘f − 𝑧 ) ∘r ≤ 𝑦 ) )
74 73 simpld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( 𝑦 ∘f − 𝑧 ) ∈ 𝐷 )
75 66 74 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
76 11 18 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ∈ ( Base ‘ 𝑅 ) )
77 57 65 75 76 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ) → ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ∈ ( Base ‘ 𝑅 ) )
78 77 fmpttd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) : { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ⟶ ( Base ‘ 𝑅 ) )
79 eldifi ⊢ ( 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) → 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } )
80 79 61 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ( 𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦 ) )
81 80 simpld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → 𝑧 ∈ 𝐷 )
82 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( 𝐼 × { 0 } ) ↔ 𝑧 = ( 𝐼 × { 0 } ) ) )
83 82 ifbid ⊢ ( 𝑥 = 𝑧 → if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) = if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
84 6 fvexi ⊢ 1 ∈ V
85 5 fvexi ⊢ 0 ∈ V
86 84 85 ifex ⊢ if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) ∈ V
87 83 7 86 fvmpt ⊢ ( 𝑧 ∈ 𝐷 → ( 𝑈 ‘ 𝑧 ) = if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
88 81 87 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ( 𝑈 ‘ 𝑧 ) = if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
89 eldifn ⊢ ( 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) → ¬ 𝑧 ∈ { ( 𝐼 × { 0 } ) } )
90 89 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ¬ 𝑧 ∈ { ( 𝐼 × { 0 } ) } )
91 velsn ⊢ ( 𝑧 ∈ { ( 𝐼 × { 0 } ) } ↔ 𝑧 = ( 𝐼 × { 0 } ) )
92 90 91 sylnib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ¬ 𝑧 = ( 𝐼 × { 0 } ) )
93 92 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) = 0 )
94 88 93 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ( 𝑈 ‘ 𝑧 ) = 0 )
95 94 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) = ( 0 ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) )
96 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → 𝑅 ∈ Ring )
97 79 75 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
98 11 18 5 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) = 0 )
99 96 97 98 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) = 0 )
100 95 99 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ∖ { ( 𝐼 × { 0 } ) } ) ) → ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) = 0 )
101 100 56 suppss2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) supp 0 ) ⊆ { ( 𝐼 × { 0 } ) } )
102 4 54 rabex2 ⊢ 𝐷 ∈ V
103 102 mptrabex ⊢ ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ∈ V
104 103 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ∈ V )
105 funmpt ⊢ Fun ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) )
106 105 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → Fun ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) )
107 85 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 0 ∈ V )
108 snfi ⊢ { ( 𝐼 × { 0 } ) } ∈ Fin
109 108 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → { ( 𝐼 × { 0 } ) } ∈ Fin )
110 suppssfifsupp ⊢ ( ( ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ∈ V ∧ Fun ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ∧ 0 ∈ V ) ∧ ( { ( 𝐼 × { 0 } ) } ∈ Fin ∧ ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) supp 0 ) ⊆ { ( 𝐼 × { 0 } ) } ) ) → ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) finSupp 0 )
111 104 106 107 109 101 110 syl32anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) finSupp 0 )
112 11 5 53 56 78 101 111 gsumres ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ↾ { ( 𝐼 × { 0 } ) } ) ) = ( 𝑅 Σg ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) )
113 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ Ring )
114 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
115 113 114 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ Mnd )
116 iftrue ⊢ ( 𝑥 = ( 𝐼 × { 0 } ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) = 1 )
117 116 7 84 fvmpt ⊢ ( ( 𝐼 × { 0 } ) ∈ 𝐷 → ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) = 1 )
118 28 117 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) = 1 )
119 nn0cn ⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ∈ ℂ )
120 119 subid1d ⊢ ( 𝑧 ∈ ℕ0 → ( 𝑧 − 0 ) = 𝑧 )
121 120 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ ℕ0 ) → ( 𝑧 − 0 ) = 𝑧 )
122 39 30 41 121 caofid0r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) = 𝑦 )
123 122 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) = ( 𝑋 ‘ 𝑦 ) )
124 118 123 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) ) = ( 1 ( .r ‘ 𝑅 ) ( 𝑋 ‘ 𝑦 ) ) )
125 16 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
126 11 18 6 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( 1 ( .r ‘ 𝑅 ) ( 𝑋 ‘ 𝑦 ) ) = ( 𝑋 ‘ 𝑦 ) )
127 113 125 126 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 1 ( .r ‘ 𝑅 ) ( 𝑋 ‘ 𝑦 ) ) = ( 𝑋 ‘ 𝑦 ) )
128 124 127 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) ) = ( 𝑋 ‘ 𝑦 ) )
129 128 125 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
130 fveq2 ⊢ ( 𝑧 = ( 𝐼 × { 0 } ) → ( 𝑈 ‘ 𝑧 ) = ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) )
131 oveq2 ⊢ ( 𝑧 = ( 𝐼 × { 0 } ) → ( 𝑦 ∘f − 𝑧 ) = ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) )
132 131 fveq2d ⊢ ( 𝑧 = ( 𝐼 × { 0 } ) → ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) = ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) )
133 130 132 oveq12d ⊢ ( 𝑧 = ( 𝐼 × { 0 } ) → ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) = ( ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) ) )
134 11 133 gsumsn ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝐼 × { 0 } ) ∈ 𝐷 ∧ ( ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑧 ∈ { ( 𝐼 × { 0 } ) } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) = ( ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) ) )
135 115 28 129 134 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑧 ∈ { ( 𝐼 × { 0 } ) } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) = ( ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) ) )
136 50 112 135 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑧 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦 } ↦ ( ( 𝑈 ‘ 𝑧 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − 𝑧 ) ) ) ) ) = ( ( 𝑈 ‘ ( 𝐼 × { 0 } ) ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑦 ∘f − ( 𝐼 × { 0 } ) ) ) ) )
137 22 136 128 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑈 · 𝑋 ) ‘ 𝑦 ) = ( 𝑋 ‘ 𝑦 ) )
138 15 17 137 eqfnfvd ⊢ ( 𝜑 → ( 𝑈 · 𝑋 ) = 𝑋 )