Proof of Theorem rmodislmodlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rmodislmod.r | . . . . 5
⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) | 
| 2 |  | simprl 770 | . . . . . . . . 9
⊢ ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟)) | 
| 3 | 2 | 2ralimi 3122 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟)) | 
| 4 | 3 | 2ralimi 3122 | . . . . . . 7
⊢
(∀𝑞 ∈
𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟)) | 
| 5 |  | ralrot3 3292 | . . . . . . . . 9
⊢
(∀𝑞 ∈
𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟)) | 
| 6 |  | rmodislmod.v | . . . . . . . . . . . . . 14
⊢ 𝑉 = (Base‘𝑅) | 
| 7 | 6 | grpbn0 18985 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ Grp → 𝑉 ≠ ∅) | 
| 8 | 7 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → 𝑉 ≠ ∅) | 
| 9 | 1, 8 | ax-mp 5 | . . . . . . . . . . 11
⊢ 𝑉 ≠ ∅ | 
| 10 |  | rspn0 4355 | . . . . . . . . . . 11
⊢ (𝑉 ≠ ∅ →
(∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))) | 
| 11 | 9, 10 | ax-mp 5 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟)) | 
| 12 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑏 → (𝑞 × 𝑟) = (𝑏 × 𝑟)) | 
| 13 | 12 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑞 = 𝑏 → (𝑤 · (𝑞 × 𝑟)) = (𝑤 · (𝑏 × 𝑟))) | 
| 14 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑏 → (𝑤 · 𝑞) = (𝑤 · 𝑏)) | 
| 15 | 14 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑞 = 𝑏 → ((𝑤 · 𝑞) · 𝑟) = ((𝑤 · 𝑏) · 𝑟)) | 
| 16 | 13, 15 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ (𝑞 = 𝑏 → ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ↔ (𝑤 · (𝑏 × 𝑟)) = ((𝑤 · 𝑏) · 𝑟))) | 
| 17 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑎 → (𝑏 × 𝑟) = (𝑏 × 𝑎)) | 
| 18 | 17 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑟 = 𝑎 → (𝑤 · (𝑏 × 𝑟)) = (𝑤 · (𝑏 × 𝑎))) | 
| 19 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑟 = 𝑎 → ((𝑤 · 𝑏) · 𝑟) = ((𝑤 · 𝑏) · 𝑎)) | 
| 20 | 18, 19 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑎 → ((𝑤 · (𝑏 × 𝑟)) = ((𝑤 · 𝑏) · 𝑟) ↔ (𝑤 · (𝑏 × 𝑎)) = ((𝑤 · 𝑏) · 𝑎))) | 
| 21 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑐 → (𝑤 · (𝑏 × 𝑎)) = (𝑐 · (𝑏 × 𝑎))) | 
| 22 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑐 → (𝑤 · 𝑏) = (𝑐 · 𝑏)) | 
| 23 | 22 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑐 → ((𝑤 · 𝑏) · 𝑎) = ((𝑐 · 𝑏) · 𝑎)) | 
| 24 | 21, 23 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑐 → ((𝑤 · (𝑏 × 𝑎)) = ((𝑤 · 𝑏) · 𝑎) ↔ (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎))) | 
| 25 | 16, 20, 24 | rspc3v 3637 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎))) | 
| 26 | 25 | 3com12 1123 | . . . . . . . . . 10
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎))) | 
| 27 | 11, 26 | syl5com 31 | . . . . . . . . 9
⊢
(∀𝑥 ∈
𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎))) | 
| 28 | 5, 27 | sylbi 217 | . . . . . . . 8
⊢
(∀𝑞 ∈
𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎))) | 
| 29 |  | eqcom 2743 | . . . . . . . 8
⊢ (((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)) ↔ (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)) | 
| 30 | 28, 29 | imbitrrdi 252 | . . . . . . 7
⊢
(∀𝑞 ∈
𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)))) | 
| 31 | 4, 30 | syl 17 | . . . . . 6
⊢
(∀𝑞 ∈
𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)))) | 
| 32 | 31 | 3ad2ant3 1135 | . . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)))) | 
| 33 | 1, 32 | ax-mp 5 | . . . 4
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎))) | 
| 34 | 33 | adantl 481 | . . 3
⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎))) | 
| 35 |  | rmodislmod.k | . . . . . . . . . 10
⊢ 𝐾 = (Base‘𝐹) | 
| 36 |  | rmodislmod.t | . . . . . . . . . 10
⊢  × =
(.r‘𝐹) | 
| 37 | 35, 36 | crngcom 20249 | . . . . . . . . 9
⊢ ((𝐹 ∈ CRing ∧ 𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾) → (𝑏 × 𝑎) = (𝑎 × 𝑏)) | 
| 38 | 37 | 3expb 1120 | . . . . . . . 8
⊢ ((𝐹 ∈ CRing ∧ (𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾)) → (𝑏 × 𝑎) = (𝑎 × 𝑏)) | 
| 39 | 38 | expcom 413 | . . . . . . 7
⊢ ((𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏))) | 
| 40 | 39 | ancoms 458 | . . . . . 6
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏))) | 
| 41 | 40 | 3adant3 1132 | . . . . 5
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏))) | 
| 42 | 41 | impcom 407 | . . . 4
⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → (𝑏 × 𝑎) = (𝑎 × 𝑏)) | 
| 43 | 42 | oveq2d 7448 | . . 3
⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → (𝑐 · (𝑏 × 𝑎)) = (𝑐 · (𝑎 × 𝑏))) | 
| 44 | 34, 43 | eqtrd 2776 | . 2
⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑎 × 𝑏))) | 
| 45 |  | rmodislmod.m | . . . . . . 7
⊢  ∗ =
(𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)) | 
| 46 | 45 | a1i 11 | . . . . . 6
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠))) | 
| 47 |  | oveq12 7441 | . . . . . . . 8
⊢ ((𝑣 = 𝑐 ∧ 𝑠 = 𝑏) → (𝑣 · 𝑠) = (𝑐 · 𝑏)) | 
| 48 | 47 | ancoms 458 | . . . . . . 7
⊢ ((𝑠 = 𝑏 ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · 𝑏)) | 
| 49 | 48 | adantl 481 | . . . . . 6
⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑏 ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑏)) | 
| 50 |  | simp2 1137 | . . . . . 6
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑏 ∈ 𝐾) | 
| 51 |  | simp3 1138 | . . . . . 6
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉) | 
| 52 |  | ovexd 7467 | . . . . . 6
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ V) | 
| 53 | 46, 49, 50, 51, 52 | ovmpod 7586 | . . . . 5
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑏 ∗ 𝑐) = (𝑐 · 𝑏)) | 
| 54 | 53 | oveq2d 7448 | . . . 4
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ (𝑏 ∗ 𝑐)) = (𝑎 ∗ (𝑐 · 𝑏))) | 
| 55 |  | oveq12 7441 | . . . . . . 7
⊢ ((𝑣 = (𝑐 · 𝑏) ∧ 𝑠 = 𝑎) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎)) | 
| 56 | 55 | ancoms 458 | . . . . . 6
⊢ ((𝑠 = 𝑎 ∧ 𝑣 = (𝑐 · 𝑏)) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎)) | 
| 57 | 56 | adantl 481 | . . . . 5
⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑎 ∧ 𝑣 = (𝑐 · 𝑏))) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎)) | 
| 58 |  | simp1 1136 | . . . . 5
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑎 ∈ 𝐾) | 
| 59 |  | simpl1 1191 | . . . . . . . . . . 11
⊢ ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · 𝑟) ∈ 𝑉) | 
| 60 | 59 | 2ralimi 3122 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉) | 
| 61 | 60 | 2ralimi 3122 | . . . . . . . . 9
⊢
(∀𝑞 ∈
𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉) | 
| 62 |  | ringgrp 20236 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp) | 
| 63 | 35 | grpbn0 18985 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ Grp → 𝐾 ≠ ∅) | 
| 64 | 62, 63 | syl 17 | . . . . . . . . . . . 12
⊢ (𝐹 ∈ Ring → 𝐾 ≠ ∅) | 
| 65 | 64 | 3ad2ant2 1134 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → 𝐾 ≠ ∅) | 
| 66 | 1, 65 | ax-mp 5 | . . . . . . . . . 10
⊢ 𝐾 ≠ ∅ | 
| 67 |  | rspn0 4355 | . . . . . . . . . 10
⊢ (𝐾 ≠ ∅ →
(∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)) | 
| 68 | 66, 67 | ax-mp 5 | . . . . . . . . 9
⊢
(∀𝑞 ∈
𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉) | 
| 69 |  | ralcom 3288 | . . . . . . . . . 10
⊢
(∀𝑟 ∈
𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉) | 
| 70 |  | rspn0 4355 | . . . . . . . . . . . 12
⊢ (𝑉 ≠ ∅ →
(∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)) | 
| 71 | 9, 70 | ax-mp 5 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉) | 
| 72 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑟 = 𝑏 → (𝑤 · 𝑟) = (𝑤 · 𝑏)) | 
| 73 | 72 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑏 → ((𝑤 · 𝑟) ∈ 𝑉 ↔ (𝑤 · 𝑏) ∈ 𝑉)) | 
| 74 | 22 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑐 → ((𝑤 · 𝑏) ∈ 𝑉 ↔ (𝑐 · 𝑏) ∈ 𝑉)) | 
| 75 | 73, 74 | rspc2v 3632 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → (𝑐 · 𝑏) ∈ 𝑉)) | 
| 76 | 71, 75 | syl5com 31 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉)) | 
| 77 | 69, 76 | sylbi 217 | . . . . . . . . 9
⊢
(∀𝑟 ∈
𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉)) | 
| 78 | 61, 68, 77 | 3syl 18 | . . . . . . . 8
⊢
(∀𝑞 ∈
𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉)) | 
| 79 | 78 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉)) | 
| 80 | 1, 79 | ax-mp 5 | . . . . . 6
⊢ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉) | 
| 81 | 80 | 3adant1 1130 | . . . . 5
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉) | 
| 82 |  | ovexd 7467 | . . . . 5
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) ∈ V) | 
| 83 | 46, 57, 58, 81, 82 | ovmpod 7586 | . . . 4
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ (𝑐 · 𝑏)) = ((𝑐 · 𝑏) · 𝑎)) | 
| 84 | 54, 83 | eqtrd 2776 | . . 3
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ (𝑏 ∗ 𝑐)) = ((𝑐 · 𝑏) · 𝑎)) | 
| 85 | 84 | adantl 481 | . 2
⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∗ (𝑏 ∗ 𝑐)) = ((𝑐 · 𝑏) · 𝑎)) | 
| 86 |  | oveq12 7441 | . . . . . 6
⊢ ((𝑣 = 𝑐 ∧ 𝑠 = (𝑎 × 𝑏)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏))) | 
| 87 | 86 | ancoms 458 | . . . . 5
⊢ ((𝑠 = (𝑎 × 𝑏) ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏))) | 
| 88 | 87 | adantl 481 | . . . 4
⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = (𝑎 × 𝑏) ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏))) | 
| 89 | 35, 36 | ringcl 20248 | . . . . . . . 8
⊢ ((𝐹 ∈ Ring ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 × 𝑏) ∈ 𝐾) | 
| 90 | 89 | 3expib 1122 | . . . . . . 7
⊢ (𝐹 ∈ Ring → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 × 𝑏) ∈ 𝐾)) | 
| 91 | 90 | 3ad2ant2 1134 | . . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 × 𝑏) ∈ 𝐾)) | 
| 92 | 1, 91 | ax-mp 5 | . . . . 5
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 × 𝑏) ∈ 𝐾) | 
| 93 | 92 | 3adant3 1132 | . . . 4
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 × 𝑏) ∈ 𝐾) | 
| 94 |  | ovexd 7467 | . . . 4
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑎 × 𝑏)) ∈ V) | 
| 95 | 46, 88, 93, 51, 94 | ovmpod 7586 | . . 3
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑐 · (𝑎 × 𝑏))) | 
| 96 | 95 | adantl 481 | . 2
⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑐 · (𝑎 × 𝑏))) | 
| 97 | 44, 85, 96 | 3eqtr4rd 2787 | 1
⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑎 ∗ (𝑏 ∗ 𝑐))) |