MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islmodd Structured version   Visualization version   GIF version
Theorem islmodd 20477
Description: Properties that determine a left module. See note in isgrpd2 18842 regarding the πœ‘ on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.)
Hypotheses
Ref Expression
islmodd.v (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘Š))
islmodd.a (πœ‘ β†’ + = (+gβ€˜π‘Š))
islmodd.f (πœ‘ β†’ 𝐹 = (Scalarβ€˜π‘Š))
islmodd.s (πœ‘ β†’ Β· = ( ·𝑠 β€˜π‘Š))
islmodd.b (πœ‘ β†’ 𝐡 = (Baseβ€˜πΉ))
islmodd.p (πœ‘ β†’ ⨣ = (+gβ€˜πΉ))
islmodd.t (πœ‘ β†’ Γ— = (.rβ€˜πΉ))
islmodd.u (πœ‘ β†’ 1 = (1rβ€˜πΉ))
islmodd.r (πœ‘ β†’ 𝐹 ∈ Ring)
islmodd.l (πœ‘ β†’ π‘Š ∈ Grp)
islmodd.w ((πœ‘ ∧ π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉) β†’ (π‘₯ Β· 𝑦) ∈ 𝑉)
islmodd.c ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) β†’ (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
islmodd.d ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
islmodd.e ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
islmodd.g ((πœ‘ ∧ π‘₯ ∈ 𝑉) β†’ ( 1 Β· π‘₯) = π‘₯)
Assertion
Ref Expression
islmodd (πœ‘ β†’ π‘Š ∈ LMod)
Distinct variable groups:   𝑦,𝑧, ⨣   π‘₯,𝑦,𝑧,𝐡   πœ‘,π‘₯,𝑦,𝑧   π‘₯,𝑉,𝑦,𝑧   π‘₯, + ,𝑦,𝑧   π‘₯,π‘Š   π‘₯, Β· ,𝑦,𝑧   𝑦, Γ— ,𝑧   π‘₯, 1
Allowed substitution hints:   ⨣ (π‘₯)   Γ— (π‘₯)   1 (𝑦,𝑧)   𝐹(π‘₯,𝑦,𝑧)   π‘Š(𝑦,𝑧)
Proof of Theorem islmodd
Dummy variables 𝑒 π‘Ÿ 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 islmodd.l . 2 (πœ‘ β†’ π‘Š ∈ Grp)
2 islmodd.f . . 3 (πœ‘ β†’ 𝐹 = (Scalarβ€˜π‘Š))
3 islmodd.r . . 3 (πœ‘ β†’ 𝐹 ∈ Ring)
42, 3eqeltrrd 2835 . 2 (πœ‘ β†’ (Scalarβ€˜π‘Š) ∈ Ring)
5 islmodd.w . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉) β†’ (π‘₯ Β· 𝑦) ∈ 𝑉)
653expb 1121 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉)) β†’ (π‘₯ Β· 𝑦) ∈ 𝑉)
76ralrimivva 3201 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉)
8 oveq1 7416 . . . . . . . . . . . 12 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· 𝑦) = (π‘Ÿ Β· 𝑦))
98eleq1d 2819 . . . . . . . . . . 11 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· 𝑦) ∈ 𝑉 ↔ (π‘Ÿ Β· 𝑦) ∈ 𝑉))
10 oveq2 7417 . . . . . . . . . . . 12 (𝑦 = 𝑀 β†’ (π‘Ÿ Β· 𝑦) = (π‘Ÿ Β· 𝑀))
1110eleq1d 2819 . . . . . . . . . . 11 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· 𝑦) ∈ 𝑉 ↔ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
129, 11rspc2v 3623 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉 β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
1312ad2ant2l 745 . . . . . . . . 9 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉 β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
147, 13mpan9 508 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉)
15 islmodd.c . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) β†’ (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
1615ralrimivvva 3204 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
17 oveq1 7416 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· (𝑦 + 𝑧)) = (π‘Ÿ Β· (𝑦 + 𝑧)))
18 oveq1 7416 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· 𝑧) = (π‘Ÿ Β· 𝑧))
198, 18oveq12d 7427 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)))
2017, 19eqeq12d 2749 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑦 + 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧))))
21 oveq1 7416 . . . . . . . . . . . . . . 15 (𝑦 = 𝑀 β†’ (𝑦 + 𝑧) = (𝑀 + 𝑧))
2221oveq2d 7425 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ (π‘Ÿ Β· (𝑦 + 𝑧)) = (π‘Ÿ Β· (𝑀 + 𝑧)))
2310oveq1d 7424 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)))
2422, 23eqeq12d 2749 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· (𝑦 + 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑀 + 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧))))
25 oveq2 7417 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ (𝑀 + 𝑧) = (𝑀 + 𝑒))
2625oveq2d 7425 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ (π‘Ÿ Β· (𝑀 + 𝑧)) = (π‘Ÿ Β· (𝑀 + 𝑒)))
27 oveq2 7417 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· 𝑒))
2827oveq2d 7425 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)))
2926, 28eqeq12d 2749 . . . . . . . . . . . . 13 (𝑧 = 𝑒 β†’ ((π‘Ÿ Β· (𝑀 + 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3020, 24, 29rspc3v 3628 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉 ∧ 𝑒 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
31303com23 1127 . . . . . . . . . . 11 ((π‘Ÿ ∈ 𝐡 ∧ 𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
32313expb 1121 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3332adantll 713 . . . . . . . . 9 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3416, 33mpan9 508 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)))
35 simpll 766 . . . . . . . . . 10 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ π‘₯ ∈ 𝐡)
36 islmodd.d . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
37363exp2 1355 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘₯ ∈ 𝐡 β†’ (𝑦 ∈ 𝐡 β†’ (𝑧 ∈ 𝑉 β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧))))))
3837imp43 429 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
3938ralrimivva 3201 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
4035, 39sylan2 594 . . . . . . . . 9 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
41 simprlr 779 . . . . . . . . . 10 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ π‘Ÿ ∈ 𝐡)
42 simprrr 781 . . . . . . . . . 10 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ 𝑀 ∈ 𝑉)
43 oveq2 7417 . . . . . . . . . . . . 13 (𝑦 = π‘Ÿ β†’ (π‘₯ ⨣ 𝑦) = (π‘₯ ⨣ π‘Ÿ))
4443oveq1d 7424 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧))
45 oveq1 7416 . . . . . . . . . . . . 13 (𝑦 = π‘Ÿ β†’ (𝑦 Β· 𝑧) = (π‘Ÿ Β· 𝑧))
4645oveq2d 7425 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)))
4744, 46eqeq12d 2749 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ (((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) ↔ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧))))
48 oveq2 7417 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀))
49 oveq2 7417 . . . . . . . . . . . . 13 (𝑧 = 𝑀 β†’ (π‘₯ Β· 𝑧) = (π‘₯ Β· 𝑀))
50 oveq2 7417 . . . . . . . . . . . . 13 (𝑧 = 𝑀 β†’ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· 𝑀))
5149, 50oveq12d 7427 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
5248, 51eqeq12d 2749 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ (((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)) ↔ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5347, 52rspc2v 3623 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5441, 42, 53syl2anc 585 . . . . . . . . 9 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5540, 54mpd 15 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
5614, 34, 553jca 1129 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
57 islmodd.e . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
58573exp2 1355 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ∈ 𝐡 β†’ (𝑦 ∈ 𝐡 β†’ (𝑧 ∈ 𝑉 β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧))))))
5958imp43 429 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
6059ralrimivva 3201 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
6135, 60sylan2 594 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
62 oveq2 7417 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ (π‘₯ Γ— 𝑦) = (π‘₯ Γ— π‘Ÿ))
6362oveq1d 7424 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = ((π‘₯ Γ— π‘Ÿ) Β· 𝑧))
6445oveq2d 7425 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ (π‘₯ Β· (𝑦 Β· 𝑧)) = (π‘₯ Β· (π‘Ÿ Β· 𝑧)))
6563, 64eqeq12d 2749 . . . . . . . . . 10 (𝑦 = π‘Ÿ β†’ (((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) ↔ ((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = (π‘₯ Β· (π‘Ÿ Β· 𝑧))))
66 oveq2 7417 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = ((π‘₯ Γ— π‘Ÿ) Β· 𝑀))
6750oveq2d 7425 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ (π‘₯ Β· (π‘Ÿ Β· 𝑧)) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)))
6866, 67eqeq12d 2749 . . . . . . . . . 10 (𝑧 = 𝑀 β†’ (((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = (π‘₯ Β· (π‘Ÿ Β· 𝑧)) ↔ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
6965, 68rspc2v 3623 . . . . . . . . 9 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
7041, 42, 69syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
7161, 70mpd 15 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)))
72 islmodd.g . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑉) β†’ ( 1 Β· π‘₯) = π‘₯)
7372ralrimiva 3147 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯)
74 oveq2 7417 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ ( 1 Β· π‘₯) = ( 1 Β· 𝑀))
75 id 22 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ π‘₯ = 𝑀)
7674, 75eqeq12d 2749 . . . . . . . . . 10 (π‘₯ = 𝑀 β†’ (( 1 Β· π‘₯) = π‘₯ ↔ ( 1 Β· 𝑀) = 𝑀))
7776rspcv 3609 . . . . . . . . 9 (𝑀 ∈ 𝑉 β†’ (βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯ β†’ ( 1 Β· 𝑀) = 𝑀))
7877ad2antll 728 . . . . . . . 8 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯ β†’ ( 1 Β· 𝑀) = 𝑀))
7973, 78mpan9 508 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ( 1 Β· 𝑀) = 𝑀)
8056, 71, 79jca32 517 . . . . . 6 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8180anassrs 469 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡)) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8281ralrimivva 3201 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡)) β†’ βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8382ralrimivva 3201 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
84 islmodd.b . . . . 5 (πœ‘ β†’ 𝐡 = (Baseβ€˜πΉ))
852fveq2d 6896 . . . . 5 (πœ‘ β†’ (Baseβ€˜πΉ) = (Baseβ€˜(Scalarβ€˜π‘Š)))
8684, 85eqtrd 2773 . . . 4 (πœ‘ β†’ 𝐡 = (Baseβ€˜(Scalarβ€˜π‘Š)))
87 islmodd.v . . . . . 6 (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘Š))
88 islmodd.s . . . . . . . . . . 11 (πœ‘ β†’ Β· = ( ·𝑠 β€˜π‘Š))
8988oveqd 7426 . . . . . . . . . 10 (πœ‘ β†’ (π‘Ÿ Β· 𝑀) = (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))
9089, 87eleq12d 2828 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ↔ (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š)))
91 eqidd 2734 . . . . . . . . . . 11 (πœ‘ β†’ π‘Ÿ = π‘Ÿ)
92 islmodd.a . . . . . . . . . . . 12 (πœ‘ β†’ + = (+gβ€˜π‘Š))
9392oveqd 7426 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀 + 𝑒) = (𝑀(+gβ€˜π‘Š)𝑒))
9488, 91, 93oveq123d 7430 . . . . . . . . . 10 (πœ‘ β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)))
9588oveqd 7426 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Ÿ Β· 𝑒) = (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒))
9692, 89, 95oveq123d 7430 . . . . . . . . . 10 (πœ‘ β†’ ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)))
9794, 96eqeq12d 2749 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ↔ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒))))
98 islmodd.p . . . . . . . . . . . . 13 (πœ‘ β†’ ⨣ = (+gβ€˜πΉ))
992fveq2d 6896 . . . . . . . . . . . . 13 (πœ‘ β†’ (+gβ€˜πΉ) = (+gβ€˜(Scalarβ€˜π‘Š)))
10098, 99eqtrd 2773 . . . . . . . . . . . 12 (πœ‘ β†’ ⨣ = (+gβ€˜(Scalarβ€˜π‘Š)))
101100oveqd 7426 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ⨣ π‘Ÿ) = (π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ))
102 eqidd 2734 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 = 𝑀)
10388, 101, 102oveq123d 7430 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀))
10488oveqd 7426 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ Β· 𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)𝑀))
10592, 104, 89oveq123d 7430 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))
106103, 105eqeq12d 2749 . . . . . . . . 9 (πœ‘ β†’ (((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)) ↔ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))))
10790, 97, 1063anbi123d 1437 . . . . . . . 8 (πœ‘ β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ↔ ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))))
108 islmodd.t . . . . . . . . . . . . 13 (πœ‘ β†’ Γ— = (.rβ€˜πΉ))
1092fveq2d 6896 . . . . . . . . . . . . 13 (πœ‘ β†’ (.rβ€˜πΉ) = (.rβ€˜(Scalarβ€˜π‘Š)))
110108, 109eqtrd 2773 . . . . . . . . . . . 12 (πœ‘ β†’ Γ— = (.rβ€˜(Scalarβ€˜π‘Š)))
111110oveqd 7426 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ Γ— π‘Ÿ) = (π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ))
11288, 111, 102oveq123d 7430 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = ((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀))
113 eqidd 2734 . . . . . . . . . . 11 (πœ‘ β†’ π‘₯ = π‘₯)
11488, 113, 89oveq123d 7430 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ Β· (π‘Ÿ Β· 𝑀)) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))
115112, 114eqeq12d 2749 . . . . . . . . 9 (πœ‘ β†’ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ↔ ((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))))
116 islmodd.u . . . . . . . . . . . 12 (πœ‘ β†’ 1 = (1rβ€˜πΉ))
1172fveq2d 6896 . . . . . . . . . . . 12 (πœ‘ β†’ (1rβ€˜πΉ) = (1rβ€˜(Scalarβ€˜π‘Š)))
118116, 117eqtrd 2773 . . . . . . . . . . 11 (πœ‘ β†’ 1 = (1rβ€˜(Scalarβ€˜π‘Š)))
11988, 118, 102oveq123d 7430 . . . . . . . . . 10 (πœ‘ β†’ ( 1 Β· 𝑀) = ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀))
120119eqeq1d 2735 . . . . . . . . 9 (πœ‘ β†’ (( 1 Β· 𝑀) = 𝑀 ↔ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))
121115, 120anbi12d 632 . . . . . . . 8 (πœ‘ β†’ ((((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀) ↔ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀)))
122107, 121anbi12d 632 . . . . . . 7 (πœ‘ β†’ ((((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ (((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12387, 122raleqbidv 3343 . . . . . 6 (πœ‘ β†’ (βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12487, 123raleqbidv 3343 . . . . 5 (πœ‘ β†’ (βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12586, 124raleqbidv 3343 . . . 4 (πœ‘ β†’ (βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12686, 125raleqbidv 3343 . . 3 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12783, 126mpbid 231 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀)))
128 eqid 2733 . . 3 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
129 eqid 2733 . . 3 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
130 eqid 2733 . . 3 ( ·𝑠 β€˜π‘Š) = ( ·𝑠 β€˜π‘Š)
131 eqid 2733 . . 3 (Scalarβ€˜π‘Š) = (Scalarβ€˜π‘Š)
132 eqid 2733 . . 3 (Baseβ€˜(Scalarβ€˜π‘Š)) = (Baseβ€˜(Scalarβ€˜π‘Š))
133 eqid 2733 . . 3 (+gβ€˜(Scalarβ€˜π‘Š)) = (+gβ€˜(Scalarβ€˜π‘Š))
134 eqid 2733 . . 3 (.rβ€˜(Scalarβ€˜π‘Š)) = (.rβ€˜(Scalarβ€˜π‘Š))
135 eqid 2733 . . 3 (1rβ€˜(Scalarβ€˜π‘Š)) = (1rβ€˜(Scalarβ€˜π‘Š))
136128, 129, 130, 131, 132, 133, 134, 135islmod 20475 . 2 (π‘Š ∈ LMod ↔ (π‘Š ∈ Grp ∧ (Scalarβ€˜π‘Š) ∈ Ring ∧ βˆ€π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
1371, 4, 127, 136syl3anbrc 1344 1 (πœ‘ β†’ π‘Š ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  β€˜cfv 6544  (class class class)co 7409  Basecbs 17144  +gcplusg 17197  .rcmulr 17198  Scalarcsca 17200   ·𝑠 cvsca 17201  Grpcgrp 18819  1rcur 20004  Ringcrg 20056  LModclmod 20471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-lmod 20473
This theorem is referenced by:  rmodislmod  20540  rmodislmodOLD  20541  islss3  20570  prdslmodd  20580  sralmod  20809  zlmlmod  21076  psrlmod  21521  cnlmod  24656  imaslmod  32468  lduallmodlem  38022  dvalveclem  39896  dvhlveclem  39979  mendlmod  41935
  Copyright terms: Public domain W3C validator