ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  islmodd GIF version
Theorem islmodd 13388
Description: Properties that determine a left module. See note in isgrpd2 12902 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 2255 . 2 (πœ‘ β†’ (Scalarβ€˜π‘Š) ∈ Ring)
5 islmodd.w . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉) β†’ (π‘₯ Β· 𝑦) ∈ 𝑉)
653expb 1204 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉)) β†’ (π‘₯ Β· 𝑦) ∈ 𝑉)
76ralrimivva 2559 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉)
8 oveq1 5884 . . . . . . . . . . . 12 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· 𝑦) = (π‘Ÿ Β· 𝑦))
98eleq1d 2246 . . . . . . . . . . 11 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· 𝑦) ∈ 𝑉 ↔ (π‘Ÿ Β· 𝑦) ∈ 𝑉))
10 oveq2 5885 . . . . . . . . . . . 12 (𝑦 = 𝑀 β†’ (π‘Ÿ Β· 𝑦) = (π‘Ÿ Β· 𝑀))
1110eleq1d 2246 . . . . . . . . . . 11 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· 𝑦) ∈ 𝑉 ↔ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
129, 11rspc2v 2856 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉 β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
1312ad2ant2l 508 . . . . . . . . 9 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉 β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
147, 13mpan9 281 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉)
15 islmodd.c . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) β†’ (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
1615ralrimivvva 2560 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
17 oveq1 5884 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· (𝑦 + 𝑧)) = (π‘Ÿ Β· (𝑦 + 𝑧)))
18 oveq1 5884 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· 𝑧) = (π‘Ÿ Β· 𝑧))
198, 18oveq12d 5895 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)))
2017, 19eqeq12d 2192 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑦 + 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧))))
21 oveq1 5884 . . . . . . . . . . . . . . 15 (𝑦 = 𝑀 β†’ (𝑦 + 𝑧) = (𝑀 + 𝑧))
2221oveq2d 5893 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ (π‘Ÿ Β· (𝑦 + 𝑧)) = (π‘Ÿ Β· (𝑀 + 𝑧)))
2310oveq1d 5892 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)))
2422, 23eqeq12d 2192 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· (𝑦 + 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑀 + 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧))))
25 oveq2 5885 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ (𝑀 + 𝑧) = (𝑀 + 𝑒))
2625oveq2d 5893 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ (π‘Ÿ Β· (𝑀 + 𝑧)) = (π‘Ÿ Β· (𝑀 + 𝑒)))
27 oveq2 5885 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· 𝑒))
2827oveq2d 5893 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)))
2926, 28eqeq12d 2192 . . . . . . . . . . . . 13 (𝑧 = 𝑒 β†’ ((π‘Ÿ Β· (𝑀 + 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3020, 24, 29rspc3v 2859 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉 ∧ 𝑒 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
31303com23 1209 . . . . . . . . . . 11 ((π‘Ÿ ∈ 𝐡 ∧ 𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
32313expb 1204 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3332adantll 476 . . . . . . . . 9 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3416, 33mpan9 281 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)))
35 simpll 527 . . . . . . . . . 10 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ π‘₯ ∈ 𝐡)
36 islmodd.d . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
37363exp2 1225 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘₯ ∈ 𝐡 β†’ (𝑦 ∈ 𝐡 β†’ (𝑧 ∈ 𝑉 β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧))))))
3837imp43 355 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
3938ralrimivva 2559 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
4035, 39sylan2 286 . . . . . . . . 9 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
41 simprlr 538 . . . . . . . . . 10 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ π‘Ÿ ∈ 𝐡)
42 simprrr 540 . . . . . . . . . 10 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ 𝑀 ∈ 𝑉)
43 oveq2 5885 . . . . . . . . . . . . 13 (𝑦 = π‘Ÿ β†’ (π‘₯ ⨣ 𝑦) = (π‘₯ ⨣ π‘Ÿ))
4443oveq1d 5892 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧))
45 oveq1 5884 . . . . . . . . . . . . 13 (𝑦 = π‘Ÿ β†’ (𝑦 Β· 𝑧) = (π‘Ÿ Β· 𝑧))
4645oveq2d 5893 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)))
4744, 46eqeq12d 2192 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ (((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) ↔ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧))))
48 oveq2 5885 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀))
49 oveq2 5885 . . . . . . . . . . . . 13 (𝑧 = 𝑀 β†’ (π‘₯ Β· 𝑧) = (π‘₯ Β· 𝑀))
50 oveq2 5885 . . . . . . . . . . . . 13 (𝑧 = 𝑀 β†’ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· 𝑀))
5149, 50oveq12d 5895 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
5248, 51eqeq12d 2192 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ (((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)) ↔ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5347, 52rspc2v 2856 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5441, 42, 53syl2anc 411 . . . . . . . . 9 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5540, 54mpd 13 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
5614, 34, 553jca 1177 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
57 islmodd.e . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
58573exp2 1225 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ∈ 𝐡 β†’ (𝑦 ∈ 𝐡 β†’ (𝑧 ∈ 𝑉 β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧))))))
5958imp43 355 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
6059ralrimivva 2559 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
6135, 60sylan2 286 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
62 oveq2 5885 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ (π‘₯ Γ— 𝑦) = (π‘₯ Γ— π‘Ÿ))
6362oveq1d 5892 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = ((π‘₯ Γ— π‘Ÿ) Β· 𝑧))
6445oveq2d 5893 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ (π‘₯ Β· (𝑦 Β· 𝑧)) = (π‘₯ Β· (π‘Ÿ Β· 𝑧)))
6563, 64eqeq12d 2192 . . . . . . . . . 10 (𝑦 = π‘Ÿ β†’ (((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) ↔ ((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = (π‘₯ Β· (π‘Ÿ Β· 𝑧))))
66 oveq2 5885 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = ((π‘₯ Γ— π‘Ÿ) Β· 𝑀))
6750oveq2d 5893 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ (π‘₯ Β· (π‘Ÿ Β· 𝑧)) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)))
6866, 67eqeq12d 2192 . . . . . . . . . 10 (𝑧 = 𝑀 β†’ (((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = (π‘₯ Β· (π‘Ÿ Β· 𝑧)) ↔ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
6965, 68rspc2v 2856 . . . . . . . . 9 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
7041, 42, 69syl2anc 411 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
7161, 70mpd 13 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)))
72 islmodd.g . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑉) β†’ ( 1 Β· π‘₯) = π‘₯)
7372ralrimiva 2550 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯)
74 oveq2 5885 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ ( 1 Β· π‘₯) = ( 1 Β· 𝑀))
75 id 19 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ π‘₯ = 𝑀)
7674, 75eqeq12d 2192 . . . . . . . . . 10 (π‘₯ = 𝑀 β†’ (( 1 Β· π‘₯) = π‘₯ ↔ ( 1 Β· 𝑀) = 𝑀))
7776rspcv 2839 . . . . . . . . 9 (𝑀 ∈ 𝑉 β†’ (βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯ β†’ ( 1 Β· 𝑀) = 𝑀))
7877ad2antll 491 . . . . . . . 8 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯ β†’ ( 1 Β· 𝑀) = 𝑀))
7973, 78mpan9 281 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ( 1 Β· 𝑀) = 𝑀)
8056, 71, 79jca32 310 . . . . . 6 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8180anassrs 400 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡)) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8281ralrimivva 2559 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡)) β†’ βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8382ralrimivva 2559 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
84 islmodd.b . . . . 5 (πœ‘ β†’ 𝐡 = (Baseβ€˜πΉ))
852fveq2d 5521 . . . . 5 (πœ‘ β†’ (Baseβ€˜πΉ) = (Baseβ€˜(Scalarβ€˜π‘Š)))
8684, 85eqtrd 2210 . . . 4 (πœ‘ β†’ 𝐡 = (Baseβ€˜(Scalarβ€˜π‘Š)))
87 islmodd.v . . . . . 6 (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘Š))
88 islmodd.s . . . . . . . . . . 11 (πœ‘ β†’ Β· = ( ·𝑠 β€˜π‘Š))
8988oveqd 5894 . . . . . . . . . 10 (πœ‘ β†’ (π‘Ÿ Β· 𝑀) = (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))
9089, 87eleq12d 2248 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ↔ (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š)))
91 eqidd 2178 . . . . . . . . . . 11 (πœ‘ β†’ π‘Ÿ = π‘Ÿ)
92 islmodd.a . . . . . . . . . . . 12 (πœ‘ β†’ + = (+gβ€˜π‘Š))
9392oveqd 5894 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀 + 𝑒) = (𝑀(+gβ€˜π‘Š)𝑒))
9488, 91, 93oveq123d 5898 . . . . . . . . . 10 (πœ‘ β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)))
9588oveqd 5894 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Ÿ Β· 𝑒) = (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒))
9692, 89, 95oveq123d 5898 . . . . . . . . . 10 (πœ‘ β†’ ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)))
9794, 96eqeq12d 2192 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ↔ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒))))
98 islmodd.p . . . . . . . . . . . . 13 (πœ‘ β†’ ⨣ = (+gβ€˜πΉ))
992fveq2d 5521 . . . . . . . . . . . . 13 (πœ‘ β†’ (+gβ€˜πΉ) = (+gβ€˜(Scalarβ€˜π‘Š)))
10098, 99eqtrd 2210 . . . . . . . . . . . 12 (πœ‘ β†’ ⨣ = (+gβ€˜(Scalarβ€˜π‘Š)))
101100oveqd 5894 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ⨣ π‘Ÿ) = (π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ))
102 eqidd 2178 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 = 𝑀)
10388, 101, 102oveq123d 5898 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀))
10488oveqd 5894 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ Β· 𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)𝑀))
10592, 104, 89oveq123d 5898 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))
106103, 105eqeq12d 2192 . . . . . . . . 9 (πœ‘ β†’ (((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)) ↔ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))))
10790, 97, 1063anbi123d 1312 . . . . . . . 8 (πœ‘ β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ↔ ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))))
108 islmodd.t . . . . . . . . . . . . 13 (πœ‘ β†’ Γ— = (.rβ€˜πΉ))
1092fveq2d 5521 . . . . . . . . . . . . 13 (πœ‘ β†’ (.rβ€˜πΉ) = (.rβ€˜(Scalarβ€˜π‘Š)))
110108, 109eqtrd 2210 . . . . . . . . . . . 12 (πœ‘ β†’ Γ— = (.rβ€˜(Scalarβ€˜π‘Š)))
111110oveqd 5894 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ Γ— π‘Ÿ) = (π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ))
11288, 111, 102oveq123d 5898 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = ((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀))
113 eqidd 2178 . . . . . . . . . . 11 (πœ‘ β†’ π‘₯ = π‘₯)
11488, 113, 89oveq123d 5898 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ Β· (π‘Ÿ Β· 𝑀)) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))
115112, 114eqeq12d 2192 . . . . . . . . 9 (πœ‘ β†’ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ↔ ((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))))
116 islmodd.u . . . . . . . . . . . 12 (πœ‘ β†’ 1 = (1rβ€˜πΉ))
1172fveq2d 5521 . . . . . . . . . . . 12 (πœ‘ β†’ (1rβ€˜πΉ) = (1rβ€˜(Scalarβ€˜π‘Š)))
118116, 117eqtrd 2210 . . . . . . . . . . 11 (πœ‘ β†’ 1 = (1rβ€˜(Scalarβ€˜π‘Š)))
11988, 118, 102oveq123d 5898 . . . . . . . . . 10 (πœ‘ β†’ ( 1 Β· 𝑀) = ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀))
120119eqeq1d 2186 . . . . . . . . 9 (πœ‘ β†’ (( 1 Β· 𝑀) = 𝑀 ↔ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))
121115, 120anbi12d 473 . . . . . . . 8 (πœ‘ β†’ ((((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀) ↔ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀)))
122107, 121anbi12d 473 . . . . . . 7 (πœ‘ β†’ ((((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ (((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12387, 122raleqbidv 2685 . . . . . 6 (πœ‘ β†’ (βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12487, 123raleqbidv 2685 . . . . 5 (πœ‘ β†’ (βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12586, 124raleqbidv 2685 . . . 4 (πœ‘ β†’ (βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12686, 125raleqbidv 2685 . . 3 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12783, 126mpbid 147 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀)))
128 eqid 2177 . . 3 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
129 eqid 2177 . . 3 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
130 eqid 2177 . . 3 ( ·𝑠 β€˜π‘Š) = ( ·𝑠 β€˜π‘Š)
131 eqid 2177 . . 3 (Scalarβ€˜π‘Š) = (Scalarβ€˜π‘Š)
132 eqid 2177 . . 3 (Baseβ€˜(Scalarβ€˜π‘Š)) = (Baseβ€˜(Scalarβ€˜π‘Š))
133 eqid 2177 . . 3 (+gβ€˜(Scalarβ€˜π‘Š)) = (+gβ€˜(Scalarβ€˜π‘Š))
134 eqid 2177 . . 3 (.rβ€˜(Scalarβ€˜π‘Š)) = (.rβ€˜(Scalarβ€˜π‘Š))
135 eqid 2177 . . 3 (1rβ€˜(Scalarβ€˜π‘Š)) = (1rβ€˜(Scalarβ€˜π‘Š))
136128, 129, 130, 131, 132, 133, 134, 135islmod 13386 . 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 1181 1 (πœ‘ β†’ π‘Š ∈ LMod)
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ∧ w3a 978   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455  β€˜cfv 5218  (class class class)co 5877  Basecbs 12464  +gcplusg 12538  .rcmulr 12539  Scalarcsca 12541   ·𝑠 cvsca 12542  Grpcgrp 12882  1rcur 13147  Ringcrg 13184  LModclmod 13382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-cnex 7904  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-sbc 2965  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-iota 5180  df-fun 5220  df-fn 5221  df-fv 5226  df-ov 5880  df-inn 8922  df-2 8980  df-3 8981  df-4 8982  df-5 8983  df-6 8984  df-ndx 12467  df-slot 12468  df-base 12470  df-plusg 12551  df-mulr 12552  df-sca 12554  df-vsca 12555  df-lmod 13384
This theorem is referenced by:  rmodislmod  13446  islss3  13471
  Copyright terms: Public domain W3C validator