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

Metamath Proof Explorer

Theorem elrspunsn

Description: Membership to the span of an ideal R and a single element X . (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses elrspunidl.n ⊢ 𝑁 = ( RSpan ‘ 𝑅 )
elrspunidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
elrspunidl.1 ⊢ 0 = ( 0g ‘ 𝑅 )
elrspunidl.x ⊢ · = ( .r ‘ 𝑅 )
elrspunidl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
elrspunsn.p ⊢ + = ( +g ‘ 𝑅 )
elrspunsn.i ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
elrspunsn.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝐼 ) )
Assertion elrspunsn ( 𝜑 → ( 𝐴 ∈ ( 𝑁 ‘ ( 𝐼 ∪ { 𝑋 } ) ) ↔ ∃ 𝑟 ∈ 𝐵 ∃ 𝑖 ∈ 𝐼 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) )

Proof

Step Hyp Ref Expression
1 elrspunidl.n ⊢ 𝑁 = ( RSpan ‘ 𝑅 )
2 elrspunidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 elrspunidl.1 ⊢ 0 = ( 0g ‘ 𝑅 )
4 elrspunidl.x ⊢ · = ( .r ‘ 𝑅 )
5 elrspunidl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 elrspunsn.p ⊢ + = ( +g ‘ 𝑅 )
7 elrspunsn.i ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
8 elrspunsn.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝐼 ) )
9 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
10 2 9 lidlss ⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
11 7 10 syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
12 8 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
13 12 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
14 11 13 unssd ⊢ ( 𝜑 → ( 𝐼 ∪ { 𝑋 } ) ⊆ 𝐵 )
15 1 2 3 4 5 14 elrsp ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑁 ‘ ( 𝐼 ∪ { 𝑋 } ) ) ↔ ∃ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ( 𝑎 finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ) )
16 oveq1 ⊢ ( 𝑟 = ( 𝑎 ‘ 𝑋 ) → ( 𝑟 · 𝑋 ) = ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) )
17 16 oveq1d ⊢ ( 𝑟 = ( 𝑎 ‘ 𝑋 ) → ( ( 𝑟 · 𝑋 ) + 𝑖 ) = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + 𝑖 ) )
18 17 eqeq2d ⊢ ( 𝑟 = ( 𝑎 ‘ 𝑋 ) → ( 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ↔ 𝐴 = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + 𝑖 ) ) )
19 oveq2 ⊢ ( 𝑖 = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) → ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + 𝑖 ) = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
20 19 eqeq2d ⊢ ( 𝑖 = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) → ( 𝐴 = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + 𝑖 ) ↔ 𝐴 = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ) )
21 elmapi ⊢ ( 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) → 𝑎 : ( 𝐼 ∪ { 𝑋 } ) ⟶ 𝐵 )
22 21 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝑎 : ( 𝐼 ∪ { 𝑋 } ) ⟶ 𝐵 )
23 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝑋 ∈ 𝐵 )
24 snidg ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ { 𝑋 } )
25 elun2 ⊢ ( 𝑋 ∈ { 𝑋 } → 𝑋 ∈ ( 𝐼 ∪ { 𝑋 } ) )
26 23 24 25 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝑋 ∈ ( 𝐼 ∪ { 𝑋 } ) )
27 22 26 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑎 ‘ 𝑋 ) ∈ 𝐵 )
28 2 fvexi ⊢ 𝐵 ∈ V
29 28 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝐵 ∈ V )
30 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
31 ssun1 ⊢ 𝐼 ⊆ ( 𝐼 ∪ { 𝑋 } )
32 31 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝐼 ⊆ ( 𝐼 ∪ { 𝑋 } ) )
33 22 32 fssresd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑎 ↾ 𝐼 ) : 𝐼 ⟶ 𝐵 )
34 29 30 33 elmapdd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑎 ↾ 𝐼 ) ∈ ( 𝐵 ↑m 𝐼 ) )
35 breq1 ⊢ ( 𝑏 = ( 𝑎 ↾ 𝐼 ) → ( 𝑏 finSupp 0 ↔ ( 𝑎 ↾ 𝐼 ) finSupp 0 ) )
36 fveq1 ⊢ ( 𝑏 = ( 𝑎 ↾ 𝐼 ) → ( 𝑏 ‘ 𝑦 ) = ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) )
37 36 oveq1d ⊢ ( 𝑏 = ( 𝑎 ↾ 𝐼 ) → ( ( 𝑏 ‘ 𝑦 ) · 𝑦 ) = ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) )
38 37 mpteq2dv ⊢ ( 𝑏 = ( 𝑎 ↾ 𝐼 ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑦 ) · 𝑦 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) )
39 38 oveq2d ⊢ ( 𝑏 = ( 𝑎 ↾ 𝐼 ) → ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑦 ) · 𝑦 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) ) )
40 39 eqeq2d ⊢ ( 𝑏 = ( 𝑎 ↾ 𝐼 ) → ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑦 ) · 𝑦 ) ) ) ↔ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) ) ) )
41 35 40 anbi12d ⊢ ( 𝑏 = ( 𝑎 ↾ 𝐼 ) → ( ( 𝑏 finSupp 0 ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑦 ) · 𝑦 ) ) ) ) ↔ ( ( 𝑎 ↾ 𝐼 ) finSupp 0 ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) ) ) ) )
42 41 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ∧ 𝑏 = ( 𝑎 ↾ 𝐼 ) ) → ( ( 𝑏 finSupp 0 ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑦 ) · 𝑦 ) ) ) ) ↔ ( ( 𝑎 ↾ 𝐼 ) finSupp 0 ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) ) ) ) )
43 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝑎 finSupp 0 )
44 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝑅 ∈ Ring )
45 2 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
46 44 45 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 0 ∈ 𝐵 )
47 43 46 fsuppres ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑎 ↾ 𝐼 ) finSupp 0 )
48 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑦 ) )
49 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
50 48 49 oveq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) = ( ( 𝑎 ‘ 𝑦 ) · 𝑦 ) )
51 50 cbvmptv ⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑦 ) · 𝑦 ) )
52 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
53 52 fvresd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) )
54 53 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) = ( ( 𝑎 ‘ 𝑦 ) · 𝑦 ) )
55 54 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑦 ) · 𝑦 ) ) )
56 51 55 eqtr4id ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) )
57 56 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) ) )
58 47 57 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( ( 𝑎 ↾ 𝐼 ) finSupp 0 ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ↾ 𝐼 ) ‘ 𝑦 ) · 𝑦 ) ) ) ) )
59 34 42 58 rspcedvd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ∃ 𝑏 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑏 finSupp 0 ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑦 ) · 𝑦 ) ) ) ) )
60 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝐼 ⊆ 𝐵 )
61 1 2 3 4 44 60 elrsp ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ∈ ( 𝑁 ‘ 𝐼 ) ↔ ∃ 𝑏 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑏 finSupp 0 ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑦 ) · 𝑦 ) ) ) ) ) )
62 59 61 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ∈ ( 𝑁 ‘ 𝐼 ) )
63 1 9 rspidlid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝐼 ) = 𝐼 )
64 5 7 63 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐼 ) = 𝐼 )
65 64 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑁 ‘ 𝐼 ) = 𝐼 )
66 62 65 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ∈ 𝐼 )
67 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) )
68 5 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
69 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝑅 ∈ CMnd )
70 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
71 snex ⊢ { 𝑋 } ∈ V
72 71 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → { 𝑋 } ∈ V )
73 70 72 unexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝐼 ∪ { 𝑋 } ) ∈ V )
74 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 𝑅 ∈ Ring )
75 21 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 𝑎 : ( 𝐼 ∪ { 𝑋 } ) ⟶ 𝐵 )
76 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) )
77 75 76 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → ( 𝑎 ‘ 𝑥 ) ∈ 𝐵 )
78 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → ( 𝐼 ∪ { 𝑋 } ) ⊆ 𝐵 )
79 78 76 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 𝑥 ∈ 𝐵 )
80 2 4 74 77 79 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ∈ 𝐵 )
81 73 mptexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ∈ V )
82 5 45 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
83 82 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 0 ∈ 𝐵 )
84 funmpt ⊢ Fun ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) )
85 84 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → Fun ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) )
86 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝑎 finSupp 0 )
87 86 fsuppimpd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑎 supp 0 ) ∈ Fin )
88 21 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → 𝑎 : ( 𝐼 ∪ { 𝑋 } ) ⟶ 𝐵 )
89 88 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → 𝑎 Fn ( 𝐼 ∪ { 𝑋 } ) )
90 73 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → ( 𝐼 ∪ { 𝑋 } ) ∈ V )
91 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → 𝑅 ∈ Ring )
92 91 45 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → 0 ∈ 𝐵 )
93 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) )
94 89 90 92 93 fvdifsupp ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → ( 𝑎 ‘ 𝑥 ) = 0 )
95 94 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) = ( 0 · 𝑥 ) )
96 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → ( 𝐼 ∪ { 𝑋 } ) ⊆ 𝐵 )
97 93 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) )
98 96 97 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → 𝑥 ∈ 𝐵 )
99 2 4 3 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 0 · 𝑥 ) = 0 )
100 91 98 99 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → ( 0 · 𝑥 ) = 0 )
101 95 100 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) ) → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) = 0 )
102 101 73 suppss2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) supp 0 ) ⊆ ( 𝑎 supp 0 ) )
103 87 102 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) supp 0 ) ∈ Fin )
104 81 83 85 103 isfsuppd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) finSupp 0 )
105 8 eldifbd ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐼 )
106 105 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ¬ 𝑋 ∈ 𝐼 )
107 disjsn ⊢ ( ( 𝐼 ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ 𝐼 )
108 106 107 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝐼 ∩ { 𝑋 } ) = ∅ )
109 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝐼 ∪ { 𝑋 } ) = ( 𝐼 ∪ { 𝑋 } ) )
110 2 3 6 69 73 80 104 108 109 gsumsplit2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) + ( 𝑅 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
111 69 cmnmndd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝑅 ∈ Mnd )
112 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝑋 ∈ 𝐵 )
113 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝑅 ∈ Ring )
114 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝑎 : ( 𝐼 ∪ { 𝑋 } ) ⟶ 𝐵 )
115 ssun2 ⊢ { 𝑋 } ⊆ ( 𝐼 ∪ { 𝑋 } )
116 12 24 syl ⊢ ( 𝜑 → 𝑋 ∈ { 𝑋 } )
117 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝑋 ∈ { 𝑋 } )
118 115 117 sselid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝑋 ∈ ( 𝐼 ∪ { 𝑋 } ) )
119 114 118 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑎 ‘ 𝑋 ) ∈ 𝐵 )
120 2 4 113 119 112 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) ∈ 𝐵 )
121 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
122 121 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 = 𝑋 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑋 ) )
123 122 121 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 = 𝑋 ) → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) = ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) )
124 2 111 112 120 123 gsumsnd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) )
125 124 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) + ( 𝑅 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) + ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) ) )
126 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Ring )
127 21 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑎 : ( 𝐼 ∪ { 𝑋 } ) ⟶ 𝐵 )
128 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
129 31 128 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) )
130 127 129 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑥 ) ∈ 𝐵 )
131 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ⊆ 𝐵 )
132 131 128 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐵 )
133 2 4 126 130 132 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ∈ 𝐵 )
134 133 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) : 𝐼 ⟶ 𝐵 )
135 31 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → 𝐼 ⊆ ( 𝐼 ∪ { 𝑋 } ) )
136 135 ssdifd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ⊆ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) )
137 136 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( 𝑎 supp 0 ) ) )
138 137 94 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → ( 𝑎 ‘ 𝑥 ) = 0 )
139 138 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) = ( 0 · 𝑥 ) )
140 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → 𝑅 ∈ Ring )
141 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → 𝐼 ⊆ 𝐵 )
142 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) )
143 142 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → 𝑥 ∈ 𝐼 )
144 141 143 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → 𝑥 ∈ 𝐵 )
145 140 144 99 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → ( 0 · 𝑥 ) = 0 )
146 139 145 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑎 supp 0 ) ) ) → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) = 0 )
147 146 70 suppss2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) supp 0 ) ⊆ ( 𝑎 supp 0 ) )
148 87 147 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) supp 0 ) ∈ Fin )
149 2 3 69 70 134 148 gsumcl2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ∈ 𝐵 )
150 2 6 cmncom ⊢ ( ( 𝑅 ∈ CMnd ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ∈ 𝐵 ∧ ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) + ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) ) = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
151 69 149 120 150 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) + ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) ) = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
152 110 125 151 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) → ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
153 152 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
154 67 153 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → 𝐴 = ( ( ( 𝑎 ‘ 𝑋 ) · 𝑋 ) + ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
155 18 20 27 66 154 2rspcedvdw ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) → ∃ 𝑟 ∈ 𝐵 ∃ 𝑖 ∈ 𝐼 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) )
156 155 anasss ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ) ∧ ( 𝑎 finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ) → ∃ 𝑟 ∈ 𝐵 ∃ 𝑖 ∈ 𝐼 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) )
157 156 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ( 𝑎 finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ) → ∃ 𝑟 ∈ 𝐵 ∃ 𝑖 ∈ 𝐼 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) )
158 28 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝐵 ∈ V )
159 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
160 71 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → { 𝑋 } ∈ V )
161 159 160 unexd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝐼 ∪ { 𝑋 } ) ∈ V )
162 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 𝑟 ∈ 𝐵 )
163 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
164 2 163 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
165 5 164 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
166 165 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
167 162 166 ifcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
168 82 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 0 ∈ 𝐵 )
169 167 168 ifcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ∈ 𝐵 )
170 169 fmpttd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) : ( 𝐼 ∪ { 𝑋 } ) ⟶ 𝐵 )
171 158 161 170 elmapdd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) )
172 breq1 ⊢ ( 𝑎 = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) → ( 𝑎 finSupp 0 ↔ ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) finSupp 0 ) )
173 fveq1 ⊢ ( 𝑎 = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) → ( 𝑎 ‘ 𝑥 ) = ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) )
174 173 oveq1d ⊢ ( 𝑎 = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) → ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) = ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) )
175 174 mpteq2dv ⊢ ( 𝑎 = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) → ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) = ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) )
176 175 oveq2d ⊢ ( 𝑎 = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) → ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) )
177 176 eqeq2d ⊢ ( 𝑎 = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) → ( 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ↔ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) ) )
178 172 177 anbi12d ⊢ ( 𝑎 = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) → ( ( 𝑎 finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ↔ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) ) ) )
179 178 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑎 = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ) → ( ( 𝑎 finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ↔ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) ) ) )
180 eqid ⊢ ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) = ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) )
181 prfi ⊢ { 𝑋 , 𝑖 } ∈ Fin
182 181 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → { 𝑋 , 𝑖 } ∈ Fin )
183 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑦 ∈ { 𝑋 , 𝑖 } ) → 𝑟 ∈ 𝐵 )
184 165 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑦 ∈ { 𝑋 , 𝑖 } ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
185 183 184 ifcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑦 ∈ { 𝑋 , 𝑖 } ) → if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
186 82 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 0 ∈ 𝐵 )
187 180 161 182 185 186 mptiffisupp ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) finSupp 0 )
188 68 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑅 ∈ CMnd )
189 159 10 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝐼 ⊆ 𝐵 )
190 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑖 ∈ 𝐼 )
191 189 190 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑖 ∈ 𝐵 )
192 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑅 ∈ Ring )
193 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑟 ∈ 𝐵 )
194 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑋 ∈ 𝐵 )
195 2 4 192 193 194 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑟 · 𝑋 ) ∈ 𝐵 )
196 2 6 cmncom ⊢ ( ( 𝑅 ∈ CMnd ∧ 𝑖 ∈ 𝐵 ∧ ( 𝑟 · 𝑋 ) ∈ 𝐵 ) → ( 𝑖 + ( 𝑟 · 𝑋 ) ) = ( ( 𝑟 · 𝑋 ) + 𝑖 ) )
197 188 191 195 196 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑖 + ( 𝑟 · 𝑋 ) ) = ( ( 𝑟 · 𝑋 ) + 𝑖 ) )
198 188 cmnmndd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑅 ∈ Mnd )
199 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑖 , 𝑖 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑖 , 𝑖 , 0 ) )
200 191 2 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑖 ∈ ( Base ‘ 𝑅 ) )
201 3 198 159 190 199 200 gsummptif1n0 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑖 , 𝑖 , 0 ) ) ) = 𝑖 )
202 fveq2 ⊢ ( 𝑥 = 𝑖 → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑖 ) )
203 id ⊢ ( 𝑥 = 𝑖 → 𝑥 = 𝑖 )
204 202 203 oveq12d ⊢ ( 𝑥 = 𝑖 → ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) = ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑖 ) · 𝑖 ) )
205 204 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) = ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑖 ) · 𝑖 ) )
206 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → 𝑦 = 𝑖 )
207 prid2g ⊢ ( 𝑖 ∈ 𝐼 → 𝑖 ∈ { 𝑋 , 𝑖 } )
208 207 ad5antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → 𝑖 ∈ { 𝑋 , 𝑖 } )
209 206 208 eqeltrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → 𝑦 ∈ { 𝑋 , 𝑖 } )
210 209 iftrued ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) = if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) )
211 190 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → 𝑖 ∈ 𝐼 )
212 211 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → 𝑖 ∈ 𝐼 )
213 206 212 eqeltrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → 𝑦 ∈ 𝐼 )
214 105 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ¬ 𝑋 ∈ 𝐼 )
215 214 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → ¬ 𝑋 ∈ 𝐼 )
216 nelneq ⊢ ( ( 𝑦 ∈ 𝐼 ∧ ¬ 𝑋 ∈ 𝐼 ) → ¬ 𝑦 = 𝑋 )
217 213 215 216 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → ¬ 𝑦 = 𝑋 )
218 217 iffalsed ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
219 210 218 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) ∧ 𝑦 = 𝑖 ) → if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) = ( 1r ‘ 𝑅 ) )
220 31 211 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → 𝑖 ∈ ( 𝐼 ∪ { 𝑋 } ) )
221 192 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → 𝑅 ∈ Ring )
222 221 164 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
223 180 219 220 222 fvmptd2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑖 ) = ( 1r ‘ 𝑅 ) )
224 223 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑖 ) · 𝑖 ) = ( ( 1r ‘ 𝑅 ) · 𝑖 ) )
225 191 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → 𝑖 ∈ 𝐵 )
226 2 4 163 221 225 ringlidmd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → ( ( 1r ‘ 𝑅 ) · 𝑖 ) = 𝑖 )
227 205 224 226 3eqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑖 ) → 𝑖 = ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) )
228 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑋 , 𝑖 } ↔ 𝑥 ∈ { 𝑋 , 𝑖 } ) )
229 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝑋 ↔ 𝑥 = 𝑋 ) )
230 229 ifbid ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) = if ( 𝑥 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) )
231 228 230 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) = if ( 𝑥 ∈ { 𝑋 , 𝑖 } , if ( 𝑥 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) )
232 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 𝑥 ∈ 𝐼 )
233 31 232 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) )
234 193 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 𝑟 ∈ 𝐵 )
235 165 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
236 234 235 ifcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → if ( 𝑥 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
237 186 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 0 ∈ 𝐵 )
238 236 237 ifcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → if ( 𝑥 ∈ { 𝑋 , 𝑖 } , if ( 𝑥 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ∈ 𝐵 )
239 180 231 233 238 fvmptd3 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ { 𝑋 , 𝑖 } , if ( 𝑥 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) )
240 214 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → ¬ 𝑋 ∈ 𝐼 )
241 nelne2 ⊢ ( ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑋 ∈ 𝐼 ) → 𝑥 ≠ 𝑋 )
242 232 240 241 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 𝑥 ≠ 𝑋 )
243 neqne ⊢ ( ¬ 𝑥 = 𝑖 → 𝑥 ≠ 𝑖 )
244 243 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 𝑥 ≠ 𝑖 )
245 242 244 nelprd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → ¬ 𝑥 ∈ { 𝑋 , 𝑖 } )
246 245 iffalsed ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → if ( 𝑥 ∈ { 𝑋 , 𝑖 } , if ( 𝑥 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) = 0 )
247 239 246 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) = 0 )
248 247 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) = ( 0 · 𝑥 ) )
249 192 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 𝑅 ∈ Ring )
250 189 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 𝐼 ⊆ 𝐵 )
251 250 232 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 𝑥 ∈ 𝐵 )
252 249 251 99 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → ( 0 · 𝑥 ) = 0 )
253 248 252 eqtr2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 = 𝑖 ) → 0 = ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) )
254 227 253 ifeqda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ 𝐼 ) → if ( 𝑥 = 𝑖 , 𝑖 , 0 ) = ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) )
255 254 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑖 , 𝑖 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) )
256 255 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑖 , 𝑖 , 0 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) )
257 201 256 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝑖 = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) )
258 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
259 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → 𝑥 = 𝑋 )
260 194 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → 𝑋 ∈ 𝐵 )
261 prid1g ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ { 𝑋 , 𝑖 } )
262 260 261 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → 𝑋 ∈ { 𝑋 , 𝑖 } )
263 259 262 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → 𝑥 ∈ { 𝑋 , 𝑖 } )
264 258 263 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → 𝑦 ∈ { 𝑋 , 𝑖 } )
265 264 iftrued ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) = if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) )
266 258 259 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑋 )
267 266 iftrued ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) = 𝑟 )
268 265 267 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑥 ) → if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) = 𝑟 )
269 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
270 116 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) → 𝑋 ∈ { 𝑋 } )
271 270 25 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) → 𝑋 ∈ ( 𝐼 ∪ { 𝑋 } ) )
272 269 271 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) → 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) )
273 193 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) → 𝑟 ∈ 𝐵 )
274 180 268 272 273 fvmptd2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) = 𝑟 )
275 274 269 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 = 𝑋 ) → ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) = ( 𝑟 · 𝑋 ) )
276 2 198 194 195 275 gsumsnd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) = ( 𝑟 · 𝑋 ) )
277 276 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑟 · 𝑋 ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) )
278 257 277 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑖 + ( 𝑟 · 𝑋 ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) + ( 𝑅 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) ) )
279 197 278 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( ( 𝑟 · 𝑋 ) + 𝑖 ) = ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) + ( 𝑅 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) ) )
280 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) )
281 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 𝑅 ∈ Ring )
282 170 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) ∈ 𝐵 )
283 14 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → ( 𝐼 ∪ { 𝑋 } ) ⊆ 𝐵 )
284 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) )
285 283 284 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → 𝑥 ∈ 𝐵 )
286 2 4 281 282 285 ringcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ) → ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ∈ 𝐵 )
287 161 mptexd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ∈ V )
288 funmpt ⊢ Fun ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) )
289 288 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → Fun ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) )
290 187 fsuppimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ∈ Fin )
291 nfv ⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) )
292 291 169 180 fnmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) Fn ( 𝐼 ∪ { 𝑋 } ) )
293 292 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) Fn ( 𝐼 ∪ { 𝑋 } ) )
294 161 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → ( 𝐼 ∪ { 𝑋 } ) ∈ V )
295 186 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → 0 ∈ 𝐵 )
296 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) )
297 293 294 295 296 fvdifsupp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) = 0 )
298 297 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) = ( 0 · 𝑥 ) )
299 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → 𝑅 ∈ Ring )
300 14 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → ( 𝐼 ∪ { 𝑋 } ) ⊆ 𝐵 )
301 296 eldifad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) )
302 300 301 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → 𝑥 ∈ 𝐵 )
303 299 302 99 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → ( 0 · 𝑥 ) = 0 )
304 298 303 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) ∧ 𝑥 ∈ ( ( 𝐼 ∪ { 𝑋 } ) ∖ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) ) ) → ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) = 0 )
305 304 161 suppss2 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) supp 0 ) ⊆ ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) supp 0 ) )
306 290 305 ssfid ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) supp 0 ) ∈ Fin )
307 287 186 289 306 isfsuppd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) finSupp 0 )
308 214 107 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝐼 ∩ { 𝑋 } ) = ∅ )
309 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝐼 ∪ { 𝑋 } ) = ( 𝐼 ∪ { 𝑋 } ) )
310 2 3 6 188 161 286 307 308 309 gsumsplit2 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) + ( 𝑅 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) ) )
311 279 280 310 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) )
312 187 311 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( ( 𝑦 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ if ( 𝑦 ∈ { 𝑋 , 𝑖 } , if ( 𝑦 = 𝑋 , 𝑟 , ( 1r ‘ 𝑅 ) ) , 0 ) ) ‘ 𝑥 ) · 𝑥 ) ) ) ) )
313 171 179 312 rspcedvd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ∃ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ( 𝑎 finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
314 313 r19.29ffa ⊢ ( ( 𝜑 ∧ ∃ 𝑟 ∈ 𝐵 ∃ 𝑖 ∈ 𝐼 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) → ∃ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ( 𝑎 finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) )
315 157 314 impbida ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐵 ↑m ( 𝐼 ∪ { 𝑋 } ) ) ( 𝑎 finSupp 0 ∧ 𝐴 = ( 𝑅 Σg ( 𝑥 ∈ ( 𝐼 ∪ { 𝑋 } ) ↦ ( ( 𝑎 ‘ 𝑥 ) · 𝑥 ) ) ) ) ↔ ∃ 𝑟 ∈ 𝐵 ∃ 𝑖 ∈ 𝐼 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) )
316 15 315 bitrd ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑁 ‘ ( 𝐼 ∪ { 𝑋 } ) ) ↔ ∃ 𝑟 ∈ 𝐵 ∃ 𝑖 ∈ 𝐼 𝐴 = ( ( 𝑟 · 𝑋 ) + 𝑖 ) ) )