| Step | Hyp | Ref | 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 2736 | . . . . . 6
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) | 
| 8 | 2, 7 | lidlss 21223 | . . . . 5
⊢ (𝐼 ∈ (LIdeal‘𝑅) → 𝐼 ⊆ 𝐵) | 
| 9 | 6, 8 | syl 17 | . . . 4
⊢ (𝜑 → 𝐼 ⊆ 𝐵) | 
| 10 |  | elrspunsn.x | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝐼)) | 
| 11 | 10 | eldifad 3962 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 12 | 11 | snssd 4808 | . . . 4
⊢ (𝜑 → {𝑋} ⊆ 𝐵) | 
| 13 | 9, 12 | unssd 4191 | . . 3
⊢ (𝜑 → (𝐼 ∪ {𝑋}) ⊆ 𝐵) | 
| 14 | 1, 2, 3, 4, 5, 13 | elrsp 33401 | . 2
⊢ (𝜑 → (𝐴 ∈ (𝑁‘(𝐼 ∪ {𝑋})) ↔ ∃𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))(𝑎 finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))))) | 
| 15 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑟 = (𝑎‘𝑋) → (𝑟 · 𝑋) = ((𝑎‘𝑋) · 𝑋)) | 
| 16 | 15 | oveq1d 7447 | . . . . . . 7
⊢ (𝑟 = (𝑎‘𝑋) → ((𝑟 · 𝑋) + 𝑖) = (((𝑎‘𝑋) · 𝑋) + 𝑖)) | 
| 17 | 16 | eqeq2d 2747 | . . . . . 6
⊢ (𝑟 = (𝑎‘𝑋) → (𝐴 = ((𝑟 · 𝑋) + 𝑖) ↔ 𝐴 = (((𝑎‘𝑋) · 𝑋) + 𝑖))) | 
| 18 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑖 = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) → (((𝑎‘𝑋) · 𝑋) + 𝑖) = (((𝑎‘𝑋) · 𝑋) + (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 19 | 18 | eqeq2d 2747 | . . . . . 6
⊢ (𝑖 = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) → (𝐴 = (((𝑎‘𝑋) · 𝑋) + 𝑖) ↔ 𝐴 = (((𝑎‘𝑋) · 𝑋) + (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥)))))) | 
| 20 |  | elmapi 8890 | . . . . . . . 8
⊢ (𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋})) → 𝑎:(𝐼 ∪ {𝑋})⟶𝐵) | 
| 21 | 20 | ad3antlr 731 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝑎:(𝐼 ∪ {𝑋})⟶𝐵) | 
| 22 | 11 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝑋 ∈ 𝐵) | 
| 23 |  | snidg 4659 | . . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ {𝑋}) | 
| 24 |  | elun2 4182 | . . . . . . . 8
⊢ (𝑋 ∈ {𝑋} → 𝑋 ∈ (𝐼 ∪ {𝑋})) | 
| 25 | 22, 23, 24 | 3syl 18 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝑋 ∈ (𝐼 ∪ {𝑋})) | 
| 26 | 21, 25 | ffvelcdmd 7104 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑎‘𝑋) ∈ 𝐵) | 
| 27 | 2 | fvexi 6919 | . . . . . . . . . . 11
⊢ 𝐵 ∈ V | 
| 28 | 27 | a1i 11 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝐵 ∈ V) | 
| 29 | 6 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 30 |  | ssun1 4177 | . . . . . . . . . . . 12
⊢ 𝐼 ⊆ (𝐼 ∪ {𝑋}) | 
| 31 | 30 | a1i 11 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝐼 ⊆ (𝐼 ∪ {𝑋})) | 
| 32 | 21, 31 | fssresd 6774 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑎 ↾ 𝐼):𝐼⟶𝐵) | 
| 33 | 28, 29, 32 | elmapdd 8882 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑎 ↾ 𝐼) ∈ (𝐵 ↑m 𝐼)) | 
| 34 |  | breq1 5145 | . . . . . . . . . . 11
⊢ (𝑏 = (𝑎 ↾ 𝐼) → (𝑏 finSupp 0 ↔ (𝑎 ↾ 𝐼) finSupp 0 )) | 
| 35 |  | fveq1 6904 | . . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑎 ↾ 𝐼) → (𝑏‘𝑦) = ((𝑎 ↾ 𝐼)‘𝑦)) | 
| 36 | 35 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑎 ↾ 𝐼) → ((𝑏‘𝑦) · 𝑦) = (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦)) | 
| 37 | 36 | mpteq2dv 5243 | . . . . . . . . . . . . 13
⊢ (𝑏 = (𝑎 ↾ 𝐼) → (𝑦 ∈ 𝐼 ↦ ((𝑏‘𝑦) · 𝑦)) = (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦))) | 
| 38 | 37 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑏 = (𝑎 ↾ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐼 ↦ ((𝑏‘𝑦) · 𝑦))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦)))) | 
| 39 | 38 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑏 = (𝑎 ↾ 𝐼) → ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ ((𝑏‘𝑦) · 𝑦))) ↔ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦))))) | 
| 40 | 34, 39 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑏 = (𝑎 ↾ 𝐼) → ((𝑏 finSupp 0 ∧ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ ((𝑏‘𝑦) · 𝑦)))) ↔ ((𝑎 ↾ 𝐼) finSupp 0 ∧ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦)))))) | 
| 41 | 40 | adantl 481 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) ∧ 𝑏 = (𝑎 ↾ 𝐼)) → ((𝑏 finSupp 0 ∧ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ ((𝑏‘𝑦) · 𝑦)))) ↔ ((𝑎 ↾ 𝐼) finSupp 0 ∧ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦)))))) | 
| 42 |  | simplr 768 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝑎 finSupp 0 ) | 
| 43 | 5 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝑅 ∈ Ring) | 
| 44 | 2, 3 | ring0cl 20265 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) | 
| 45 | 43, 44 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 0 ∈ 𝐵) | 
| 46 | 42, 45 | fsuppres 9434 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑎 ↾ 𝐼) finSupp 0 ) | 
| 47 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑎‘𝑥) = (𝑎‘𝑦)) | 
| 48 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) | 
| 49 | 47, 48 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑎‘𝑥) · 𝑥) = ((𝑎‘𝑦) · 𝑦)) | 
| 50 | 49 | cbvmptv 5254 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥)) = (𝑦 ∈ 𝐼 ↦ ((𝑎‘𝑦) · 𝑦)) | 
| 51 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) | 
| 52 | 51 | fvresd 6925 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) ∧ 𝑦 ∈ 𝐼) → ((𝑎 ↾ 𝐼)‘𝑦) = (𝑎‘𝑦)) | 
| 53 | 52 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) ∧ 𝑦 ∈ 𝐼) → (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦) = ((𝑎‘𝑦) · 𝑦)) | 
| 54 | 53 | mpteq2dva 5241 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦)) = (𝑦 ∈ 𝐼 ↦ ((𝑎‘𝑦) · 𝑦))) | 
| 55 | 50, 54 | eqtr4id 2795 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥)) = (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦))) | 
| 56 | 55 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦)))) | 
| 57 | 46, 56 | jca 511 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → ((𝑎 ↾ 𝐼) finSupp 0 ∧ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ (((𝑎 ↾ 𝐼)‘𝑦) · 𝑦))))) | 
| 58 | 33, 41, 57 | rspcedvd 3623 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → ∃𝑏 ∈ (𝐵 ↑m 𝐼)(𝑏 finSupp 0 ∧ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ ((𝑏‘𝑦) · 𝑦))))) | 
| 59 | 9 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝐼 ⊆ 𝐵) | 
| 60 | 1, 2, 3, 4, 43, 59 | elrsp 33401 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) ∈ (𝑁‘𝐼) ↔ ∃𝑏 ∈ (𝐵 ↑m 𝐼)(𝑏 finSupp 0 ∧ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐼 ↦ ((𝑏‘𝑦) · 𝑦)))))) | 
| 61 | 58, 60 | mpbird 257 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) ∈ (𝑁‘𝐼)) | 
| 62 | 1, 7 | rspidlid 33404 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑁‘𝐼) = 𝐼) | 
| 63 | 5, 6, 62 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑁‘𝐼) = 𝐼) | 
| 64 | 63 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑁‘𝐼) = 𝐼) | 
| 65 | 61, 64 | eleqtrd 2842 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) ∈ 𝐼) | 
| 66 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) | 
| 67 |  | elrspunsn.p | . . . . . . . . . 10
⊢  + =
(+g‘𝑅) | 
| 68 | 5 | ringcmnd 20282 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ CMnd) | 
| 69 | 68 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝑅 ∈ CMnd) | 
| 70 | 6 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 71 |  | snex 5435 | . . . . . . . . . . . 12
⊢ {𝑋} ∈ V | 
| 72 | 71 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → {𝑋} ∈ V) | 
| 73 | 70, 72 | unexd 7775 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝐼 ∪ {𝑋}) ∈ V) | 
| 74 | 5 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → 𝑅 ∈ Ring) | 
| 75 | 20 | ad3antlr 731 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → 𝑎:(𝐼 ∪ {𝑋})⟶𝐵) | 
| 76 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → 𝑥 ∈ (𝐼 ∪ {𝑋})) | 
| 77 | 75, 76 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → (𝑎‘𝑥) ∈ 𝐵) | 
| 78 | 13 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → (𝐼 ∪ {𝑋}) ⊆ 𝐵) | 
| 79 | 78, 76 | sseldd 3983 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → 𝑥 ∈ 𝐵) | 
| 80 | 2, 4, 74, 77, 79 | ringcld 20258 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → ((𝑎‘𝑥) · 𝑥) ∈ 𝐵) | 
| 81 | 73 | mptexd 7245 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)) ∈ V) | 
| 82 | 5, 44 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ 𝐵) | 
| 83 | 82 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 0 ∈ 𝐵) | 
| 84 |  | funmpt 6603 | . . . . . . . . . . . 12
⊢ Fun
(𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)) | 
| 85 | 84 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → Fun (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))) | 
| 86 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝑎 finSupp 0 ) | 
| 87 | 86 | fsuppimpd 9410 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑎 supp 0 ) ∈
Fin) | 
| 88 | 20 | ad3antlr 731 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → 𝑎:(𝐼 ∪ {𝑋})⟶𝐵) | 
| 89 | 88 | ffnd 6736 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → 𝑎 Fn (𝐼 ∪ {𝑋})) | 
| 90 | 73 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → (𝐼 ∪ {𝑋}) ∈ V) | 
| 91 | 5 | ad3antrrr 730 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → 𝑅 ∈ Ring) | 
| 92 | 91, 44 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → 0 ∈ 𝐵) | 
| 93 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) | 
| 94 | 89, 90, 92, 93 | fvdifsupp 8197 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → (𝑎‘𝑥) = 0 ) | 
| 95 | 94 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → ((𝑎‘𝑥) · 𝑥) = ( 0 · 𝑥)) | 
| 96 | 13 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → (𝐼 ∪ {𝑋}) ⊆ 𝐵) | 
| 97 | 93 | eldifad 3962 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → 𝑥 ∈ (𝐼 ∪ {𝑋})) | 
| 98 | 96, 97 | sseldd 3983 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → 𝑥 ∈ 𝐵) | 
| 99 | 2, 4, 3 | ringlz 20291 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → ( 0 · 𝑥) = 0 ) | 
| 100 | 91, 98, 99 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → ( 0 · 𝑥) = 0 ) | 
| 101 | 95, 100 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) → ((𝑎‘𝑥) · 𝑥) = 0 ) | 
| 102 | 101, 73 | suppss2 8226 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → ((𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)) supp 0 ) ⊆ (𝑎 supp 0 )) | 
| 103 | 87, 102 | ssfid 9302 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → ((𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)) supp 0 ) ∈
Fin) | 
| 104 | 81, 83, 85, 103 | isfsuppd 9407 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)) finSupp 0 ) | 
| 105 | 10 | eldifbd 3963 | . . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑋 ∈ 𝐼) | 
| 106 | 105 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → ¬ 𝑋 ∈ 𝐼) | 
| 107 |  | disjsn 4710 | . . . . . . . . . . 11
⊢ ((𝐼 ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ 𝐼) | 
| 108 | 106, 107 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝐼 ∩ {𝑋}) = ∅) | 
| 109 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝐼 ∪ {𝑋}) = (𝐼 ∪ {𝑋})) | 
| 110 | 2, 3, 67, 69, 73, 80, 104, 108, 109 | gsumsplit2 19948 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑅 Σg
(𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) + (𝑅 Σg (𝑥 ∈ {𝑋} ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 111 | 69 | cmnmndd 19823 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝑅 ∈ Mnd) | 
| 112 | 11 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝑋 ∈ 𝐵) | 
| 113 | 5 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝑅 ∈ Ring) | 
| 114 | 20 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝑎:(𝐼 ∪ {𝑋})⟶𝐵) | 
| 115 |  | ssun2 4178 | . . . . . . . . . . . . . 14
⊢ {𝑋} ⊆ (𝐼 ∪ {𝑋}) | 
| 116 | 11, 23 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ {𝑋}) | 
| 117 | 116 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝑋 ∈ {𝑋}) | 
| 118 | 115, 117 | sselid 3980 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝑋 ∈ (𝐼 ∪ {𝑋})) | 
| 119 | 114, 118 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑎‘𝑋) ∈ 𝐵) | 
| 120 | 2, 4, 113, 119, 112 | ringcld 20258 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → ((𝑎‘𝑋) · 𝑋) ∈ 𝐵) | 
| 121 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) | 
| 122 | 121 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 = 𝑋) → (𝑎‘𝑥) = (𝑎‘𝑋)) | 
| 123 | 122, 121 | oveq12d 7450 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 = 𝑋) → ((𝑎‘𝑥) · 𝑥) = ((𝑎‘𝑋) · 𝑋)) | 
| 124 | 2, 111, 112, 120, 123 | gsumsnd 19971 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑅 Σg
(𝑥 ∈ {𝑋} ↦ ((𝑎‘𝑥) · 𝑥))) = ((𝑎‘𝑋) · 𝑋)) | 
| 125 | 124 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → ((𝑅 Σg
(𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) + (𝑅 Σg (𝑥 ∈ {𝑋} ↦ ((𝑎‘𝑥) · 𝑥)))) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) + ((𝑎‘𝑋) · 𝑋))) | 
| 126 | 5 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) | 
| 127 | 20 | ad3antlr 731 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑎:(𝐼 ∪ {𝑋})⟶𝐵) | 
| 128 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) | 
| 129 | 30, 128 | sselid 3980 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ (𝐼 ∪ {𝑋})) | 
| 130 | 127, 129 | ffvelcdmd 7104 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝐵) | 
| 131 | 9 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼) → 𝐼 ⊆ 𝐵) | 
| 132 | 131, 128 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐵) | 
| 133 | 2, 4, 126, 130, 132 | ringcld 20258 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥) · 𝑥) ∈ 𝐵) | 
| 134 | 133 | fmpttd 7134 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥)):𝐼⟶𝐵) | 
| 135 | 30 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → 𝐼 ⊆ (𝐼 ∪ {𝑋})) | 
| 136 | 135 | ssdifd 4144 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝐼 ∖ (𝑎 supp 0 )) ⊆ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) | 
| 137 | 136 | sselda 3982 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ (𝑎 supp 0 ))) | 
| 138 | 137, 94 | syldan 591 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → (𝑎‘𝑥) = 0 ) | 
| 139 | 138 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → ((𝑎‘𝑥) · 𝑥) = ( 0 · 𝑥)) | 
| 140 | 5 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → 𝑅 ∈ Ring) | 
| 141 | 9 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → 𝐼 ⊆ 𝐵) | 
| 142 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) | 
| 143 | 142 | eldifad 3962 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → 𝑥 ∈ 𝐼) | 
| 144 | 141, 143 | sseldd 3983 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → 𝑥 ∈ 𝐵) | 
| 145 | 140, 144,
99 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → ( 0 · 𝑥) = 0 ) | 
| 146 | 139, 145 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝑥 ∈ (𝐼 ∖ (𝑎 supp 0 ))) → ((𝑎‘𝑥) · 𝑥) = 0 ) | 
| 147 | 146, 70 | suppss2 8226 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → ((𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥)) supp 0 ) ⊆ (𝑎 supp 0 )) | 
| 148 | 87, 147 | ssfid 9302 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → ((𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥)) supp 0 ) ∈
Fin) | 
| 149 | 2, 3, 69, 70, 134, 148 | gsumcl2 19933 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑅 Σg
(𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) ∈ 𝐵) | 
| 150 | 2, 67 | cmncom 19817 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CMnd ∧ (𝑅 Σg
(𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) ∈ 𝐵 ∧ ((𝑎‘𝑋) · 𝑋) ∈ 𝐵) → ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) + ((𝑎‘𝑋) · 𝑋)) = (((𝑎‘𝑋) · 𝑋) + (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 151 | 69, 149, 120, 150 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → ((𝑅 Σg
(𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))) + ((𝑎‘𝑋) · 𝑋)) = (((𝑎‘𝑋) · 𝑋) + (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 152 | 110, 125,
151 | 3eqtrd 2780 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) → (𝑅 Σg
(𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))) = (((𝑎‘𝑋) · 𝑋) + (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 153 | 152 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))) = (((𝑎‘𝑋) · 𝑋) + (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 154 | 66, 153 | eqtrd 2776 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → 𝐴 = (((𝑎‘𝑋) · 𝑋) + (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 155 | 17, 19, 26, 65, 154 | 2rspcedvdw 3635 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ 𝑎 finSupp 0 ) ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) → ∃𝑟 ∈ 𝐵 ∃𝑖 ∈ 𝐼 𝐴 = ((𝑟 · 𝑋) + 𝑖)) | 
| 156 | 155 | anasss 466 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) ∧ (𝑎 finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))))) → ∃𝑟 ∈ 𝐵 ∃𝑖 ∈ 𝐼 𝐴 = ((𝑟 · 𝑋) + 𝑖)) | 
| 157 | 156 | r19.29an 3157 | . . 3
⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))(𝑎 finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))))) → ∃𝑟 ∈ 𝐵 ∃𝑖 ∈ 𝐼 𝐴 = ((𝑟 · 𝑋) + 𝑖)) | 
| 158 | 27 | a1i 11 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝐵 ∈ V) | 
| 159 | 6 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 160 | 71 | a1i 11 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → {𝑋} ∈ V) | 
| 161 | 159, 160 | unexd 7775 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝐼 ∪ {𝑋}) ∈ V) | 
| 162 |  | simp-4r 783 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 ∪ {𝑋})) → 𝑟 ∈ 𝐵) | 
| 163 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 164 | 2, 163 | ringidcl 20263 | . . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) | 
| 165 | 5, 164 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) | 
| 166 | 165 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 ∪ {𝑋})) → (1r‘𝑅) ∈ 𝐵) | 
| 167 | 162, 166 | ifcld 4571 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 ∪ {𝑋})) → if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)) ∈ 𝐵) | 
| 168 | 82 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 ∪ {𝑋})) → 0 ∈ 𝐵) | 
| 169 | 167, 168 | ifcld 4571 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑦 ∈ (𝐼 ∪ {𝑋})) → if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ) ∈ 𝐵) | 
| 170 | 169 | fmpttd 7134 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )):(𝐼 ∪ {𝑋})⟶𝐵) | 
| 171 | 158, 161,
170 | elmapdd 8882 | . . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))) | 
| 172 |  | breq1 5145 | . . . . . . 7
⊢ (𝑎 = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) → (𝑎 finSupp 0 ↔ (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) finSupp 0
)) | 
| 173 |  | fveq1 6904 | . . . . . . . . . . 11
⊢ (𝑎 = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) → (𝑎‘𝑥) = ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥)) | 
| 174 | 173 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑎 = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) → ((𝑎‘𝑥) · 𝑥) = (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) | 
| 175 | 174 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝑎 = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) → (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)) = (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))) | 
| 176 | 175 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑎 = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) → (𝑅 Σg
(𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))) = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)))) | 
| 177 | 176 | eqeq2d 2747 | . . . . . . 7
⊢ (𝑎 = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) → (𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))) ↔ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))))) | 
| 178 | 172, 177 | anbi12d 632 | . . . . . 6
⊢ (𝑎 = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) → ((𝑎 finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) ↔ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)))))) | 
| 179 | 178 | adantl 481 | . . . . 5
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑎 = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))) → ((𝑎 finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) ↔ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)))))) | 
| 180 |  | eqid 2736 | . . . . . . 7
⊢ (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) = (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) | 
| 181 |  | prfi 9364 | . . . . . . . 8
⊢ {𝑋, 𝑖} ∈ Fin | 
| 182 | 181 | a1i 11 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → {𝑋, 𝑖} ∈ Fin) | 
| 183 |  | simp-4r 783 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑦 ∈ {𝑋, 𝑖}) → 𝑟 ∈ 𝐵) | 
| 184 | 165 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑦 ∈ {𝑋, 𝑖}) → (1r‘𝑅) ∈ 𝐵) | 
| 185 | 183, 184 | ifcld 4571 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑦 ∈ {𝑋, 𝑖}) → if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)) ∈ 𝐵) | 
| 186 | 82 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 0 ∈ 𝐵) | 
| 187 | 180, 161,
182, 185, 186 | mptiffisupp 32703 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) finSupp 0
) | 
| 188 | 68 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑅 ∈ CMnd) | 
| 189 | 159, 8 | syl 17 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝐼 ⊆ 𝐵) | 
| 190 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑖 ∈ 𝐼) | 
| 191 | 189, 190 | sseldd 3983 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑖 ∈ 𝐵) | 
| 192 | 5 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑅 ∈ Ring) | 
| 193 |  | simpllr 775 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑟 ∈ 𝐵) | 
| 194 | 11 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑋 ∈ 𝐵) | 
| 195 | 2, 4, 192, 193, 194 | ringcld 20258 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑟 · 𝑋) ∈ 𝐵) | 
| 196 | 2, 67 | cmncom 19817 | . . . . . . . . 9
⊢ ((𝑅 ∈ CMnd ∧ 𝑖 ∈ 𝐵 ∧ (𝑟 · 𝑋) ∈ 𝐵) → (𝑖 + (𝑟 · 𝑋)) = ((𝑟 · 𝑋) + 𝑖)) | 
| 197 | 188, 191,
195, 196 | syl3anc 1372 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑖 + (𝑟 · 𝑋)) = ((𝑟 · 𝑋) + 𝑖)) | 
| 198 | 188 | cmnmndd 19823 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑅 ∈ Mnd) | 
| 199 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑖, 𝑖, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑖, 𝑖, 0 )) | 
| 200 | 191, 2 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑖 ∈ (Base‘𝑅)) | 
| 201 | 3, 198, 159, 190, 199, 200 | gsummptif1n0 19985 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑖, 𝑖, 0 ))) = 𝑖) | 
| 202 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑖 → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) = ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑖)) | 
| 203 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑖 → 𝑥 = 𝑖) | 
| 204 | 202, 203 | oveq12d 7450 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑖 → (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥) = (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑖) · 𝑖)) | 
| 205 | 204 | adantl 481 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥) = (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑖) · 𝑖)) | 
| 206 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → 𝑦 = 𝑖) | 
| 207 |  | prid2g 4760 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ 𝐼 → 𝑖 ∈ {𝑋, 𝑖}) | 
| 208 | 207 | ad5antlr 735 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → 𝑖 ∈ {𝑋, 𝑖}) | 
| 209 | 206, 208 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → 𝑦 ∈ {𝑋, 𝑖}) | 
| 210 | 209 | iftrued 4532 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ) = if(𝑦 = 𝑋, 𝑟, (1r‘𝑅))) | 
| 211 | 190 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → 𝑖 ∈ 𝐼) | 
| 212 | 211 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → 𝑖 ∈ 𝐼) | 
| 213 | 206, 212 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → 𝑦 ∈ 𝐼) | 
| 214 | 105 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → ¬ 𝑋 ∈ 𝐼) | 
| 215 | 214 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → ¬ 𝑋 ∈ 𝐼) | 
| 216 |  | nelneq 2864 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ 𝐼 ∧ ¬ 𝑋 ∈ 𝐼) → ¬ 𝑦 = 𝑋) | 
| 217 | 213, 215,
216 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → ¬ 𝑦 = 𝑋) | 
| 218 | 217 | iffalsed 4535 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)) = (1r‘𝑅)) | 
| 219 | 210, 218 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) ∧ 𝑦 = 𝑖) → if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ) =
(1r‘𝑅)) | 
| 220 | 30, 211 | sselid 3980 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → 𝑖 ∈ (𝐼 ∪ {𝑋})) | 
| 221 | 192 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → 𝑅 ∈ Ring) | 
| 222 | 221, 164 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → (1r‘𝑅) ∈ 𝐵) | 
| 223 | 180, 219,
220, 222 | fvmptd2 7023 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑖) = (1r‘𝑅)) | 
| 224 | 223 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑖) · 𝑖) = ((1r‘𝑅) · 𝑖)) | 
| 225 | 191 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → 𝑖 ∈ 𝐵) | 
| 226 | 2, 4, 163, 221, 225 | ringlidmd 20270 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → ((1r‘𝑅) · 𝑖) = 𝑖) | 
| 227 | 205, 224,
226 | 3eqtrrd 2781 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑖) → 𝑖 = (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) | 
| 228 |  | eleq1w 2823 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑋, 𝑖} ↔ 𝑥 ∈ {𝑋, 𝑖})) | 
| 229 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → (𝑦 = 𝑋 ↔ 𝑥 = 𝑋)) | 
| 230 | 229 | ifbid 4548 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)) = if(𝑥 = 𝑋, 𝑟, (1r‘𝑅))) | 
| 231 | 228, 230 | ifbieq1d 4549 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ) = if(𝑥 ∈ {𝑋, 𝑖}, if(𝑥 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) | 
| 232 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 𝑥 ∈ 𝐼) | 
| 233 | 30, 232 | sselid 3980 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 𝑥 ∈ (𝐼 ∪ {𝑋})) | 
| 234 | 193 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 𝑟 ∈ 𝐵) | 
| 235 | 165 | ad5antr 734 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → (1r‘𝑅) ∈ 𝐵) | 
| 236 | 234, 235 | ifcld 4571 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → if(𝑥 = 𝑋, 𝑟, (1r‘𝑅)) ∈ 𝐵) | 
| 237 | 186 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 0 ∈ 𝐵) | 
| 238 | 236, 237 | ifcld 4571 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → if(𝑥 ∈ {𝑋, 𝑖}, if(𝑥 = 𝑋, 𝑟, (1r‘𝑅)), 0 ) ∈ 𝐵) | 
| 239 | 180, 231,
233, 238 | fvmptd3 7038 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) = if(𝑥 ∈ {𝑋, 𝑖}, if(𝑥 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) | 
| 240 | 214 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → ¬ 𝑋 ∈ 𝐼) | 
| 241 |  | nelne2 3039 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝐼 ∧ ¬ 𝑋 ∈ 𝐼) → 𝑥 ≠ 𝑋) | 
| 242 | 232, 240,
241 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 𝑥 ≠ 𝑋) | 
| 243 |  | neqne 2947 | . . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑥 = 𝑖 → 𝑥 ≠ 𝑖) | 
| 244 | 243 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 𝑥 ≠ 𝑖) | 
| 245 | 242, 244 | nelprd 4656 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → ¬ 𝑥 ∈ {𝑋, 𝑖}) | 
| 246 | 245 | iffalsed 4535 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → if(𝑥 ∈ {𝑋, 𝑖}, if(𝑥 = 𝑋, 𝑟, (1r‘𝑅)), 0 ) = 0 ) | 
| 247 | 239, 246 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) = 0 ) | 
| 248 | 247 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥) = ( 0 · 𝑥)) | 
| 249 | 192 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 𝑅 ∈ Ring) | 
| 250 | 189 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 𝐼 ⊆ 𝐵) | 
| 251 | 250, 232 | sseldd 3983 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 𝑥 ∈ 𝐵) | 
| 252 | 249, 251,
99 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → ( 0 · 𝑥) = 0 ) | 
| 253 | 248, 252 | eqtr2d 2777 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) ∧ ¬ 𝑥 = 𝑖) → 0 = (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) | 
| 254 | 227, 253 | ifeqda 4561 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑖, 𝑖, 0 ) = (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) | 
| 255 | 254 | mpteq2dva 5241 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑖, 𝑖, 0 )) = (𝑥 ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))) | 
| 256 | 255 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑖, 𝑖, 0 ))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)))) | 
| 257 | 201, 256 | eqtr3d 2778 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝑖 = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)))) | 
| 258 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) | 
| 259 |  | simplr 768 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → 𝑥 = 𝑋) | 
| 260 | 194 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → 𝑋 ∈ 𝐵) | 
| 261 |  | prid1g 4759 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ {𝑋, 𝑖}) | 
| 262 | 260, 261 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → 𝑋 ∈ {𝑋, 𝑖}) | 
| 263 | 259, 262 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → 𝑥 ∈ {𝑋, 𝑖}) | 
| 264 | 258, 263 | eqeltrd 2840 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → 𝑦 ∈ {𝑋, 𝑖}) | 
| 265 | 264 | iftrued 4532 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ) = if(𝑦 = 𝑋, 𝑟, (1r‘𝑅))) | 
| 266 | 258, 259 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑋) | 
| 267 | 266 | iftrued 4532 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)) = 𝑟) | 
| 268 | 265, 267 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑥) → if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ) = 𝑟) | 
| 269 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) | 
| 270 | 116 | ad4antr 732 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) → 𝑋 ∈ {𝑋}) | 
| 271 | 270, 24 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) → 𝑋 ∈ (𝐼 ∪ {𝑋})) | 
| 272 | 269, 271 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) → 𝑥 ∈ (𝐼 ∪ {𝑋})) | 
| 273 | 193 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) → 𝑟 ∈ 𝐵) | 
| 274 | 180, 268,
272, 273 | fvmptd2 7023 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) = 𝑟) | 
| 275 | 274, 269 | oveq12d 7450 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 = 𝑋) → (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥) = (𝑟 · 𝑋)) | 
| 276 | 2, 198, 194, 195, 275 | gsumsnd 19971 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑅 Σg (𝑥 ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))) = (𝑟 · 𝑋)) | 
| 277 | 276 | eqcomd 2742 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑟 · 𝑋) = (𝑅 Σg (𝑥 ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)))) | 
| 278 | 257, 277 | oveq12d 7450 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑖 + (𝑟 · 𝑋)) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))) + (𝑅 Σg (𝑥 ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))))) | 
| 279 | 197, 278 | eqtr3d 2778 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → ((𝑟 · 𝑋) + 𝑖) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))) + (𝑅 Σg (𝑥 ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))))) | 
| 280 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝐴 = ((𝑟 · 𝑋) + 𝑖)) | 
| 281 | 5 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → 𝑅 ∈ Ring) | 
| 282 | 170 | ffvelcdmda 7103 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) ∈ 𝐵) | 
| 283 | 13 | ad4antr 732 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → (𝐼 ∪ {𝑋}) ⊆ 𝐵) | 
| 284 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → 𝑥 ∈ (𝐼 ∪ {𝑋})) | 
| 285 | 283, 284 | sseldd 3983 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → 𝑥 ∈ 𝐵) | 
| 286 | 2, 4, 281, 282, 285 | ringcld 20258 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ (𝐼 ∪ {𝑋})) → (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥) ∈ 𝐵) | 
| 287 | 161 | mptexd 7245 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) ∈ V) | 
| 288 |  | funmpt 6603 | . . . . . . . . . 10
⊢ Fun
(𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) | 
| 289 | 288 | a1i 11 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → Fun (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))) | 
| 290 | 187 | fsuppimpd 9410 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ) ∈
Fin) | 
| 291 |  | nfv 1913 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) | 
| 292 | 291, 169,
180 | fnmptd 6708 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) Fn (𝐼 ∪ {𝑋})) | 
| 293 | 292 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → (𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) Fn (𝐼 ∪ {𝑋})) | 
| 294 | 161 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → (𝐼 ∪ {𝑋}) ∈ V) | 
| 295 | 186 | adantr 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 ))) | 
| 297 | 293, 294,
295, 296 | fvdifsupp 8197 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) = 0 ) | 
| 298 | 297 | oveq1d 7447 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥) = ( 0 · 𝑥)) | 
| 299 | 5 | ad4antr 732 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → 𝑅 ∈ Ring) | 
| 300 | 13 | ad4antr 732 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → (𝐼 ∪ {𝑋}) ⊆ 𝐵) | 
| 301 | 296 | eldifad 3962 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → 𝑥 ∈ (𝐼 ∪ {𝑋})) | 
| 302 | 300, 301 | sseldd 3983 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → 𝑥 ∈ 𝐵) | 
| 303 | 299, 302,
99 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → ( 0 · 𝑥) = 0 ) | 
| 304 | 298, 303 | eqtrd 2776 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) ∧ 𝑥 ∈ ((𝐼 ∪ {𝑋}) ∖ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 ))) → (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥) = 0 ) | 
| 305 | 304, 161 | suppss2 8226 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → ((𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) supp 0 ) ⊆ ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) supp 0 )) | 
| 306 | 290, 305 | ssfid 9302 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → ((𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) supp 0 ) ∈
Fin) | 
| 307 | 287, 186,
289, 306 | isfsuppd 9407 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)) finSupp 0 ) | 
| 308 | 214, 107 | sylibr 234 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝐼 ∩ {𝑋}) = ∅) | 
| 309 |  | eqidd 2737 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝐼 ∪ {𝑋}) = (𝐼 ∪ {𝑋})) | 
| 310 | 2, 3, 67, 188, 161, 286, 307, 308, 309 | gsumsplit2 19948 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))) + (𝑅 Σg (𝑥 ∈ {𝑋} ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))))) | 
| 311 | 279, 280,
310 | 3eqtr4d 2786 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥)))) | 
| 312 | 187, 311 | jca 511 | . . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → ((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 )) finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ (((𝑦 ∈ (𝐼 ∪ {𝑋}) ↦ if(𝑦 ∈ {𝑋, 𝑖}, if(𝑦 = 𝑋, 𝑟, (1r‘𝑅)), 0 ))‘𝑥) · 𝑥))))) | 
| 313 | 171, 179,
312 | rspcedvd 3623 | . . . 4
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) ∧ 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → ∃𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))(𝑎 finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 314 | 313 | r19.29ffa 32491 | . . 3
⊢ ((𝜑 ∧ ∃𝑟 ∈ 𝐵 ∃𝑖 ∈ 𝐼 𝐴 = ((𝑟 · 𝑋) + 𝑖)) → ∃𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))(𝑎 finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥))))) | 
| 315 | 157, 314 | impbida 800 | . 2
⊢ (𝜑 → (∃𝑎 ∈ (𝐵 ↑m (𝐼 ∪ {𝑋}))(𝑎 finSupp 0 ∧ 𝐴 = (𝑅 Σg (𝑥 ∈ (𝐼 ∪ {𝑋}) ↦ ((𝑎‘𝑥) · 𝑥)))) ↔ ∃𝑟 ∈ 𝐵 ∃𝑖 ∈ 𝐼 𝐴 = ((𝑟 · 𝑋) + 𝑖))) | 
| 316 | 14, 315 | bitrd 279 | 1
⊢ (𝜑 → (𝐴 ∈ (𝑁‘(𝐼 ∪ {𝑋})) ↔ ∃𝑟 ∈ 𝐵 ∃𝑖 ∈ 𝐼 𝐴 = ((𝑟 · 𝑋) + 𝑖))) |