| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑥 ↑ (𝐴 + 𝐵)) = (0 ↑ (𝐴 + 𝐵))) |
| 2 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (0...𝑥) = (0...0)) |
| 3 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝑥C𝑘) = (0C𝑘)) |
| 4 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (𝑥 − 𝑘) = (0 − 𝑘)) |
| 5 | 4 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → ((𝑥 − 𝑘) ↑ 𝐴) = ((0 − 𝑘) ↑ 𝐴)) |
| 6 | 5 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) |
| 7 | 3, 6 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
| 8 | 2, 7 | mpteq12dv 5233 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...0) ↦ ((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
| 9 | 8 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (𝑅 Σg (𝑘 ∈ (0...0) ↦
((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
| 10 | 1, 9 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑥 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ↔ (0 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...0) ↦
((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
| 11 | 10 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 0 → (((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑥 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) ↔ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (0 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...0) ↦
((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))))) |
| 12 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑥 ↑ (𝐴 + 𝐵)) = (𝑛 ↑ (𝐴 + 𝐵))) |
| 13 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (0...𝑥) = (0...𝑛)) |
| 14 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (𝑥C𝑘) = (𝑛C𝑘)) |
| 15 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑛 → (𝑥 − 𝑘) = (𝑛 − 𝑘)) |
| 16 | 15 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → ((𝑥 − 𝑘) ↑ 𝐴) = ((𝑛 − 𝑘) ↑ 𝐴)) |
| 17 | 16 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) |
| 18 | 14, 17 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
| 19 | 13, 18 | mpteq12dv 5233 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
| 20 | 19 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
| 21 | 12, 20 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝑥 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ↔ (𝑛 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
| 22 | 21 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑛 → (((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑥 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) ↔ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑛 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))))) |
| 23 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ↑ (𝐴 + 𝐵)) = ((𝑛 + 1) ↑ (𝐴 + 𝐵))) |
| 24 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (0...𝑥) = (0...(𝑛 + 1))) |
| 25 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (𝑥C𝑘) = ((𝑛 + 1)C𝑘)) |
| 26 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑛 + 1) → (𝑥 − 𝑘) = ((𝑛 + 1) − 𝑘)) |
| 27 | 26 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 − 𝑘) ↑ 𝐴) = (((𝑛 + 1) − 𝑘) ↑ 𝐴)) |
| 28 | 27 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) |
| 29 | 25, 28 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = (((𝑛 + 1)C𝑘) · ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
| 30 | 24, 29 | mpteq12dv 5233 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...(𝑛 + 1)) ↦ (((𝑛 + 1)C𝑘) · ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
| 31 | 30 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (𝑅 Σg (𝑘 ∈ (0...(𝑛 + 1)) ↦ (((𝑛 + 1)C𝑘) · ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
| 32 | 23, 31 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ↔ ((𝑛 + 1) ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...(𝑛 + 1)) ↦ (((𝑛 + 1)C𝑘) · ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
| 33 | 32 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → (((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑥 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) ↔ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → ((𝑛 + 1) ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...(𝑛 + 1)) ↦ (((𝑛 + 1)C𝑘) · ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))))) |
| 34 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑥 ↑ (𝐴 + 𝐵)) = (𝑁 ↑ (𝐴 + 𝐵))) |
| 35 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (0...𝑥) = (0...𝑁)) |
| 36 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑁 → (𝑥C𝑘) = (𝑁C𝑘)) |
| 37 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑁 → (𝑥 − 𝑘) = (𝑁 − 𝑘)) |
| 38 | 37 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑁 → ((𝑥 − 𝑘) ↑ 𝐴) = ((𝑁 − 𝑘) ↑ 𝐴)) |
| 39 | 38 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑁 → (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) |
| 40 | 36, 39 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
| 41 | 35, 40 | mpteq12dv 5233 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
| 42 | 41 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
| 43 | 34, 42 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝑥 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ↔ (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
| 44 | 43 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑁 → (((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑥 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑥) ↦ ((𝑥C𝑘) · (((𝑥 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) ↔ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))))) |
| 45 | | simpr1 1195 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → 𝐴 ∈ 𝑆) |
| 46 | | srgbinom.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (mulGrp‘𝑅) |
| 47 | | srgbinom.s |
. . . . . . . . . . . 12
⊢ 𝑆 = (Base‘𝑅) |
| 48 | 46, 47 | mgpbas 20142 |
. . . . . . . . . . 11
⊢ 𝑆 = (Base‘𝐺) |
| 49 | 45, 48 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → 𝐴 ∈ (Base‘𝐺)) |
| 50 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 51 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 52 | | srgbinom.e |
. . . . . . . . . . 11
⊢ ↑ =
(.g‘𝐺) |
| 53 | 50, 51, 52 | mulg0 19092 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (Base‘𝐺) → (0 ↑ 𝐴) = (0g‘𝐺)) |
| 54 | 49, 53 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (0 ↑ 𝐴) = (0g‘𝐺)) |
| 55 | | simpr2 1196 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → 𝐵 ∈ 𝑆) |
| 56 | 55, 48 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → 𝐵 ∈ (Base‘𝐺)) |
| 57 | 50, 51, 52 | mulg0 19092 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (Base‘𝐺) → (0 ↑ 𝐵) = (0g‘𝐺)) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (0 ↑ 𝐵) = (0g‘𝐺)) |
| 59 | 54, 58 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → ((0 ↑ 𝐴) × (0 ↑ 𝐵)) = ((0g‘𝐺) ×
(0g‘𝐺))) |
| 60 | 59 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (1 · ((0 ↑ 𝐴) × (0 ↑ 𝐵))) = (1 ·
((0g‘𝐺)
×
(0g‘𝐺)))) |
| 61 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 62 | 47, 61 | srgidcl 20196 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ SRing →
(1r‘𝑅)
∈ 𝑆) |
| 63 | 62 | ancli 548 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ SRing → (𝑅 ∈ SRing ∧
(1r‘𝑅)
∈ 𝑆)) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑅 ∈ SRing ∧
(1r‘𝑅)
∈ 𝑆)) |
| 65 | | srgbinom.m |
. . . . . . . . . . . 12
⊢ × =
(.r‘𝑅) |
| 66 | 47, 65, 61 | srglidm 20199 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ SRing ∧
(1r‘𝑅)
∈ 𝑆) →
((1r‘𝑅)
×
(1r‘𝑅)) =
(1r‘𝑅)) |
| 67 | 64, 66 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → ((1r‘𝑅) ×
(1r‘𝑅)) =
(1r‘𝑅)) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (1 ·
((1r‘𝑅)
×
(1r‘𝑅))) =
(1 ·
(1r‘𝑅))) |
| 69 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 70 | 69, 61 | srgidcl 20196 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ SRing →
(1r‘𝑅)
∈ (Base‘𝑅)) |
| 71 | | srgbinom.t |
. . . . . . . . . . . 12
⊢ · =
(.g‘𝑅) |
| 72 | 69, 71 | mulg1 19099 |
. . . . . . . . . . 11
⊢
((1r‘𝑅) ∈ (Base‘𝑅) → (1 ·
(1r‘𝑅)) =
(1r‘𝑅)) |
| 73 | 70, 72 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ SRing → (1 ·
(1r‘𝑅)) =
(1r‘𝑅)) |
| 74 | 73 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (1 ·
(1r‘𝑅)) =
(1r‘𝑅)) |
| 75 | 68, 74 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (1 ·
((1r‘𝑅)
×
(1r‘𝑅))) =
(1r‘𝑅)) |
| 76 | 46, 61 | ringidval 20180 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (0g‘𝐺) |
| 77 | | id 22 |
. . . . . . . . . . . 12
⊢
((1r‘𝑅) = (0g‘𝐺) → (1r‘𝑅) = (0g‘𝐺)) |
| 78 | 77, 77 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
((1r‘𝑅) = (0g‘𝐺) → ((1r‘𝑅) ×
(1r‘𝑅)) =
((0g‘𝐺)
×
(0g‘𝐺))) |
| 79 | 78 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((1r‘𝑅) = (0g‘𝐺) → (1 ·
((1r‘𝑅)
×
(1r‘𝑅))) =
(1 ·
((0g‘𝐺)
×
(0g‘𝐺)))) |
| 80 | 79, 77 | eqeq12d 2753 |
. . . . . . . . 9
⊢
((1r‘𝑅) = (0g‘𝐺) → ((1 ·
((1r‘𝑅)
×
(1r‘𝑅))) =
(1r‘𝑅)
↔ (1 ·
((0g‘𝐺)
×
(0g‘𝐺))) =
(0g‘𝐺))) |
| 81 | 76, 80 | ax-mp 5 |
. . . . . . . 8
⊢ ((1 ·
((1r‘𝑅)
×
(1r‘𝑅))) =
(1r‘𝑅)
↔ (1 ·
((0g‘𝐺)
×
(0g‘𝐺))) =
(0g‘𝐺)) |
| 82 | 75, 81 | sylib 218 |
. . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (1 ·
((0g‘𝐺)
×
(0g‘𝐺))) =
(0g‘𝐺)) |
| 83 | 60, 82 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (1 · ((0 ↑ 𝐴) × (0 ↑ 𝐵))) = (0g‘𝐺)) |
| 84 | | fz0sn 13667 |
. . . . . . . . . 10
⊢ (0...0) =
{0} |
| 85 | 84 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (0...0) = {0}) |
| 86 | 85 | mpteq1d 5237 |
. . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑘 ∈ (0...0) ↦ ((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ {0} ↦ ((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
| 87 | 86 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑅 Σg (𝑘 ∈ (0...0) ↦
((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (𝑅 Σg (𝑘 ∈ {0} ↦ ((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
| 88 | | srgmnd 20187 |
. . . . . . . . 9
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
| 89 | 88 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → 𝑅 ∈ Mnd) |
| 90 | | c0ex 11255 |
. . . . . . . . 9
⊢ 0 ∈
V |
| 91 | 90 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → 0 ∈ V) |
| 92 | 76, 62 | eqeltrrid 2846 |
. . . . . . . . . 10
⊢ (𝑅 ∈ SRing →
(0g‘𝐺)
∈ 𝑆) |
| 93 | 92 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (0g‘𝐺) ∈ 𝑆) |
| 94 | 83, 93 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (1 · ((0 ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
| 95 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (0C𝑘) = (0C0)) |
| 96 | | 0nn0 12541 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
| 97 | | bcn0 14349 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℕ0 → (0C0) = 1) |
| 98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (0C0) =
1 |
| 99 | 95, 98 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (0C𝑘) = 1) |
| 100 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (0 − 𝑘) = (0 −
0)) |
| 101 | | 0m0e0 12386 |
. . . . . . . . . . . . 13
⊢ (0
− 0) = 0 |
| 102 | 100, 101 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (0 − 𝑘) = 0) |
| 103 | 102 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((0 − 𝑘) ↑ 𝐴) = (0 ↑ 𝐴)) |
| 104 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑘 ↑ 𝐵) = (0 ↑ 𝐵)) |
| 105 | 103, 104 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((0 ↑ 𝐴) × (0 ↑ 𝐵))) |
| 106 | 99, 105 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = (1 · ((0 ↑ 𝐴) × (0 ↑ 𝐵)))) |
| 107 | 47, 106 | gsumsn 19972 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ 0 ∈ V
∧ (1 · ((0 ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) → (𝑅 Σg (𝑘 ∈ {0} ↦ ((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (1 · ((0 ↑ 𝐴) × (0 ↑ 𝐵)))) |
| 108 | 89, 91, 94, 107 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑅 Σg (𝑘 ∈ {0} ↦ ((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (1 · ((0 ↑ 𝐴) × (0 ↑ 𝐵)))) |
| 109 | 87, 108 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑅 Σg (𝑘 ∈ (0...0) ↦
((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (1 · ((0 ↑ 𝐴) × (0 ↑ 𝐵)))) |
| 110 | | srgbinom.a |
. . . . . . . . . 10
⊢ + =
(+g‘𝑅) |
| 111 | 47, 110 | mndcl 18755 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 + 𝐵) ∈ 𝑆) |
| 112 | 89, 45, 55, 111 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝐴 + 𝐵) ∈ 𝑆) |
| 113 | 112, 48 | eleqtrdi 2851 |
. . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝐴 + 𝐵) ∈ (Base‘𝐺)) |
| 114 | 50, 51, 52 | mulg0 19092 |
. . . . . . 7
⊢ ((𝐴 + 𝐵) ∈ (Base‘𝐺) → (0 ↑ (𝐴 + 𝐵)) = (0g‘𝐺)) |
| 115 | 113, 114 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (0 ↑ (𝐴 + 𝐵)) = (0g‘𝐺)) |
| 116 | 83, 109, 115 | 3eqtr4rd 2788 |
. . . . 5
⊢ ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (0 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...0) ↦
((0C𝑘) · (((0 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
| 117 | | simprl 771 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ (𝑅 ∈ SRing ∧
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴)))) → 𝑅 ∈ SRing) |
| 118 | 45 | adantl 481 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ (𝑅 ∈ SRing ∧
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴)))) → 𝐴 ∈ 𝑆) |
| 119 | 55 | adantl 481 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ (𝑅 ∈ SRing ∧
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴)))) → 𝐵 ∈ 𝑆) |
| 120 | | simprr3 1224 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ (𝑅 ∈ SRing ∧
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴)))) → (𝐴 × 𝐵) = (𝐵 × 𝐴)) |
| 121 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ (𝑅 ∈ SRing ∧
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴)))) → 𝑛 ∈ ℕ0) |
| 122 | | id 22 |
. . . . . . . 8
⊢ ((𝑛 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) → (𝑛 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
| 123 | 47, 65, 71, 110, 46, 52, 117, 118, 119, 120, 121, 122 | srgbinomlem 20227 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ0
∧ (𝑅 ∈ SRing ∧
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴)))) ∧ (𝑛 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) → ((𝑛 + 1) ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...(𝑛 + 1)) ↦ (((𝑛 + 1)C𝑘) · ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
| 124 | 123 | exp31 419 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((𝑅 ∈ SRing
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → ((𝑛 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) → ((𝑛 + 1) ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...(𝑛 + 1)) ↦ (((𝑛 + 1)C𝑘) · ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))))) |
| 125 | 124 | a2d 29 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (((𝑅 ∈ SRing
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑛 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑛C𝑘) · (((𝑛 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) → ((𝑅 ∈ SRing ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → ((𝑛 + 1) ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...(𝑛 + 1)) ↦ (((𝑛 + 1)C𝑘) · ((((𝑛 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))))) |
| 126 | 11, 22, 33, 44, 116, 125 | nn0ind 12713 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝑅 ∈ SRing
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
| 127 | 126 | expd 415 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑅 ∈ SRing
→ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴)) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))))) |
| 128 | 127 | impcom 407 |
. 2
⊢ ((𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴)) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
| 129 | 128 | imp 406 |
1
⊢ (((𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |