| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mpteq1 5234 | . . . 4
⊢ (𝑥 = ∅ → (𝑛 ∈ 𝑥 ↦ 𝐴) = (𝑛 ∈ ∅ ↦ 𝐴)) | 
| 2 | 1 | oveq2d 7448 | . . 3
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝑛 ∈ 𝑥 ↦ 𝐴)) = (𝐺 Σg (𝑛 ∈ ∅ ↦ 𝐴))) | 
| 3 | 2 | neeq1d 2999 | . 2
⊢ (𝑥 = ∅ → ((𝐺 Σg
(𝑛 ∈ 𝑥 ↦ 𝐴)) ≠ (0g‘𝑅) ↔ (𝐺 Σg (𝑛 ∈ ∅ ↦ 𝐴)) ≠
(0g‘𝑅))) | 
| 4 |  | mpteq1 5234 | . . . 4
⊢ (𝑥 = 𝑦 → (𝑛 ∈ 𝑥 ↦ 𝐴) = (𝑛 ∈ 𝑦 ↦ 𝐴)) | 
| 5 | 4 | oveq2d 7448 | . . 3
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝑛 ∈ 𝑥 ↦ 𝐴)) = (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴))) | 
| 6 | 5 | neeq1d 2999 | . 2
⊢ (𝑥 = 𝑦 → ((𝐺 Σg (𝑛 ∈ 𝑥 ↦ 𝐴)) ≠ (0g‘𝑅) ↔ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅))) | 
| 7 |  | mpteq1 5234 | . . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑛 ∈ 𝑥 ↦ 𝐴) = (𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴)) | 
| 8 | 7 | oveq2d 7448 | . . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝑛 ∈ 𝑥 ↦ 𝐴)) = (𝐺 Σg (𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴))) | 
| 9 | 8 | neeq1d 2999 | . 2
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐺 Σg (𝑛 ∈ 𝑥 ↦ 𝐴)) ≠ (0g‘𝑅) ↔ (𝐺 Σg (𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴)) ≠ (0g‘𝑅))) | 
| 10 |  | mpteq1 5234 | . . . 4
⊢ (𝑥 = 𝑁 → (𝑛 ∈ 𝑥 ↦ 𝐴) = (𝑛 ∈ 𝑁 ↦ 𝐴)) | 
| 11 | 10 | oveq2d 7448 | . . 3
⊢ (𝑥 = 𝑁 → (𝐺 Σg (𝑛 ∈ 𝑥 ↦ 𝐴)) = (𝐺 Σg (𝑛 ∈ 𝑁 ↦ 𝐴))) | 
| 12 | 11 | neeq1d 2999 | . 2
⊢ (𝑥 = 𝑁 → ((𝐺 Σg (𝑛 ∈ 𝑥 ↦ 𝐴)) ≠ (0g‘𝑅) ↔ (𝐺 Σg (𝑛 ∈ 𝑁 ↦ 𝐴)) ≠ (0g‘𝑅))) | 
| 13 |  | mpt0 6709 | . . . . . 6
⊢ (𝑛 ∈ ∅ ↦ 𝐴) = ∅ | 
| 14 | 13 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑛 ∈ ∅ ↦ 𝐴) = ∅) | 
| 15 | 14 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ ∅ ↦ 𝐴)) = (𝐺 Σg
∅)) | 
| 16 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 17 | 16 | gsum0 18698 | . . . . 5
⊢ (𝐺 Σg
∅) = (0g‘𝐺) | 
| 18 | 17 | a1i 11 | . . . 4
⊢ (𝜑 → (𝐺 Σg ∅) =
(0g‘𝐺)) | 
| 19 | 15, 18 | eqtrd 2776 | . . 3
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ ∅ ↦ 𝐴)) = (0g‘𝐺)) | 
| 20 |  | idomnnzgmulnz.1 | . . . . . . 7
⊢ 𝐺 = (mulGrp‘𝑅) | 
| 21 |  | eqid 2736 | . . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 22 | 20, 21 | ringidval 20181 | . . . . . 6
⊢
(1r‘𝑅) = (0g‘𝐺) | 
| 23 | 22 | eqcomi 2745 | . . . . 5
⊢
(0g‘𝐺) = (1r‘𝑅) | 
| 24 | 23 | a1i 11 | . . . 4
⊢ (𝜑 → (0g‘𝐺) = (1r‘𝑅)) | 
| 25 |  | idomnnzgmulnz.2 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ IDomn) | 
| 26 |  | isidom 20726 | . . . . . 6
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | 
| 27 | 26 | simprbi 496 | . . . . 5
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) | 
| 28 |  | domnnzr 20707 | . . . . 5
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | 
| 29 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 30 | 21, 29 | nzrnz 20516 | . . . . 5
⊢ (𝑅 ∈ NzRing →
(1r‘𝑅)
≠ (0g‘𝑅)) | 
| 31 | 25, 27, 28, 30 | 4syl 19 | . . . 4
⊢ (𝜑 → (1r‘𝑅) ≠
(0g‘𝑅)) | 
| 32 | 24, 31 | eqnetrd 3007 | . . 3
⊢ (𝜑 → (0g‘𝐺) ≠
(0g‘𝑅)) | 
| 33 | 19, 32 | eqnetrd 3007 | . 2
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ ∅ ↦ 𝐴)) ≠
(0g‘𝑅)) | 
| 34 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑚𝐴 | 
| 35 |  | nfcsb1v 3922 | . . . . . . . 8
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 | 
| 36 |  | csbeq1a 3912 | . . . . . . . 8
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) | 
| 37 | 34, 35, 36 | cbvmpt 5252 | . . . . . . 7
⊢ (𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴) = (𝑚 ∈ (𝑦 ∪ {𝑧}) ↦ ⦋𝑚 / 𝑛⦌𝐴) | 
| 38 | 37 | oveq2i 7443 | . . . . . 6
⊢ (𝐺 Σg
(𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴)) = (𝐺 Σg (𝑚 ∈ (𝑦 ∪ {𝑧}) ↦ ⦋𝑚 / 𝑛⦌𝐴)) | 
| 39 | 38 | a1i 11 | . . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝐺 Σg (𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴)) = (𝐺 Σg (𝑚 ∈ (𝑦 ∪ {𝑧}) ↦ ⦋𝑚 / 𝑛⦌𝐴))) | 
| 40 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 41 |  | eqid 2736 | . . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 42 | 26 | simplbi 497 | . . . . . . . . . 10
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) | 
| 43 | 25, 42 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 44 | 20 | crngmgp 20239 | . . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd) | 
| 45 | 43, 44 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ CMnd) | 
| 46 | 45 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → 𝐺 ∈ CMnd) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → 𝐺 ∈ CMnd) | 
| 48 |  | idomnnzgmulnz.3 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ Fin) | 
| 49 | 48 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → 𝑁 ∈ Fin) | 
| 50 |  | simprl 770 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → 𝑦 ⊆ 𝑁) | 
| 51 | 49, 50 | ssfid 9302 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → 𝑦 ∈ Fin) | 
| 52 | 51 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → 𝑦 ∈ Fin) | 
| 53 | 50 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) ∧ 𝑚 ∈ 𝑦) → 𝑦 ⊆ 𝑁) | 
| 54 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) ∧ 𝑚 ∈ 𝑦) → 𝑚 ∈ 𝑦) | 
| 55 | 53, 54 | sseldd 3983 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) ∧ 𝑚 ∈ 𝑦) → 𝑚 ∈ 𝑁) | 
| 56 |  | idomnnzgmulnz.4 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅)) | 
| 57 | 56 | ralrimiva 3145 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ 𝑁 𝐴 ∈ (Base‘𝑅)) | 
| 58 | 57 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) ∧ 𝑚 ∈ 𝑦) → ∀𝑛 ∈ 𝑁 𝐴 ∈ (Base‘𝑅)) | 
| 59 |  | rspcsbela 4437 | . . . . . . . 8
⊢ ((𝑚 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝐴 ∈ (Base‘𝑅)) → ⦋𝑚 / 𝑛⦌𝐴 ∈ (Base‘𝑅)) | 
| 60 | 55, 58, 59 | syl2anc 584 | . . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) ∧ 𝑚 ∈ 𝑦) → ⦋𝑚 / 𝑛⦌𝐴 ∈ (Base‘𝑅)) | 
| 61 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 62 | 20, 61 | mgpbas 20143 | . . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝐺) | 
| 63 | 62 | a1i 11 | . . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) ∧ 𝑚 ∈ 𝑦) → (Base‘𝑅) = (Base‘𝐺)) | 
| 64 | 60, 63 | eleqtrd 2842 | . . . . . 6
⊢ ((((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) ∧ 𝑚 ∈ 𝑦) → ⦋𝑚 / 𝑛⦌𝐴 ∈ (Base‘𝐺)) | 
| 65 |  | eldifi 4130 | . . . . . . . . 9
⊢ (𝑧 ∈ (𝑁 ∖ 𝑦) → 𝑧 ∈ 𝑁) | 
| 66 | 65 | adantl 481 | . . . . . . . 8
⊢ ((𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦)) → 𝑧 ∈ 𝑁) | 
| 67 | 66 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → 𝑧 ∈ 𝑁) | 
| 68 | 67 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → 𝑧 ∈ 𝑁) | 
| 69 |  | eldifn 4131 | . . . . . . . . 9
⊢ (𝑧 ∈ (𝑁 ∖ 𝑦) → ¬ 𝑧 ∈ 𝑦) | 
| 70 | 69 | adantl 481 | . . . . . . . 8
⊢ ((𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦)) → ¬ 𝑧 ∈ 𝑦) | 
| 71 | 70 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦) | 
| 72 | 71 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → ¬ 𝑧 ∈ 𝑦) | 
| 73 | 57 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → ∀𝑛 ∈ 𝑁 𝐴 ∈ (Base‘𝑅)) | 
| 74 |  | rspcsbela 4437 | . . . . . . . 8
⊢ ((𝑧 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝐴 ∈ (Base‘𝑅)) → ⦋𝑧 / 𝑛⦌𝐴 ∈ (Base‘𝑅)) | 
| 75 | 68, 73, 74 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → ⦋𝑧 / 𝑛⦌𝐴 ∈ (Base‘𝑅)) | 
| 76 | 62 | a1i 11 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (Base‘𝑅) = (Base‘𝐺)) | 
| 77 | 75, 76 | eleqtrd 2842 | . . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → ⦋𝑧 / 𝑛⦌𝐴 ∈ (Base‘𝐺)) | 
| 78 |  | csbeq1 3901 | . . . . . 6
⊢ (𝑚 = 𝑧 → ⦋𝑚 / 𝑛⦌𝐴 = ⦋𝑧 / 𝑛⦌𝐴) | 
| 79 | 40, 41, 47, 52, 64, 68, 72, 77, 78 | gsumunsn 19979 | . . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝐺 Σg (𝑚 ∈ (𝑦 ∪ {𝑧}) ↦ ⦋𝑚 / 𝑛⦌𝐴)) = ((𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴))(+g‘𝐺)⦋𝑧 / 𝑛⦌𝐴)) | 
| 80 | 39, 79 | eqtrd 2776 | . . . 4
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝐺 Σg (𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴)) = ((𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴))(+g‘𝐺)⦋𝑧 / 𝑛⦌𝐴)) | 
| 81 | 25, 27 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Domn) | 
| 82 | 81 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → 𝑅 ∈ Domn) | 
| 83 | 82 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → 𝑅 ∈ Domn) | 
| 84 | 60 | ralrimiva 3145 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → ∀𝑚 ∈ 𝑦 ⦋𝑚 / 𝑛⦌𝐴 ∈ (Base‘𝑅)) | 
| 85 | 62, 47, 52, 84 | gsummptcl 19986 | . . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴)) ∈ (Base‘𝑅)) | 
| 86 | 36 | equcoms 2018 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) | 
| 87 | 86 | eqcomd 2742 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ⦋𝑚 / 𝑛⦌𝐴 = 𝐴) | 
| 88 | 35, 34, 87 | cbvmpt 5252 | . . . . . . . . 9
⊢ (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴) = (𝑛 ∈ 𝑦 ↦ 𝐴) | 
| 89 | 88 | a1i 11 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴) = (𝑛 ∈ 𝑦 ↦ 𝐴)) | 
| 90 | 89 | oveq2d 7448 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴)) = (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴))) | 
| 91 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) | 
| 92 | 90, 91 | eqnetrd 3007 | . . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴)) ≠ (0g‘𝑅)) | 
| 93 | 85, 92 | jca 511 | . . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → ((𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴)) ∈ (Base‘𝑅) ∧ (𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴)) ≠ (0g‘𝑅))) | 
| 94 |  | idomnnzgmulnz.5 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ≠ (0g‘𝑅)) | 
| 95 | 94 | ralrimiva 3145 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ 𝑁 𝐴 ≠ (0g‘𝑅)) | 
| 96 | 95 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → ∀𝑛 ∈ 𝑁 𝐴 ≠ (0g‘𝑅)) | 
| 97 |  | rspcsbnea 42133 | . . . . . . . 8
⊢ ((𝑧 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝐴 ≠ (0g‘𝑅)) → ⦋𝑧 / 𝑛⦌𝐴 ≠ (0g‘𝑅)) | 
| 98 | 67, 96, 97 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → ⦋𝑧 / 𝑛⦌𝐴 ≠ (0g‘𝑅)) | 
| 99 | 98 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → ⦋𝑧 / 𝑛⦌𝐴 ≠ (0g‘𝑅)) | 
| 100 | 75, 99 | jca 511 | . . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (⦋𝑧 / 𝑛⦌𝐴 ∈ (Base‘𝑅) ∧ ⦋𝑧 / 𝑛⦌𝐴 ≠ (0g‘𝑅))) | 
| 101 |  | eqid 2736 | . . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 102 | 20, 101 | mgpplusg 20142 | . . . . . . 7
⊢
(.r‘𝑅) = (+g‘𝐺) | 
| 103 | 102 | eqcomi 2745 | . . . . . 6
⊢
(+g‘𝐺) = (.r‘𝑅) | 
| 104 | 61, 103, 29 | domnmuln0 20710 | . . . . 5
⊢ ((𝑅 ∈ Domn ∧ ((𝐺 Σg
(𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴)) ∈ (Base‘𝑅) ∧ (𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴)) ≠ (0g‘𝑅)) ∧ (⦋𝑧 / 𝑛⦌𝐴 ∈ (Base‘𝑅) ∧ ⦋𝑧 / 𝑛⦌𝐴 ≠ (0g‘𝑅))) → ((𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴))(+g‘𝐺)⦋𝑧 / 𝑛⦌𝐴) ≠ (0g‘𝑅)) | 
| 105 | 83, 93, 100, 104 | syl3anc 1372 | . . . 4
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → ((𝐺 Σg (𝑚 ∈ 𝑦 ↦ ⦋𝑚 / 𝑛⦌𝐴))(+g‘𝐺)⦋𝑧 / 𝑛⦌𝐴) ≠ (0g‘𝑅)) | 
| 106 | 80, 105 | eqnetrd 3007 | . . 3
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) ∧ (𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅)) → (𝐺 Σg (𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴)) ≠ (0g‘𝑅)) | 
| 107 | 106 | ex 412 | . 2
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ (𝑁 ∖ 𝑦))) → ((𝐺 Σg (𝑛 ∈ 𝑦 ↦ 𝐴)) ≠ (0g‘𝑅) → (𝐺 Σg (𝑛 ∈ (𝑦 ∪ {𝑧}) ↦ 𝐴)) ≠ (0g‘𝑅))) | 
| 108 | 3, 6, 9, 12, 33, 107, 48 | findcard2d 9207 | 1
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ 𝐴)) ≠ (0g‘𝑅)) |