MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rmodislmodlem Structured version   Visualization version   GIF version

Theorem rmodislmodlem 18978
Description: Lemma for rmodislmod 18979. This is the part of the proof of rmodislmod 18979 which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021.)
Hypotheses
Ref Expression
rmodislmod.v 𝑉 = (Base‘𝑅)
rmodislmod.a + = (+g𝑅)
rmodislmod.s · = ( ·𝑠𝑅)
rmodislmod.f 𝐹 = (Scalar‘𝑅)
rmodislmod.k 𝐾 = (Base‘𝐹)
rmodislmod.p = (+g𝐹)
rmodislmod.t × = (.r𝐹)
rmodislmod.u 1 = (1r𝐹)
rmodislmod.r (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))
rmodislmod.m = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠))
rmodislmod.l 𝐿 = (𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩)
Assertion
Ref Expression
rmodislmodlem ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → ((𝑎 × 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
Distinct variable groups:   × ,𝑞,𝑟,𝑤,𝑥   × ,𝑠,𝑣   · ,𝑞,𝑟,𝑤,𝑥   · ,𝑠,𝑣   𝐾,𝑞,𝑟,𝑥   𝐾,𝑠,𝑣   𝑉,𝑞,𝑟,𝑤,𝑥   𝑉,𝑠,𝑣   𝑟,𝑎,𝑤   𝑠,𝑎,𝑣   𝑞,𝑏,𝑟,𝑤   𝑠,𝑏,𝑣   𝑠,𝑐,𝑣   𝑤,𝑐
Allowed substitution hints:   + (𝑥,𝑤,𝑣,𝑠,𝑟,𝑞,𝑎,𝑏,𝑐)   (𝑥,𝑤,𝑣,𝑠,𝑟,𝑞,𝑎,𝑏,𝑐)   𝑅(𝑥,𝑤,𝑣,𝑠,𝑟,𝑞,𝑎,𝑏,𝑐)   · (𝑎,𝑏,𝑐)   × (𝑎,𝑏,𝑐)   1 (𝑥,𝑤,𝑣,𝑠,𝑟,𝑞,𝑎,𝑏,𝑐)   𝐹(𝑥,𝑤,𝑣,𝑠,𝑟,𝑞,𝑎,𝑏,𝑐)   (𝑥,𝑤,𝑣,𝑠,𝑟,𝑞,𝑎,𝑏,𝑐)   𝐾(𝑤,𝑎,𝑏,𝑐)   𝐿(𝑥,𝑤,𝑣,𝑠,𝑟,𝑞,𝑎,𝑏,𝑐)   𝑉(𝑎,𝑏,𝑐)

Proof of Theorem rmodislmodlem
StepHypRef Expression
1 rmodislmod.r . . . . 5 (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))
2 simprl 809 . . . . . . . . 9 ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
322ralimi 2982 . . . . . . . 8 (∀𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
432ralimi 2982 . . . . . . 7 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
5 ralrot3 3131 . . . . . . . . 9 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ↔ ∀𝑥𝑉𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
6 rmodislmod.v . . . . . . . . . . . . . 14 𝑉 = (Base‘𝑅)
76grpbn0 17498 . . . . . . . . . . . . 13 (𝑅 ∈ Grp → 𝑉 ≠ ∅)
873ad2ant1 1102 . . . . . . . . . . . 12 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → 𝑉 ≠ ∅)
91, 8ax-mp 5 . . . . . . . . . . 11 𝑉 ≠ ∅
10 rspn0 3967 . . . . . . . . . . 11 (𝑉 ≠ ∅ → (∀𝑥𝑉𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ∀𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟)))
119, 10ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑉𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ∀𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
12 oveq1 6697 . . . . . . . . . . . . . 14 (𝑞 = 𝑏 → (𝑞 × 𝑟) = (𝑏 × 𝑟))
1312oveq2d 6706 . . . . . . . . . . . . 13 (𝑞 = 𝑏 → (𝑤 · (𝑞 × 𝑟)) = (𝑤 · (𝑏 × 𝑟)))
14 oveq2 6698 . . . . . . . . . . . . . 14 (𝑞 = 𝑏 → (𝑤 · 𝑞) = (𝑤 · 𝑏))
1514oveq1d 6705 . . . . . . . . . . . . 13 (𝑞 = 𝑏 → ((𝑤 · 𝑞) · 𝑟) = ((𝑤 · 𝑏) · 𝑟))
1613, 15eqeq12d 2666 . . . . . . . . . . . 12 (𝑞 = 𝑏 → ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ↔ (𝑤 · (𝑏 × 𝑟)) = ((𝑤 · 𝑏) · 𝑟)))
17 oveq2 6698 . . . . . . . . . . . . . 14 (𝑟 = 𝑎 → (𝑏 × 𝑟) = (𝑏 × 𝑎))
1817oveq2d 6706 . . . . . . . . . . . . 13 (𝑟 = 𝑎 → (𝑤 · (𝑏 × 𝑟)) = (𝑤 · (𝑏 × 𝑎)))
19 oveq2 6698 . . . . . . . . . . . . 13 (𝑟 = 𝑎 → ((𝑤 · 𝑏) · 𝑟) = ((𝑤 · 𝑏) · 𝑎))
2018, 19eqeq12d 2666 . . . . . . . . . . . 12 (𝑟 = 𝑎 → ((𝑤 · (𝑏 × 𝑟)) = ((𝑤 · 𝑏) · 𝑟) ↔ (𝑤 · (𝑏 × 𝑎)) = ((𝑤 · 𝑏) · 𝑎)))
21 oveq1 6697 . . . . . . . . . . . . 13 (𝑤 = 𝑐 → (𝑤 · (𝑏 × 𝑎)) = (𝑐 · (𝑏 × 𝑎)))
22 oveq1 6697 . . . . . . . . . . . . . 14 (𝑤 = 𝑐 → (𝑤 · 𝑏) = (𝑐 · 𝑏))
2322oveq1d 6705 . . . . . . . . . . . . 13 (𝑤 = 𝑐 → ((𝑤 · 𝑏) · 𝑎) = ((𝑐 · 𝑏) · 𝑎))
2421, 23eqeq12d 2666 . . . . . . . . . . . 12 (𝑤 = 𝑐 → ((𝑤 · (𝑏 × 𝑎)) = ((𝑤 · 𝑏) · 𝑎) ↔ (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
2516, 20, 24rspc3v 3356 . . . . . . . . . . 11 ((𝑏𝐾𝑎𝐾𝑐𝑉) → (∀𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
26253com12 1288 . . . . . . . . . 10 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (∀𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
2711, 26syl5com 31 . . . . . . . . 9 (∀𝑥𝑉𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
285, 27sylbi 207 . . . . . . . 8 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
29 eqcom 2658 . . . . . . . 8 (((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)) ↔ (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎))
3028, 29syl6ibr 242 . . . . . . 7 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎))))
314, 30syl 17 . . . . . 6 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎))))
32313ad2ant3 1104 . . . . 5 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎))))
331, 32ax-mp 5 . . . 4 ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)))
3433adantl 481 . . 3 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)))
35 rmodislmod.k . . . . . . . . . 10 𝐾 = (Base‘𝐹)
36 rmodislmod.t . . . . . . . . . 10 × = (.r𝐹)
3735, 36crngcom 18608 . . . . . . . . 9 ((𝐹 ∈ CRing ∧ 𝑏𝐾𝑎𝐾) → (𝑏 × 𝑎) = (𝑎 × 𝑏))
38373expb 1285 . . . . . . . 8 ((𝐹 ∈ CRing ∧ (𝑏𝐾𝑎𝐾)) → (𝑏 × 𝑎) = (𝑎 × 𝑏))
3938expcom 450 . . . . . . 7 ((𝑏𝐾𝑎𝐾) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏)))
4039ancoms 468 . . . . . 6 ((𝑎𝐾𝑏𝐾) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏)))
41403adant3 1101 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏)))
4241impcom 445 . . . 4 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → (𝑏 × 𝑎) = (𝑎 × 𝑏))
4342oveq2d 6706 . . 3 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → (𝑐 · (𝑏 × 𝑎)) = (𝑐 · (𝑎 × 𝑏)))
4434, 43eqtrd 2685 . 2 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑎 × 𝑏)))
45 rmodislmod.m . . . . . . 7 = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠))
4645a1i 11 . . . . . 6 ((𝑎𝐾𝑏𝐾𝑐𝑉) → = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠)))
47 oveq12 6699 . . . . . . . 8 ((𝑣 = 𝑐𝑠 = 𝑏) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
4847ancoms 468 . . . . . . 7 ((𝑠 = 𝑏𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
4948adantl 481 . . . . . 6 (((𝑎𝐾𝑏𝐾𝑐𝑉) ∧ (𝑠 = 𝑏𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
50 simp2 1082 . . . . . 6 ((𝑎𝐾𝑏𝐾𝑐𝑉) → 𝑏𝐾)
51 simp3 1083 . . . . . 6 ((𝑎𝐾𝑏𝐾𝑐𝑉) → 𝑐𝑉)
52 ovexd 6720 . . . . . 6 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · 𝑏) ∈ V)
5346, 49, 50, 51, 52ovmpt2d 6830 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑏 𝑐) = (𝑐 · 𝑏))
5453oveq2d 6706 . . . 4 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑎 (𝑏 𝑐)) = (𝑎 (𝑐 · 𝑏)))
55 oveq12 6699 . . . . . . 7 ((𝑣 = (𝑐 · 𝑏) ∧ 𝑠 = 𝑎) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎))
5655ancoms 468 . . . . . 6 ((𝑠 = 𝑎𝑣 = (𝑐 · 𝑏)) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎))
5756adantl 481 . . . . 5 (((𝑎𝐾𝑏𝐾𝑐𝑉) ∧ (𝑠 = 𝑎𝑣 = (𝑐 · 𝑏))) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎))
58 simp1 1081 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → 𝑎𝐾)
59 simpl1 1084 . . . . . . . . . . 11 ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · 𝑟) ∈ 𝑉)
60592ralimi 2982 . . . . . . . . . 10 (∀𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
61602ralimi 2982 . . . . . . . . 9 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
62 ringgrp 18598 . . . . . . . . . . . . 13 (𝐹 ∈ Ring → 𝐹 ∈ Grp)
6335grpbn0 17498 . . . . . . . . . . . . 13 (𝐹 ∈ Grp → 𝐾 ≠ ∅)
6462, 63syl 17 . . . . . . . . . . . 12 (𝐹 ∈ Ring → 𝐾 ≠ ∅)
65643ad2ant2 1103 . . . . . . . . . . 11 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → 𝐾 ≠ ∅)
661, 65ax-mp 5 . . . . . . . . . 10 𝐾 ≠ ∅
67 rspn0 3967 . . . . . . . . . 10 (𝐾 ≠ ∅ → (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉))
6866, 67ax-mp 5 . . . . . . . . 9 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
69 ralcom 3127 . . . . . . . . . 10 (∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥𝑉𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
70 rspn0 3967 . . . . . . . . . . . 12 (𝑉 ≠ ∅ → (∀𝑥𝑉𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉))
719, 70ax-mp 5 . . . . . . . . . . 11 (∀𝑥𝑉𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
72 oveq2 6698 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → (𝑤 · 𝑟) = (𝑤 · 𝑏))
7372eleq1d 2715 . . . . . . . . . . . 12 (𝑟 = 𝑏 → ((𝑤 · 𝑟) ∈ 𝑉 ↔ (𝑤 · 𝑏) ∈ 𝑉))
7422eleq1d 2715 . . . . . . . . . . . 12 (𝑤 = 𝑐 → ((𝑤 · 𝑏) ∈ 𝑉 ↔ (𝑐 · 𝑏) ∈ 𝑉))
7573, 74rspc2v 3353 . . . . . . . . . . 11 ((𝑏𝐾𝑐𝑉) → (∀𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → (𝑐 · 𝑏) ∈ 𝑉))
7671, 75syl5com 31 . . . . . . . . . 10 (∀𝑥𝑉𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝑏𝐾𝑐𝑉) → (𝑐 · 𝑏) ∈ 𝑉))
7769, 76sylbi 207 . . . . . . . . 9 (∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝑏𝐾𝑐𝑉) → (𝑐 · 𝑏) ∈ 𝑉))
7861, 68, 773syl 18 . . . . . . . 8 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑏𝐾𝑐𝑉) → (𝑐 · 𝑏) ∈ 𝑉))
79783ad2ant3 1104 . . . . . . 7 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑏𝐾𝑐𝑉) → (𝑐 · 𝑏) ∈ 𝑉))
801, 79ax-mp 5 . . . . . 6 ((𝑏𝐾𝑐𝑉) → (𝑐 · 𝑏) ∈ 𝑉)
81803adant1 1099 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · 𝑏) ∈ 𝑉)
82 ovexd 6720 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑐 · 𝑏) · 𝑎) ∈ V)
8346, 57, 58, 81, 82ovmpt2d 6830 . . . 4 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑎 (𝑐 · 𝑏)) = ((𝑐 · 𝑏) · 𝑎))
8454, 83eqtrd 2685 . . 3 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑎 (𝑏 𝑐)) = ((𝑐 · 𝑏) · 𝑎))
8584adantl 481 . 2 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → (𝑎 (𝑏 𝑐)) = ((𝑐 · 𝑏) · 𝑎))
86 oveq12 6699 . . . . . 6 ((𝑣 = 𝑐𝑠 = (𝑎 × 𝑏)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏)))
8786ancoms 468 . . . . 5 ((𝑠 = (𝑎 × 𝑏) ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏)))
8887adantl 481 . . . 4 (((𝑎𝐾𝑏𝐾𝑐𝑉) ∧ (𝑠 = (𝑎 × 𝑏) ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏)))
8935, 36ringcl 18607 . . . . . . . 8 ((𝐹 ∈ Ring ∧ 𝑎𝐾𝑏𝐾) → (𝑎 × 𝑏) ∈ 𝐾)
90893expib 1287 . . . . . . 7 (𝐹 ∈ Ring → ((𝑎𝐾𝑏𝐾) → (𝑎 × 𝑏) ∈ 𝐾))
91903ad2ant2 1103 . . . . . 6 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎𝐾𝑏𝐾) → (𝑎 × 𝑏) ∈ 𝐾))
921, 91ax-mp 5 . . . . 5 ((𝑎𝐾𝑏𝐾) → (𝑎 × 𝑏) ∈ 𝐾)
93923adant3 1101 . . . 4 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑎 × 𝑏) ∈ 𝐾)
94 ovexd 6720 . . . 4 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑎 × 𝑏)) ∈ V)
9546, 88, 93, 51, 94ovmpt2d 6830 . . 3 ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑎 × 𝑏) 𝑐) = (𝑐 · (𝑎 × 𝑏)))
9695adantl 481 . 2 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → ((𝑎 × 𝑏) 𝑐) = (𝑐 · (𝑎 × 𝑏)))
9744, 85, 963eqtr4rd 2696 1 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → ((𝑎 × 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  Vcvv 3231  c0 3948  cop 4216  cfv 5926  (class class class)co 6690  cmpt2 6692  ndxcnx 15901   sSet csts 15902  Basecbs 15904  +gcplusg 15988  .rcmulr 15989  Scalarcsca 15991   ·𝑠 cvsca 15992  Grpcgrp 17469  1rcur 18547  Ringcrg 18593  CRingccrg 18594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-plusg 16001  df-0g 16149  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-grp 17472  df-cmn 18241  df-mgp 18536  df-ring 18595  df-cring 18596
This theorem is referenced by:  rmodislmod  18979
  Copyright terms: Public domain W3C validator