| Step | Hyp | Ref
| Expression |
| 1 | | isclmp.s |
. . 3
⊢ 𝑆 = (Scalar‘𝑊) |
| 2 | | isclmp.k |
. . 3
⊢ 𝐾 = (Base‘𝑆) |
| 3 | 1, 2 | isclm 25097 |
. 2
⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) |
| 4 | | isclmp.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
| 5 | | isclmp.a |
. . . . 5
⊢ + =
(+g‘𝑊) |
| 6 | | isclmp.t |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
| 7 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 8 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝑆) = (.r‘𝑆) |
| 9 | | eqid 2737 |
. . . . 5
⊢
(1r‘𝑆) = (1r‘𝑆) |
| 10 | 4, 5, 6, 1, 2, 7, 8, 9 | islmod 20862 |
. . . 4
⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)))) |
| 11 | 10 | 3anbi1i 1158 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ↔ ((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) |
| 12 | | 3anass 1095 |
. . . 4
⊢ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ↔ ((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
| 13 | | df-3an 1089 |
. . . . 5
⊢ ((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ↔ ((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)))) |
| 14 | 13 | anbi1i 624 |
. . . 4
⊢ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ↔ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
| 15 | 12, 14 | bitri 275 |
. . 3
⊢ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ↔ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
| 16 | | an32 646 |
. . 3
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧
∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ↔ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)))) |
| 17 | 11, 15, 16 | 3bitri 297 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ↔ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)))) |
| 18 | | an32 646 |
. . . . 5
⊢ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ↔ ((𝑊 ∈ Grp ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ∧ 𝑆 ∈ Ring)) |
| 19 | | 3anass 1095 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ↔ (𝑊 ∈ Grp ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
| 20 | 19 | bicomi 224 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ↔ (𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) |
| 21 | 20 | anbi1i 624 |
. . . . 5
⊢ (((𝑊 ∈ Grp ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ∧ 𝑆 ∈ Ring) ↔ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ 𝑆 ∈ Ring)) |
| 22 | 18, 21 | bitri 275 |
. . . 4
⊢ (((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ↔ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ 𝑆 ∈ Ring)) |
| 23 | 22 | anbi1i 624 |
. . 3
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ↔ (((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ 𝑆 ∈ Ring) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)))) |
| 24 | | anass 468 |
. . 3
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ 𝑆 ∈ Ring) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ↔ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))))) |
| 25 | | df-3an 1089 |
. . . . . . . . . . 11
⊢ (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ↔ (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)))) |
| 26 | | ancom 460 |
. . . . . . . . . . 11
⊢ ((((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥) ↔ (((1r‘𝑆) · 𝑥) = 𝑥 ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) |
| 27 | 25, 26 | anbi12i 628 |
. . . . . . . . . 10
⊢ ((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)) ↔ ((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((1r‘𝑆) · 𝑥) = 𝑥 ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 28 | | an4 656 |
. . . . . . . . . 10
⊢
(((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((1r‘𝑆) · 𝑥) = 𝑥 ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ ((1r‘𝑆) · 𝑥) = 𝑥) ∧ (((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 29 | | an32 646 |
. . . . . . . . . . . 12
⊢ ((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ ((1r‘𝑆) · 𝑥) = 𝑥) ↔ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ((1r‘𝑆) · 𝑥) = 𝑥) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)))) |
| 30 | | ancom 460 |
. . . . . . . . . . . . 13
⊢ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ((1r‘𝑆) · 𝑥) = 𝑥) ↔ (((1r‘𝑆) · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) |
| 31 | 30 | anbi1i 624 |
. . . . . . . . . . . 12
⊢ ((((𝑦 · 𝑥) ∈ 𝑉 ∧ ((1r‘𝑆) · 𝑥) = 𝑥) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ↔ ((((1r‘𝑆) · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)))) |
| 32 | 29, 31 | bitri 275 |
. . . . . . . . . . 11
⊢ ((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ ((1r‘𝑆) · 𝑥) = 𝑥) ↔ ((((1r‘𝑆) · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)))) |
| 33 | 32 | anbi1i 624 |
. . . . . . . . . 10
⊢
(((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ ((1r‘𝑆) · 𝑥) = 𝑥) ∧ (((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((((1r‘𝑆) · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 34 | 27, 28, 33 | 3bitri 297 |
. . . . . . . . 9
⊢ ((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)) ↔ (((((1r‘𝑆) · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 35 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 = (ℂfld
↾s 𝐾)
→ (1r‘𝑆) =
(1r‘(ℂfld ↾s 𝐾))) |
| 36 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℂfld ↾s 𝐾) = (ℂfld
↾s 𝐾) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1r‘ℂfld) =
(1r‘ℂfld) |
| 38 | 36, 37 | subrg1 20582 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈
(SubRing‘ℂfld) →
(1r‘ℂfld) =
(1r‘(ℂfld ↾s 𝐾))) |
| 39 | 38 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈
(SubRing‘ℂfld) →
(1r‘(ℂfld ↾s 𝐾)) =
(1r‘ℂfld)) |
| 40 | 35, 39 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (1r‘𝑆) =
(1r‘ℂfld)) |
| 41 | | cnfld1 21406 |
. . . . . . . . . . . . . . . . 17
⊢ 1 =
(1r‘ℂfld) |
| 42 | 40, 41 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (1r‘𝑆) = 1) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → ((1r‘𝑆) · 𝑥) = (1 · 𝑥)) |
| 44 | 43 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (((1r‘𝑆) · 𝑥) = 𝑥 ↔ (1 · 𝑥) = 𝑥)) |
| 45 | 44 | 3adant1 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (((1r‘𝑆) · 𝑥) = 𝑥 ↔ (1 · 𝑥) = 𝑥)) |
| 46 | 45 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (((1r‘𝑆) · 𝑥) = 𝑥 ↔ (1 · 𝑥) = 𝑥)) |
| 47 | 46 | anbi1d 631 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → ((((1r‘𝑆) · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ↔ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉))) |
| 48 | 47 | anbi1d 631 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (((((1r‘𝑆) · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ↔ (((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))))) |
| 49 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(+g‘ℂfld) =
(+g‘ℂfld) |
| 50 | 36, 49 | ressplusg 17334 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈
(SubRing‘ℂfld) →
(+g‘ℂfld) =
(+g‘(ℂfld ↾s 𝐾))) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) →
(+g‘ℂfld) =
(+g‘(ℂfld ↾s 𝐾))) |
| 52 | | cnfldadd 21370 |
. . . . . . . . . . . . . . . . . 18
⊢ + =
(+g‘ℂfld) |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → + =
(+g‘ℂfld)) |
| 54 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 = (ℂfld
↾s 𝐾)
→ (+g‘𝑆) =
(+g‘(ℂfld ↾s 𝐾))) |
| 55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (+g‘𝑆) =
(+g‘(ℂfld ↾s 𝐾))) |
| 56 | 51, 53, 55 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (+g‘𝑆) = + ) |
| 57 | 56 | 3adant1 1131 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (+g‘𝑆) = + ) |
| 58 | 57 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (𝑟(+g‘𝑆)𝑦) = (𝑟 + 𝑦)) |
| 59 | 58 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (𝑟(+g‘𝑆)𝑦) = (𝑟 + 𝑦)) |
| 60 | 59 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 + 𝑦) · 𝑥)) |
| 61 | 60 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ↔ ((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)))) |
| 62 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(.r‘ℂfld) =
(.r‘ℂfld) |
| 63 | 36, 62 | ressmulr 17351 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈
(SubRing‘ℂfld) →
(.r‘ℂfld) =
(.r‘(ℂfld ↾s 𝐾))) |
| 64 | 63 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) →
(.r‘ℂfld) =
(.r‘(ℂfld ↾s 𝐾))) |
| 65 | | cnfldmul 21372 |
. . . . . . . . . . . . . . . . 17
⊢ ·
= (.r‘ℂfld) |
| 66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → · =
(.r‘ℂfld)) |
| 67 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 = (ℂfld
↾s 𝐾)
→ (.r‘𝑆) =
(.r‘(ℂfld ↾s 𝐾))) |
| 68 | 67 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (.r‘𝑆) =
(.r‘(ℂfld ↾s 𝐾))) |
| 69 | 64, 66, 68 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (.r‘𝑆) = · ) |
| 70 | 69 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (𝑟(.r‘𝑆)𝑦) = (𝑟 · 𝑦)) |
| 71 | 70 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (𝑟(.r‘𝑆)𝑦) = (𝑟 · 𝑦)) |
| 72 | 71 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → ((𝑟(.r‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑦) · 𝑥)) |
| 73 | 72 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ↔ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) |
| 74 | 61, 73 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → ((((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))) ↔ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 75 | 48, 74 | anbi12d 632 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → ((((((1r‘𝑆) · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 76 | 34, 75 | bitrid 283 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ (𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → ((((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)) ↔ ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 77 | 76 | 2ralbidva 3219 |
. . . . . . 7
⊢ (((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)) ↔ ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 78 | 77 | 2ralbidva 3219 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)) ↔ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 79 | | ralrot3 3293 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 80 | 79 | ralbii 3093 |
. . . . . . . 8
⊢
(∀𝑟 ∈
𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 81 | | ralcom 3289 |
. . . . . . . 8
⊢
(∀𝑟 ∈
𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 82 | 80, 81 | bitri 275 |
. . . . . . 7
⊢
(∀𝑟 ∈
𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 83 | | ralcom 3289 |
. . . . . . . 8
⊢
(∀𝑟 ∈
𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑦 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 84 | 83 | ralbii 3093 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑉 ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 85 | | ralcom 3289 |
. . . . . . . 8
⊢
(∀𝑟 ∈
𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 86 | 85 | 2ralbii 3128 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 87 | 82, 84, 86 | 3bitri 297 |
. . . . . 6
⊢
(∀𝑟 ∈
𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 88 | 78, 87 | bitrdi 287 |
. . . . 5
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 89 | 36 | subrgring 20574 |
. . . . . . . 8
⊢ (𝐾 ∈
(SubRing‘ℂfld) → (ℂfld
↾s 𝐾)
∈ Ring) |
| 90 | 89 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (ℂfld
↾s 𝐾)
∈ Ring) |
| 91 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑆 = (ℂfld
↾s 𝐾)
→ (𝑆 ∈ Ring
↔ (ℂfld ↾s 𝐾) ∈ Ring)) |
| 92 | 91 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (𝑆 ∈ Ring ↔ (ℂfld
↾s 𝐾)
∈ Ring)) |
| 93 | 90, 92 | mpbird 257 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → 𝑆 ∈ Ring) |
| 94 | 93 | biantrurd 532 |
. . . . 5
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)) ↔ (𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))))) |
| 95 | 4 | grpbn0 18984 |
. . . . . . . 8
⊢ (𝑊 ∈ Grp → 𝑉 ≠ ∅) |
| 96 | 95 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → 𝑉 ≠ ∅) |
| 97 | 37 | subrg1cl 20580 |
. . . . . . . . 9
⊢ (𝐾 ∈
(SubRing‘ℂfld) →
(1r‘ℂfld) ∈ 𝐾) |
| 98 | 97 | ne0d 4342 |
. . . . . . . 8
⊢ (𝐾 ∈
(SubRing‘ℂfld) → 𝐾 ≠ ∅) |
| 99 | 98 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → 𝐾 ≠ ∅) |
| 100 | | ancom 460 |
. . . . . . . . . . . . . . . . 17
⊢ ((((1
·
𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ↔ ((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉))) |
| 101 | 100 | anbi1i 624 |
. . . . . . . . . . . . . . . 16
⊢ (((((1
·
𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 102 | 101 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) → (((((1
·
𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 103 | 102 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑟 ∈ 𝐾 (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 104 | | r19.28zv 4501 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ≠ ∅ →
(∀𝑟 ∈ 𝐾 (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 105 | 104 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑟 ∈ 𝐾 (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 106 | 103, 105 | bitrd 279 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 107 | | anass 468 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ (((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 108 | | anass 468 |
. . . . . . . . . . . . . . 15
⊢ ((((1
·
𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) |
| 109 | 108 | anbi2i 623 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ (((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ↔ ((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))))) |
| 110 | | ancom 460 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))))) ↔ (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)))) |
| 111 | 107, 109,
110 | 3bitri 297 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉)) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)))) |
| 112 | 106, 111 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))))) |
| 113 | 112 | ralbidv 3178 |
. . . . . . . . . . 11
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑧 ∈ 𝑉 (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))))) |
| 114 | | r19.28zv 4501 |
. . . . . . . . . . . 12
⊢ (𝑉 ≠ ∅ →
(∀𝑧 ∈ 𝑉 (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ↔ (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))))) |
| 115 | 114 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑧 ∈ 𝑉 (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ↔ (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))))) |
| 116 | 113, 115 | bitrd 279 |
. . . . . . . . . 10
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))))) |
| 117 | | anass 468 |
. . . . . . . . . . 11
⊢ ((((1
·
𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ↔ ((1 · 𝑥) = 𝑥 ∧ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))))) |
| 118 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑟 → (𝑧 + 𝑦) = (𝑟 + 𝑦)) |
| 119 | 118 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑟 → ((𝑧 + 𝑦) · 𝑥) = ((𝑟 + 𝑦) · 𝑥)) |
| 120 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑟 → (𝑧 · 𝑥) = (𝑟 · 𝑥)) |
| 121 | 120 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑟 → ((𝑧 · 𝑥) + (𝑦 · 𝑥)) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) |
| 122 | 119, 121 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑟 → (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ↔ ((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)))) |
| 123 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑟 → (𝑧 · 𝑦) = (𝑟 · 𝑦)) |
| 124 | 123 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑟 → ((𝑧 · 𝑦) · 𝑥) = ((𝑟 · 𝑦) · 𝑥)) |
| 125 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑟 → (𝑧 · (𝑦 · 𝑥)) = (𝑟 · (𝑦 · 𝑥))) |
| 126 | 124, 125 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑟 → (((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥)) ↔ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) |
| 127 | 122, 126 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑟 → ((((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))) ↔ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 128 | 127 | cbvralvw 3237 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))) ↔ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) |
| 129 | 128 | 3anbi3i 1160 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥)))) ↔ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) |
| 130 | | 3anan32 1097 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)))) |
| 131 | 129, 130 | bitri 275 |
. . . . . . . . . . . . 13
⊢ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥)))) ↔ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)))) |
| 132 | 131 | bicomi 224 |
. . . . . . . . . . . 12
⊢ ((((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ↔ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))) |
| 133 | 132 | anbi2i 623 |
. . . . . . . . . . 11
⊢ (((1
·
𝑥) = 𝑥 ∧ (((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)))) ↔ ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥)))))) |
| 134 | 117, 133 | bitri 275 |
. . . . . . . . . 10
⊢ ((((1
·
𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑟 ∈ 𝐾 (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥))))) ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ↔ ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥)))))) |
| 135 | 116, 134 | bitrdi 287 |
. . . . . . . . 9
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 136 | 135 | ralbidv 3178 |
. . . . . . . 8
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑦 ∈ 𝐾 ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 137 | | r19.28zv 4501 |
. . . . . . . . 9
⊢ (𝐾 ≠ ∅ →
(∀𝑦 ∈ 𝐾 ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))) ↔ ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 138 | 137 | adantl 481 |
. . . . . . . 8
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑦 ∈ 𝐾 ((1 · 𝑥) = 𝑥 ∧ ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))) ↔ ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 139 | 136, 138 | bitrd 279 |
. . . . . . 7
⊢ ((𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅) →
(∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 140 | 96, 99, 139 | syl2anc 584 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 141 | 140 | ralbidv 3178 |
. . . . 5
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ((((1 · 𝑥) = 𝑥 ∧ (𝑦 · 𝑥) ∈ 𝑉) ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) ∧ (((𝑟 + 𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑟 · 𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)))) ↔ ∀𝑥 ∈ 𝑉 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 142 | 88, 94, 141 | 3bitr3d 309 |
. . . 4
⊢ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) → ((𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ↔ ∀𝑥 ∈ 𝑉 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 143 | 142 | pm5.32i 574 |
. . 3
⊢ (((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ (𝑆 ∈ Ring ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥)))) ↔ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ ∀𝑥 ∈ 𝑉 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 144 | 23, 24, 143 | 3bitri 297 |
. 2
⊢ ((((𝑊 ∈ Grp ∧ 𝑆 ∈ Ring) ∧ (𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) ∧ ∀𝑟 ∈ 𝐾 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝑉 ∀𝑥 ∈ 𝑉 (((𝑦 · 𝑥) ∈ 𝑉 ∧ (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ((𝑟(+g‘𝑆)𝑦) · 𝑥) = ((𝑟 · 𝑥) + (𝑦 · 𝑥))) ∧ (((𝑟(.r‘𝑆)𝑦) · 𝑥) = (𝑟 · (𝑦 · 𝑥)) ∧ ((1r‘𝑆) · 𝑥) = 𝑥))) ↔ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ ∀𝑥 ∈ 𝑉 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |
| 145 | 3, 17, 144 | 3bitri 297 |
1
⊢ (𝑊 ∈ ℂMod ↔
((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ∧ ∀𝑥 ∈ 𝑉 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) |