Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elrspunsn Structured version   Visualization version   GIF version

Theorem elrspunsn 33053
Description: Membership to the span of an ideal 𝑅 and a single element 𝑋. (Contributed by Thierry Arnoux, 9-Mar-2025.)
Hypotheses
Ref Expression
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
Ref Expression
elrspunsn (πœ‘ β†’ (𝐴 ∈ (π‘β€˜(𝐼 βˆͺ {𝑋})) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘– ∈ 𝐼 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)))
Distinct variable groups:   0 ,𝑖   Β· ,𝑖   𝐡,𝑖   𝑅,𝑖   𝑖,𝑋   πœ‘,𝑖   + ,𝑖,π‘Ÿ   0 ,π‘Ÿ   Β· ,π‘Ÿ   𝐴,𝑖,π‘Ÿ   𝐡,π‘Ÿ   𝑖,𝐼,π‘Ÿ   𝑅,π‘Ÿ   𝑋,π‘Ÿ   πœ‘,π‘Ÿ
Allowed substitution hints:   𝑁(𝑖,π‘Ÿ)

Proof of Theorem elrspunsn
Dummy variables π‘Ž 𝑏 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elrspunidl.n . . 3 𝑁 = (RSpanβ€˜π‘…)
2 elrspunidl.b . . 3 𝐡 = (Baseβ€˜π‘…)
3 elrspunidl.1 . . 3 0 = (0gβ€˜π‘…)
4 elrspunidl.x . . 3 Β· = (.rβ€˜π‘…)
5 elrspunidl.r . . 3 (πœ‘ β†’ 𝑅 ∈ Ring)
6 elrspunsn.i . . . . 5 (πœ‘ β†’ 𝐼 ∈ (LIdealβ€˜π‘…))
7 eqid 2726 . . . . . 6 (LIdealβ€˜π‘…) = (LIdealβ€˜π‘…)
82, 7lidlss 21071 . . . . 5 (𝐼 ∈ (LIdealβ€˜π‘…) β†’ 𝐼 βŠ† 𝐡)
96, 8syl 17 . . . 4 (πœ‘ β†’ 𝐼 βŠ† 𝐡)
10 elrspunsn.x . . . . . 6 (πœ‘ β†’ 𝑋 ∈ (𝐡 βˆ– 𝐼))
1110eldifad 3955 . . . . 5 (πœ‘ β†’ 𝑋 ∈ 𝐡)
1211snssd 4807 . . . 4 (πœ‘ β†’ {𝑋} βŠ† 𝐡)
139, 12unssd 4181 . . 3 (πœ‘ β†’ (𝐼 βˆͺ {𝑋}) βŠ† 𝐡)
141, 2, 3, 4, 5, 13elrsp 32992 . 2 (πœ‘ β†’ (𝐴 ∈ (π‘β€˜(𝐼 βˆͺ {𝑋})) ↔ βˆƒπ‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))(π‘Ž finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))))))
15 oveq1 7412 . . . . . . . 8 (π‘Ÿ = (π‘Žβ€˜π‘‹) β†’ (π‘Ÿ Β· 𝑋) = ((π‘Žβ€˜π‘‹) Β· 𝑋))
1615oveq1d 7420 . . . . . . 7 (π‘Ÿ = (π‘Žβ€˜π‘‹) β†’ ((π‘Ÿ Β· 𝑋) + 𝑖) = (((π‘Žβ€˜π‘‹) Β· 𝑋) + 𝑖))
1716eqeq2d 2737 . . . . . 6 (π‘Ÿ = (π‘Žβ€˜π‘‹) β†’ (𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖) ↔ 𝐴 = (((π‘Žβ€˜π‘‹) Β· 𝑋) + 𝑖)))
18 oveq2 7413 . . . . . . 7 (𝑖 = (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) β†’ (((π‘Žβ€˜π‘‹) Β· 𝑋) + 𝑖) = (((π‘Žβ€˜π‘‹) Β· 𝑋) + (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
1918eqeq2d 2737 . . . . . 6 (𝑖 = (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) β†’ (𝐴 = (((π‘Žβ€˜π‘‹) Β· 𝑋) + 𝑖) ↔ 𝐴 = (((π‘Žβ€˜π‘‹) Β· 𝑋) + (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))))))
20 elmapi 8845 . . . . . . . 8 (π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋})) β†’ π‘Ž:(𝐼 βˆͺ {𝑋})⟢𝐡)
2120ad3antlr 728 . . . . . . 7 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ π‘Ž:(𝐼 βˆͺ {𝑋})⟢𝐡)
2211ad3antrrr 727 . . . . . . . 8 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝑋 ∈ 𝐡)
23 snidg 4657 . . . . . . . 8 (𝑋 ∈ 𝐡 β†’ 𝑋 ∈ {𝑋})
24 elun2 4172 . . . . . . . 8 (𝑋 ∈ {𝑋} β†’ 𝑋 ∈ (𝐼 βˆͺ {𝑋}))
2522, 23, 243syl 18 . . . . . . 7 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝑋 ∈ (𝐼 βˆͺ {𝑋}))
2621, 25ffvelcdmd 7081 . . . . . 6 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (π‘Žβ€˜π‘‹) ∈ 𝐡)
272fvexi 6899 . . . . . . . . . . 11 𝐡 ∈ V
2827a1i 11 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝐡 ∈ V)
296ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝐼 ∈ (LIdealβ€˜π‘…))
30 ssun1 4167 . . . . . . . . . . . 12 𝐼 βŠ† (𝐼 βˆͺ {𝑋})
3130a1i 11 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝐼 βŠ† (𝐼 βˆͺ {𝑋}))
3221, 31fssresd 6752 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (π‘Ž β†Ύ 𝐼):𝐼⟢𝐡)
3328, 29, 32elmapdd 8837 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (π‘Ž β†Ύ 𝐼) ∈ (𝐡 ↑m 𝐼))
34 breq1 5144 . . . . . . . . . . 11 (𝑏 = (π‘Ž β†Ύ 𝐼) β†’ (𝑏 finSupp 0 ↔ (π‘Ž β†Ύ 𝐼) finSupp 0 ))
35 fveq1 6884 . . . . . . . . . . . . . . 15 (𝑏 = (π‘Ž β†Ύ 𝐼) β†’ (π‘β€˜π‘¦) = ((π‘Ž β†Ύ 𝐼)β€˜π‘¦))
3635oveq1d 7420 . . . . . . . . . . . . . 14 (𝑏 = (π‘Ž β†Ύ 𝐼) β†’ ((π‘β€˜π‘¦) Β· 𝑦) = (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦))
3736mpteq2dv 5243 . . . . . . . . . . . . 13 (𝑏 = (π‘Ž β†Ύ 𝐼) β†’ (𝑦 ∈ 𝐼 ↦ ((π‘β€˜π‘¦) Β· 𝑦)) = (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦)))
3837oveq2d 7421 . . . . . . . . . . . 12 (𝑏 = (π‘Ž β†Ύ 𝐼) β†’ (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ ((π‘β€˜π‘¦) Β· 𝑦))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦))))
3938eqeq2d 2737 . . . . . . . . . . 11 (𝑏 = (π‘Ž β†Ύ 𝐼) β†’ ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ ((π‘β€˜π‘¦) Β· 𝑦))) ↔ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦)))))
4034, 39anbi12d 630 . . . . . . . . . 10 (𝑏 = (π‘Ž β†Ύ 𝐼) β†’ ((𝑏 finSupp 0 ∧ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ ((π‘β€˜π‘¦) Β· 𝑦)))) ↔ ((π‘Ž β†Ύ 𝐼) finSupp 0 ∧ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦))))))
4140adantl 481 . . . . . . . . 9 (((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) ∧ 𝑏 = (π‘Ž β†Ύ 𝐼)) β†’ ((𝑏 finSupp 0 ∧ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ ((π‘β€˜π‘¦) Β· 𝑦)))) ↔ ((π‘Ž β†Ύ 𝐼) finSupp 0 ∧ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦))))))
42 simplr 766 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ π‘Ž finSupp 0 )
435ad3antrrr 727 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝑅 ∈ Ring)
442, 3ring0cl 20166 . . . . . . . . . . . 12 (𝑅 ∈ Ring β†’ 0 ∈ 𝐡)
4543, 44syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 0 ∈ 𝐡)
4642, 45fsuppres 9390 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (π‘Ž β†Ύ 𝐼) finSupp 0 )
47 fveq2 6885 . . . . . . . . . . . . . 14 (π‘₯ = 𝑦 β†’ (π‘Žβ€˜π‘₯) = (π‘Žβ€˜π‘¦))
48 id 22 . . . . . . . . . . . . . 14 (π‘₯ = 𝑦 β†’ π‘₯ = 𝑦)
4947, 48oveq12d 7423 . . . . . . . . . . . . 13 (π‘₯ = 𝑦 β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) = ((π‘Žβ€˜π‘¦) Β· 𝑦))
5049cbvmptv 5254 . . . . . . . . . . . 12 (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) = (𝑦 ∈ 𝐼 ↦ ((π‘Žβ€˜π‘¦) Β· 𝑦))
51 simpr 484 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) ∧ 𝑦 ∈ 𝐼) β†’ 𝑦 ∈ 𝐼)
5251fvresd 6905 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) ∧ 𝑦 ∈ 𝐼) β†’ ((π‘Ž β†Ύ 𝐼)β€˜π‘¦) = (π‘Žβ€˜π‘¦))
5352oveq1d 7420 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) ∧ 𝑦 ∈ 𝐼) β†’ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦) = ((π‘Žβ€˜π‘¦) Β· 𝑦))
5453mpteq2dva 5241 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦)) = (𝑦 ∈ 𝐼 ↦ ((π‘Žβ€˜π‘¦) Β· 𝑦)))
5550, 54eqtr4id 2785 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) = (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦)))
5655oveq2d 7421 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦))))
5746, 56jca 511 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ ((π‘Ž β†Ύ 𝐼) finSupp 0 ∧ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ (((π‘Ž β†Ύ 𝐼)β€˜π‘¦) Β· 𝑦)))))
5833, 41, 57rspcedvd 3608 . . . . . . . 8 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ βˆƒπ‘ ∈ (𝐡 ↑m 𝐼)(𝑏 finSupp 0 ∧ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ ((π‘β€˜π‘¦) Β· 𝑦)))))
599ad3antrrr 727 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝐼 βŠ† 𝐡)
601, 2, 3, 4, 43, 59elrsp 32992 . . . . . . . 8 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) ∈ (π‘β€˜πΌ) ↔ βˆƒπ‘ ∈ (𝐡 ↑m 𝐼)(𝑏 finSupp 0 ∧ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (𝑦 ∈ 𝐼 ↦ ((π‘β€˜π‘¦) Β· 𝑦))))))
6158, 60mpbird 257 . . . . . . 7 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) ∈ (π‘β€˜πΌ))
621, 7rspidlid 32993 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdealβ€˜π‘…)) β†’ (π‘β€˜πΌ) = 𝐼)
635, 6, 62syl2anc 583 . . . . . . . 8 (πœ‘ β†’ (π‘β€˜πΌ) = 𝐼)
6463ad3antrrr 727 . . . . . . 7 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (π‘β€˜πΌ) = 𝐼)
6561, 64eleqtrd 2829 . . . . . 6 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) ∈ 𝐼)
66 simpr 484 . . . . . . 7 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))))
67 elrspunsn.p . . . . . . . . . 10 + = (+gβ€˜π‘…)
685ringcmnd 20183 . . . . . . . . . . 11 (πœ‘ β†’ 𝑅 ∈ CMnd)
6968ad2antrr 723 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 𝑅 ∈ CMnd)
706ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 𝐼 ∈ (LIdealβ€˜π‘…))
71 snex 5424 . . . . . . . . . . . 12 {𝑋} ∈ V
7271a1i 11 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ {𝑋} ∈ V)
7370, 72unexd 7738 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (𝐼 βˆͺ {𝑋}) ∈ V)
745ad3antrrr 727 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ 𝑅 ∈ Ring)
7520ad3antlr 728 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ π‘Ž:(𝐼 βˆͺ {𝑋})⟢𝐡)
76 simpr 484 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ π‘₯ ∈ (𝐼 βˆͺ {𝑋}))
7775, 76ffvelcdmd 7081 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ (π‘Žβ€˜π‘₯) ∈ 𝐡)
7813ad3antrrr 727 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ (𝐼 βˆͺ {𝑋}) βŠ† 𝐡)
7978, 76sseldd 3978 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ π‘₯ ∈ 𝐡)
802, 4, 74, 77, 79ringcld 20162 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) ∈ 𝐡)
8173mptexd 7221 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) ∈ V)
825, 44syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 0 ∈ 𝐡)
8382ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 0 ∈ 𝐡)
84 funmpt 6580 . . . . . . . . . . . 12 Fun (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))
8584a1i 11 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ Fun (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))
86 simpr 484 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ π‘Ž finSupp 0 )
8786fsuppimpd 9371 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (π‘Ž supp 0 ) ∈ Fin)
8820ad3antlr 728 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ π‘Ž:(𝐼 βˆͺ {𝑋})⟢𝐡)
8988ffnd 6712 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ π‘Ž Fn (𝐼 βˆͺ {𝑋}))
9073adantr 480 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ (𝐼 βˆͺ {𝑋}) ∈ V)
915ad3antrrr 727 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ 𝑅 ∈ Ring)
9291, 44syl 17 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ 0 ∈ 𝐡)
93 simpr 484 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 )))
9489, 90, 92, 93fvdifsupp 32414 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ (π‘Žβ€˜π‘₯) = 0 )
9594oveq1d 7420 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) = ( 0 Β· π‘₯))
9613ad3antrrr 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ (𝐼 βˆͺ {𝑋}) βŠ† 𝐡)
9793eldifad 3955 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ π‘₯ ∈ (𝐼 βˆͺ {𝑋}))
9896, 97sseldd 3978 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ π‘₯ ∈ 𝐡)
992, 4, 3ringlz 20192 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ π‘₯ ∈ 𝐡) β†’ ( 0 Β· π‘₯) = 0 )
10091, 98, 99syl2anc 583 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ ( 0 Β· π‘₯) = 0 )
10195, 100eqtrd 2766 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 ))) β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) = 0 )
102101, 73suppss2 8186 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ ((π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) supp 0 ) βŠ† (π‘Ž supp 0 ))
10387, 102ssfid 9269 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ ((π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) supp 0 ) ∈ Fin)
10481, 83, 85, 103isfsuppd 9368 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) finSupp 0 )
10510eldifbd 3956 . . . . . . . . . . . 12 (πœ‘ β†’ Β¬ 𝑋 ∈ 𝐼)
106105ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ Β¬ 𝑋 ∈ 𝐼)
107 disjsn 4710 . . . . . . . . . . 11 ((𝐼 ∩ {𝑋}) = βˆ… ↔ Β¬ 𝑋 ∈ 𝐼)
108106, 107sylibr 233 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (𝐼 ∩ {𝑋}) = βˆ…)
109 eqidd 2727 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (𝐼 βˆͺ {𝑋}) = (𝐼 βˆͺ {𝑋}))
1102, 3, 67, 69, 73, 80, 104, 108, 109gsumsplit2 19849 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) + (𝑅 Ξ£g (π‘₯ ∈ {𝑋} ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
11169cmnmndd 19724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 𝑅 ∈ Mnd)
11211ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 𝑋 ∈ 𝐡)
1135ad2antrr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 𝑅 ∈ Ring)
11420ad2antlr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ π‘Ž:(𝐼 βˆͺ {𝑋})⟢𝐡)
115 ssun2 4168 . . . . . . . . . . . . . 14 {𝑋} βŠ† (𝐼 βˆͺ {𝑋})
11611, 23syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 ∈ {𝑋})
117116ad2antrr 723 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 𝑋 ∈ {𝑋})
118115, 117sselid 3975 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 𝑋 ∈ (𝐼 βˆͺ {𝑋}))
119114, 118ffvelcdmd 7081 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (π‘Žβ€˜π‘‹) ∈ 𝐡)
1202, 4, 113, 119, 112ringcld 20162 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ ((π‘Žβ€˜π‘‹) Β· 𝑋) ∈ 𝐡)
121 simpr 484 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ = 𝑋) β†’ π‘₯ = 𝑋)
122121fveq2d 6889 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ = 𝑋) β†’ (π‘Žβ€˜π‘₯) = (π‘Žβ€˜π‘‹))
123122, 121oveq12d 7423 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ = 𝑋) β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) = ((π‘Žβ€˜π‘‹) Β· 𝑋))
1242, 111, 112, 120, 123gsumsnd 19872 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (𝑅 Ξ£g (π‘₯ ∈ {𝑋} ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = ((π‘Žβ€˜π‘‹) Β· 𝑋))
125124oveq2d 7421 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) + (𝑅 Ξ£g (π‘₯ ∈ {𝑋} ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) = ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) + ((π‘Žβ€˜π‘‹) Β· 𝑋)))
1265ad3antrrr 727 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ 𝐼) β†’ 𝑅 ∈ Ring)
12720ad3antlr 728 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ 𝐼) β†’ π‘Ž:(𝐼 βˆͺ {𝑋})⟢𝐡)
128 simpr 484 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ 𝐼) β†’ π‘₯ ∈ 𝐼)
12930, 128sselid 3975 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ 𝐼) β†’ π‘₯ ∈ (𝐼 βˆͺ {𝑋}))
130127, 129ffvelcdmd 7081 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ 𝐼) β†’ (π‘Žβ€˜π‘₯) ∈ 𝐡)
1319ad3antrrr 727 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ 𝐼) β†’ 𝐼 βŠ† 𝐡)
132131, 128sseldd 3978 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ 𝐼) β†’ π‘₯ ∈ 𝐡)
1332, 4, 126, 130, 132ringcld 20162 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ 𝐼) β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) ∈ 𝐡)
134133fmpttd 7110 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)):𝐼⟢𝐡)
13530a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ 𝐼 βŠ† (𝐼 βˆͺ {𝑋}))
136135ssdifd 4135 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (𝐼 βˆ– (π‘Ž supp 0 )) βŠ† ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 )))
137136sselda 3977 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– (π‘Ž supp 0 )))
138137, 94syldan 590 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ (π‘Žβ€˜π‘₯) = 0 )
139138oveq1d 7420 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) = ( 0 Β· π‘₯))
1405ad3antrrr 727 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ 𝑅 ∈ Ring)
1419ad3antrrr 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ 𝐼 βŠ† 𝐡)
142 simpr 484 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 )))
143142eldifad 3955 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ π‘₯ ∈ 𝐼)
144141, 143sseldd 3978 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ π‘₯ ∈ 𝐡)
145140, 144, 99syl2anc 583 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ ( 0 Β· π‘₯) = 0 )
146139, 145eqtrd 2766 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ π‘₯ ∈ (𝐼 βˆ– (π‘Ž supp 0 ))) β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) = 0 )
147146, 70suppss2 8186 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ ((π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) supp 0 ) βŠ† (π‘Ž supp 0 ))
14887, 147ssfid 9269 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ ((π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) supp 0 ) ∈ Fin)
1492, 3, 69, 70, 134, 148gsumcl2 19834 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) ∈ 𝐡)
1502, 67cmncom 19718 . . . . . . . . . 10 ((𝑅 ∈ CMnd ∧ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) ∈ 𝐡 ∧ ((π‘Žβ€˜π‘‹) Β· 𝑋) ∈ 𝐡) β†’ ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) + ((π‘Žβ€˜π‘‹) Β· 𝑋)) = (((π‘Žβ€˜π‘‹) Β· 𝑋) + (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
15169, 149, 120, 150syl3anc 1368 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) + ((π‘Žβ€˜π‘‹) Β· 𝑋)) = (((π‘Žβ€˜π‘‹) Β· 𝑋) + (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
152110, 125, 1513eqtrd 2770 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) β†’ (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (((π‘Žβ€˜π‘‹) Β· 𝑋) + (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
153152adantr 480 . . . . . . 7 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (((π‘Žβ€˜π‘‹) Β· 𝑋) + (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
15466, 153eqtrd 2766 . . . . . 6 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ 𝐴 = (((π‘Žβ€˜π‘‹) Β· 𝑋) + (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
15517, 19, 26, 65, 1542rspcedvdw 3620 . . . . 5 ((((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ π‘Ž finSupp 0 ) ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) β†’ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘– ∈ 𝐼 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖))
156155anasss 466 . . . 4 (((πœ‘ ∧ π‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))) ∧ (π‘Ž finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))))) β†’ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘– ∈ 𝐼 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖))
157156r19.29an 3152 . . 3 ((πœ‘ ∧ βˆƒπ‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))(π‘Ž finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))))) β†’ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘– ∈ 𝐼 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖))
15827a1i 11 . . . . . 6 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝐡 ∈ V)
1596ad3antrrr 727 . . . . . . 7 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝐼 ∈ (LIdealβ€˜π‘…))
16071a1i 11 . . . . . . 7 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ {𝑋} ∈ V)
161159, 160unexd 7738 . . . . . 6 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝐼 βˆͺ {𝑋}) ∈ V)
162 simp-4r 781 . . . . . . . . 9 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 βˆͺ {𝑋})) β†’ π‘Ÿ ∈ 𝐡)
163 eqid 2726 . . . . . . . . . . . 12 (1rβ€˜π‘…) = (1rβ€˜π‘…)
1642, 163ringidcl 20165 . . . . . . . . . . 11 (𝑅 ∈ Ring β†’ (1rβ€˜π‘…) ∈ 𝐡)
1655, 164syl 17 . . . . . . . . . 10 (πœ‘ β†’ (1rβ€˜π‘…) ∈ 𝐡)
166165ad4antr 729 . . . . . . . . 9 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 βˆͺ {𝑋})) β†’ (1rβ€˜π‘…) ∈ 𝐡)
167162, 166ifcld 4569 . . . . . . . 8 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 βˆͺ {𝑋})) β†’ if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)) ∈ 𝐡)
16882ad4antr 729 . . . . . . . 8 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 βˆͺ {𝑋})) β†’ 0 ∈ 𝐡)
169167, 168ifcld 4569 . . . . . . 7 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 βˆͺ {𝑋})) β†’ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ) ∈ 𝐡)
170169fmpttd 7110 . . . . . 6 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )):(𝐼 βˆͺ {𝑋})⟢𝐡)
171158, 161, 170elmapdd 8837 . . . . 5 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋})))
172 breq1 5144 . . . . . . 7 (π‘Ž = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) β†’ (π‘Ž finSupp 0 ↔ (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) finSupp 0 ))
173 fveq1 6884 . . . . . . . . . . 11 (π‘Ž = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) β†’ (π‘Žβ€˜π‘₯) = ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯))
174173oveq1d 7420 . . . . . . . . . 10 (π‘Ž = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) β†’ ((π‘Žβ€˜π‘₯) Β· π‘₯) = (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))
175174mpteq2dv 5243 . . . . . . . . 9 (π‘Ž = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) β†’ (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)) = (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)))
176175oveq2d 7421 . . . . . . . 8 (π‘Ž = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) β†’ (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))))
177176eqeq2d 2737 . . . . . . 7 (π‘Ž = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) β†’ (𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯))) ↔ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)))))
178172, 177anbi12d 630 . . . . . 6 (π‘Ž = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) β†’ ((π‘Ž finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) ↔ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))))))
179178adantl 481 . . . . 5 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘Ž = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))) β†’ ((π‘Ž finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) ↔ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))))))
180 eqid 2726 . . . . . . 7 (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) = (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))
181 prfi 9324 . . . . . . . 8 {𝑋, 𝑖} ∈ Fin
182181a1i 11 . . . . . . 7 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ {𝑋, 𝑖} ∈ Fin)
183 simp-4r 781 . . . . . . . 8 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ 𝑦 ∈ {𝑋, 𝑖}) β†’ π‘Ÿ ∈ 𝐡)
184165ad4antr 729 . . . . . . . 8 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ 𝑦 ∈ {𝑋, 𝑖}) β†’ (1rβ€˜π‘…) ∈ 𝐡)
185183, 184ifcld 4569 . . . . . . 7 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ 𝑦 ∈ {𝑋, 𝑖}) β†’ if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)) ∈ 𝐡)
18682ad3antrrr 727 . . . . . . 7 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 0 ∈ 𝐡)
187180, 161, 182, 185, 186mptiffisupp 32422 . . . . . 6 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) finSupp 0 )
18868ad3antrrr 727 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝑅 ∈ CMnd)
189159, 8syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝐼 βŠ† 𝐡)
190 simplr 766 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝑖 ∈ 𝐼)
191189, 190sseldd 3978 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝑖 ∈ 𝐡)
1925ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝑅 ∈ Ring)
193 simpllr 773 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ π‘Ÿ ∈ 𝐡)
19411ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝑋 ∈ 𝐡)
1952, 4, 192, 193, 194ringcld 20162 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (π‘Ÿ Β· 𝑋) ∈ 𝐡)
1962, 67cmncom 19718 . . . . . . . . 9 ((𝑅 ∈ CMnd ∧ 𝑖 ∈ 𝐡 ∧ (π‘Ÿ Β· 𝑋) ∈ 𝐡) β†’ (𝑖 + (π‘Ÿ Β· 𝑋)) = ((π‘Ÿ Β· 𝑋) + 𝑖))
197188, 191, 195, 196syl3anc 1368 . . . . . . . 8 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑖 + (π‘Ÿ Β· 𝑋)) = ((π‘Ÿ Β· 𝑋) + 𝑖))
198188cmnmndd 19724 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝑅 ∈ Mnd)
199 eqid 2726 . . . . . . . . . . 11 (π‘₯ ∈ 𝐼 ↦ if(π‘₯ = 𝑖, 𝑖, 0 )) = (π‘₯ ∈ 𝐼 ↦ if(π‘₯ = 𝑖, 𝑖, 0 ))
200191, 2eleqtrdi 2837 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝑖 ∈ (Baseβ€˜π‘…))
2013, 198, 159, 190, 199, 200gsummptif1n0 19886 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ if(π‘₯ = 𝑖, 𝑖, 0 ))) = 𝑖)
202 fveq2 6885 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑖 β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) = ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘–))
203 id 22 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑖 β†’ π‘₯ = 𝑖)
204202, 203oveq12d 7423 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑖 β†’ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯) = (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘–) Β· 𝑖))
205204adantl 481 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯) = (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘–) Β· 𝑖))
206 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ 𝑦 = 𝑖)
207 prid2g 4760 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ 𝐼 β†’ 𝑖 ∈ {𝑋, 𝑖})
208207ad5antlr 732 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ 𝑖 ∈ {𝑋, 𝑖})
209206, 208eqeltrd 2827 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ 𝑦 ∈ {𝑋, 𝑖})
210209iftrued 4531 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ) = if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)))
211190ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ 𝑖 ∈ 𝐼)
212211adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ 𝑖 ∈ 𝐼)
213206, 212eqeltrd 2827 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ 𝑦 ∈ 𝐼)
214105ad3antrrr 727 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ Β¬ 𝑋 ∈ 𝐼)
215214ad3antrrr 727 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ Β¬ 𝑋 ∈ 𝐼)
216 nelneq 2851 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ 𝐼 ∧ Β¬ 𝑋 ∈ 𝐼) β†’ Β¬ 𝑦 = 𝑋)
217213, 215, 216syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ Β¬ 𝑦 = 𝑋)
218217iffalsed 4534 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)) = (1rβ€˜π‘…))
219210, 218eqtrd 2766 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) ∧ 𝑦 = 𝑖) β†’ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ) = (1rβ€˜π‘…))
22030, 211sselid 3975 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ 𝑖 ∈ (𝐼 βˆͺ {𝑋}))
221192ad2antrr 723 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ 𝑅 ∈ Ring)
222221, 164syl 17 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ (1rβ€˜π‘…) ∈ 𝐡)
223180, 219, 220, 222fvmptd2 7000 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘–) = (1rβ€˜π‘…))
224223oveq1d 7420 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘–) Β· 𝑖) = ((1rβ€˜π‘…) Β· 𝑖))
225191ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ 𝑖 ∈ 𝐡)
2262, 4, 163, 221, 225ringlidmd 20171 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ ((1rβ€˜π‘…) Β· 𝑖) = 𝑖)
227205, 224, 2263eqtrrd 2771 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ π‘₯ = 𝑖) β†’ 𝑖 = (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))
228 eleq1w 2810 . . . . . . . . . . . . . . . . . 18 (𝑦 = π‘₯ β†’ (𝑦 ∈ {𝑋, 𝑖} ↔ π‘₯ ∈ {𝑋, 𝑖}))
229 eqeq1 2730 . . . . . . . . . . . . . . . . . . 19 (𝑦 = π‘₯ β†’ (𝑦 = 𝑋 ↔ π‘₯ = 𝑋))
230229ifbid 4546 . . . . . . . . . . . . . . . . . 18 (𝑦 = π‘₯ β†’ if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)) = if(π‘₯ = 𝑋, π‘Ÿ, (1rβ€˜π‘…)))
231228, 230ifbieq1d 4547 . . . . . . . . . . . . . . . . 17 (𝑦 = π‘₯ β†’ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ) = if(π‘₯ ∈ {𝑋, 𝑖}, if(π‘₯ = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))
232 simplr 766 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ π‘₯ ∈ 𝐼)
23330, 232sselid 3975 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ π‘₯ ∈ (𝐼 βˆͺ {𝑋}))
234193ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ π‘Ÿ ∈ 𝐡)
235165ad5antr 731 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ (1rβ€˜π‘…) ∈ 𝐡)
236234, 235ifcld 4569 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ if(π‘₯ = 𝑋, π‘Ÿ, (1rβ€˜π‘…)) ∈ 𝐡)
237186ad2antrr 723 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ 0 ∈ 𝐡)
238236, 237ifcld 4569 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ if(π‘₯ ∈ {𝑋, 𝑖}, if(π‘₯ = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ) ∈ 𝐡)
239180, 231, 233, 238fvmptd3 7015 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) = if(π‘₯ ∈ {𝑋, 𝑖}, if(π‘₯ = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))
240214ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ Β¬ 𝑋 ∈ 𝐼)
241 nelne2 3034 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ 𝐼 ∧ Β¬ 𝑋 ∈ 𝐼) β†’ π‘₯ β‰  𝑋)
242232, 240, 241syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ π‘₯ β‰  𝑋)
243 neqne 2942 . . . . . . . . . . . . . . . . . . 19 (Β¬ π‘₯ = 𝑖 β†’ π‘₯ β‰  𝑖)
244243adantl 481 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ π‘₯ β‰  𝑖)
245242, 244nelprd 4654 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ Β¬ π‘₯ ∈ {𝑋, 𝑖})
246245iffalsed 4534 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ if(π‘₯ ∈ {𝑋, 𝑖}, if(π‘₯ = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ) = 0 )
247239, 246eqtrd 2766 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) = 0 )
248247oveq1d 7420 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯) = ( 0 Β· π‘₯))
249192ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ 𝑅 ∈ Ring)
250189ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ 𝐼 βŠ† 𝐡)
251250, 232sseldd 3978 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ π‘₯ ∈ 𝐡)
252249, 251, 99syl2anc 583 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ ( 0 Β· π‘₯) = 0 )
253248, 252eqtr2d 2767 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) ∧ Β¬ π‘₯ = 𝑖) β†’ 0 = (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))
254227, 253ifeqda 4559 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ 𝐼) β†’ if(π‘₯ = 𝑖, 𝑖, 0 ) = (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))
255254mpteq2dva 5241 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (π‘₯ ∈ 𝐼 ↦ if(π‘₯ = 𝑖, 𝑖, 0 )) = (π‘₯ ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)))
256255oveq2d 7421 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ if(π‘₯ = 𝑖, 𝑖, 0 ))) = (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))))
257201, 256eqtr3d 2768 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝑖 = (𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))))
258 simpr 484 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ 𝑦 = π‘₯)
259 simplr 766 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ π‘₯ = 𝑋)
260194ad2antrr 723 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ 𝑋 ∈ 𝐡)
261 prid1g 4759 . . . . . . . . . . . . . . . . . 18 (𝑋 ∈ 𝐡 β†’ 𝑋 ∈ {𝑋, 𝑖})
262260, 261syl 17 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ 𝑋 ∈ {𝑋, 𝑖})
263259, 262eqeltrd 2827 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ π‘₯ ∈ {𝑋, 𝑖})
264258, 263eqeltrd 2827 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ 𝑦 ∈ {𝑋, 𝑖})
265264iftrued 4531 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ) = if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)))
266258, 259eqtrd 2766 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ 𝑦 = 𝑋)
267266iftrued 4531 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)) = π‘Ÿ)
268265, 267eqtrd 2766 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) ∧ 𝑦 = π‘₯) β†’ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ) = π‘Ÿ)
269 simpr 484 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) β†’ π‘₯ = 𝑋)
270116ad4antr 729 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) β†’ 𝑋 ∈ {𝑋})
271270, 24syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) β†’ 𝑋 ∈ (𝐼 βˆͺ {𝑋}))
272269, 271eqeltrd 2827 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) β†’ π‘₯ ∈ (𝐼 βˆͺ {𝑋}))
273193adantr 480 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) β†’ π‘Ÿ ∈ 𝐡)
274180, 268, 272, 273fvmptd2 7000 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) = π‘Ÿ)
275274, 269oveq12d 7423 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ = 𝑋) β†’ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯) = (π‘Ÿ Β· 𝑋))
2762, 198, 194, 195, 275gsumsnd 19872 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑅 Ξ£g (π‘₯ ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))) = (π‘Ÿ Β· 𝑋))
277276eqcomd 2732 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (π‘Ÿ Β· 𝑋) = (𝑅 Ξ£g (π‘₯ ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))))
278257, 277oveq12d 7423 . . . . . . . 8 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑖 + (π‘Ÿ Β· 𝑋)) = ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))) + (𝑅 Ξ£g (π‘₯ ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)))))
279197, 278eqtr3d 2768 . . . . . . 7 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ ((π‘Ÿ Β· 𝑋) + 𝑖) = ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))) + (𝑅 Ξ£g (π‘₯ ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)))))
280 simpr 484 . . . . . . 7 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖))
2815ad4antr 729 . . . . . . . . 9 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ 𝑅 ∈ Ring)
282170ffvelcdmda 7080 . . . . . . . . 9 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) ∈ 𝐡)
28313ad4antr 729 . . . . . . . . . 10 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ (𝐼 βˆͺ {𝑋}) βŠ† 𝐡)
284 simpr 484 . . . . . . . . . 10 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ π‘₯ ∈ (𝐼 βˆͺ {𝑋}))
285283, 284sseldd 3978 . . . . . . . . 9 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ π‘₯ ∈ 𝐡)
2862, 4, 281, 282, 285ringcld 20162 . . . . . . . 8 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ (𝐼 βˆͺ {𝑋})) β†’ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯) ∈ 𝐡)
287161mptexd 7221 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)) ∈ V)
288 funmpt 6580 . . . . . . . . . 10 Fun (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))
289288a1i 11 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ Fun (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)))
290187fsuppimpd 9371 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ) ∈ Fin)
291 nfv 1909 . . . . . . . . . . . . . . . 16 Ⅎ𝑦(((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖))
292291, 169, 180fnmptd 6685 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) Fn (𝐼 βˆͺ {𝑋}))
293292adantr 480 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ (𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) Fn (𝐼 βˆͺ {𝑋}))
294161adantr 480 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ (𝐼 βˆͺ {𝑋}) ∈ V)
295186adantr 480 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ 0 ∈ 𝐡)
296 simpr 484 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 )))
297293, 294, 295, 296fvdifsupp 32414 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) = 0 )
298297oveq1d 7420 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯) = ( 0 Β· π‘₯))
2995ad4antr 729 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ 𝑅 ∈ Ring)
30013ad4antr 729 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ (𝐼 βˆͺ {𝑋}) βŠ† 𝐡)
301296eldifad 3955 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ π‘₯ ∈ (𝐼 βˆͺ {𝑋}))
302300, 301sseldd 3978 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ π‘₯ ∈ 𝐡)
303299, 302, 99syl2anc 583 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ ( 0 Β· π‘₯) = 0 )
304298, 303eqtrd 2766 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) ∧ π‘₯ ∈ ((𝐼 βˆͺ {𝑋}) βˆ– ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))) β†’ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯) = 0 )
305304, 161suppss2 8186 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ ((π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)) supp 0 ) βŠ† ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) supp 0 ))
306290, 305ssfid 9269 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ ((π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)) supp 0 ) ∈ Fin)
307287, 186, 289, 306isfsuppd 9368 . . . . . . . 8 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)) finSupp 0 )
308214, 107sylibr 233 . . . . . . . 8 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝐼 ∩ {𝑋}) = βˆ…)
309 eqidd 2727 . . . . . . . 8 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝐼 βˆͺ {𝑋}) = (𝐼 βˆͺ {𝑋}))
3102, 3, 67, 188, 161, 286, 307, 308, 309gsumsplit2 19849 . . . . . . 7 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))) = ((𝑅 Ξ£g (π‘₯ ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))) + (𝑅 Ξ£g (π‘₯ ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)))))
311279, 280, 3103eqtr4d 2776 . . . . . 6 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯))))
312187, 311jca 511 . . . . 5 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ ((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 )) finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ (((𝑦 ∈ (𝐼 βˆͺ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, π‘Ÿ, (1rβ€˜π‘…)), 0 ))β€˜π‘₯) Β· π‘₯)))))
313171, 179, 312rspcedvd 3608 . . . 4 ((((πœ‘ ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ βˆƒπ‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))(π‘Ž finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
314313r19.29ffa 32222 . . 3 ((πœ‘ ∧ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘– ∈ 𝐼 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)) β†’ βˆƒπ‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))(π‘Ž finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))))
315157, 314impbida 798 . 2 (πœ‘ β†’ (βˆƒπ‘Ž ∈ (𝐡 ↑m (𝐼 βˆͺ {𝑋}))(π‘Ž finSupp 0 ∧ 𝐴 = (𝑅 Ξ£g (π‘₯ ∈ (𝐼 βˆͺ {𝑋}) ↦ ((π‘Žβ€˜π‘₯) Β· π‘₯)))) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘– ∈ 𝐼 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)))
31614, 315bitrd 279 1 (πœ‘ β†’ (𝐴 ∈ (π‘β€˜(𝐼 βˆͺ {𝑋})) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘– ∈ 𝐼 𝐴 = ((π‘Ÿ Β· 𝑋) + 𝑖)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆƒwrex 3064  Vcvv 3468   βˆ– cdif 3940   βˆͺ cun 3941   ∩ cin 3942   βŠ† wss 3943  βˆ…c0 4317  ifcif 4523  {csn 4623  {cpr 4625   class class class wbr 5141   ↦ cmpt 5224   β†Ύ cres 5671  Fun wfun 6531   Fn wfn 6532  βŸΆwf 6533  β€˜cfv 6537  (class class class)co 7405   supp csupp 8146   ↑m cmap 8822  Fincfn 8941   finSupp cfsupp 9363  Basecbs 17153  +gcplusg 17206  .rcmulr 17207  0gc0g 17394   Ξ£g cgsu 17395  CMndccmn 19700  1rcur 20086  Ringcrg 20138  LIdealclidl 21065  RSpancrsp 21066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-fz 13491  df-fzo 13634  df-seq 13973  df-hash 14296  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-hom 17230  df-cco 17231  df-0g 17396  df-gsum 17397  df-prds 17402  df-pws 17404  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-mhm 18713  df-submnd 18714  df-grp 18866  df-minusg 18867  df-sbg 18868  df-mulg 18996  df-subg 19050  df-ghm 19139  df-cntz 19233  df-cmn 19702  df-abl 19703  df-mgp 20040  df-rng 20058  df-ur 20087  df-ring 20140  df-nzr 20415  df-subrg 20471  df-lmod 20708  df-lss 20779  df-lsp 20819  df-lmhm 20870  df-lbs 20923  df-sra 21021  df-rgmod 21022  df-lidl 21067  df-rsp 21068  df-dsmm 21627  df-frlm 21642  df-uvc 21678
This theorem is referenced by:  qsdrngilem  33114
  Copyright terms: Public domain W3C validator