MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islmodd Structured version   Visualization version   GIF version
Theorem islmodd 20476
Description: Properties that determine a left module. See note in isgrpd2 18841 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 2834 . 2 (πœ‘ β†’ (Scalarβ€˜π‘Š) ∈ Ring)
5 islmodd.w . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉) β†’ (π‘₯ Β· 𝑦) ∈ 𝑉)
653expb 1120 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉)) β†’ (π‘₯ Β· 𝑦) ∈ 𝑉)
76ralrimivva 3200 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉)
8 oveq1 7415 . . . . . . . . . . . 12 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· 𝑦) = (π‘Ÿ Β· 𝑦))
98eleq1d 2818 . . . . . . . . . . 11 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· 𝑦) ∈ 𝑉 ↔ (π‘Ÿ Β· 𝑦) ∈ 𝑉))
10 oveq2 7416 . . . . . . . . . . . 12 (𝑦 = 𝑀 β†’ (π‘Ÿ Β· 𝑦) = (π‘Ÿ Β· 𝑀))
1110eleq1d 2818 . . . . . . . . . . 11 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· 𝑦) ∈ 𝑉 ↔ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
129, 11rspc2v 3622 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉 β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
1312ad2ant2l 744 . . . . . . . . 9 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 (π‘₯ Β· 𝑦) ∈ 𝑉 β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
147, 13mpan9 507 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (π‘Ÿ Β· 𝑀) ∈ 𝑉)
15 islmodd.c . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) β†’ (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
1615ralrimivvva 3203 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
17 oveq1 7415 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· (𝑦 + 𝑧)) = (π‘Ÿ Β· (𝑦 + 𝑧)))
18 oveq1 7415 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (π‘₯ Β· 𝑧) = (π‘Ÿ Β· 𝑧))
198, 18oveq12d 7426 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)))
2017, 19eqeq12d 2748 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ ((π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑦 + 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧))))
21 oveq1 7415 . . . . . . . . . . . . . . 15 (𝑦 = 𝑀 β†’ (𝑦 + 𝑧) = (𝑀 + 𝑧))
2221oveq2d 7424 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ (π‘Ÿ Β· (𝑦 + 𝑧)) = (π‘Ÿ Β· (𝑀 + 𝑧)))
2310oveq1d 7423 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)))
2422, 23eqeq12d 2748 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ ((π‘Ÿ Β· (𝑦 + 𝑧)) = ((π‘Ÿ Β· 𝑦) + (π‘Ÿ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑀 + 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧))))
25 oveq2 7416 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ (𝑀 + 𝑧) = (𝑀 + 𝑒))
2625oveq2d 7424 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ (π‘Ÿ Β· (𝑀 + 𝑧)) = (π‘Ÿ Β· (𝑀 + 𝑒)))
27 oveq2 7416 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· 𝑒))
2827oveq2d 7424 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)))
2926, 28eqeq12d 2748 . . . . . . . . . . . . 13 (𝑧 = 𝑒 β†’ ((π‘Ÿ Β· (𝑀 + 𝑧)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑧)) ↔ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3020, 24, 29rspc3v 3627 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉 ∧ 𝑒 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
31303com23 1126 . . . . . . . . . . 11 ((π‘Ÿ ∈ 𝐡 ∧ 𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
32313expb 1120 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3332adantll 712 . . . . . . . . 9 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝑉 βˆ€π‘§ ∈ 𝑉 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒))))
3416, 33mpan9 507 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)))
35 simpll 765 . . . . . . . . . 10 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ π‘₯ ∈ 𝐡)
36 islmodd.d . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
37363exp2 1354 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘₯ ∈ 𝐡 β†’ (𝑦 ∈ 𝐡 β†’ (𝑧 ∈ 𝑉 β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧))))))
3837imp43 428 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
3938ralrimivva 3200 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
4035, 39sylan2 593 . . . . . . . . 9 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
41 simprlr 778 . . . . . . . . . 10 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ π‘Ÿ ∈ 𝐡)
42 simprrr 780 . . . . . . . . . 10 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ 𝑀 ∈ 𝑉)
43 oveq2 7416 . . . . . . . . . . . . 13 (𝑦 = π‘Ÿ β†’ (π‘₯ ⨣ 𝑦) = (π‘₯ ⨣ π‘Ÿ))
4443oveq1d 7423 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧))
45 oveq1 7415 . . . . . . . . . . . . 13 (𝑦 = π‘Ÿ β†’ (𝑦 Β· 𝑧) = (π‘Ÿ Β· 𝑧))
4645oveq2d 7424 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)))
4744, 46eqeq12d 2748 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ (((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) ↔ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧))))
48 oveq2 7416 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀))
49 oveq2 7416 . . . . . . . . . . . . 13 (𝑧 = 𝑀 β†’ (π‘₯ Β· 𝑧) = (π‘₯ Β· 𝑀))
50 oveq2 7416 . . . . . . . . . . . . 13 (𝑧 = 𝑀 β†’ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· 𝑀))
5149, 50oveq12d 7426 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
5248, 51eqeq12d 2748 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ (((π‘₯ ⨣ π‘Ÿ) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (π‘Ÿ Β· 𝑧)) ↔ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5347, 52rspc2v 3622 . . . . . . . . . 10 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5441, 42, 53syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ ⨣ 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
5540, 54mpd 15 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
5614, 34, 553jca 1128 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
57 islmodd.e . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
58573exp2 1354 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ∈ 𝐡 β†’ (𝑦 ∈ 𝐡 β†’ (𝑧 ∈ 𝑉 β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧))))))
5958imp43 428 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝑉)) β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
6059ralrimivva 3200 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
6135, 60sylan2 593 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)))
62 oveq2 7416 . . . . . . . . . . . 12 (𝑦 = π‘Ÿ β†’ (π‘₯ Γ— 𝑦) = (π‘₯ Γ— π‘Ÿ))
6362oveq1d 7423 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ ((π‘₯ Γ— 𝑦) Β· 𝑧) = ((π‘₯ Γ— π‘Ÿ) Β· 𝑧))
6445oveq2d 7424 . . . . . . . . . . 11 (𝑦 = π‘Ÿ β†’ (π‘₯ Β· (𝑦 Β· 𝑧)) = (π‘₯ Β· (π‘Ÿ Β· 𝑧)))
6563, 64eqeq12d 2748 . . . . . . . . . 10 (𝑦 = π‘Ÿ β†’ (((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) ↔ ((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = (π‘₯ Β· (π‘Ÿ Β· 𝑧))))
66 oveq2 7416 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = ((π‘₯ Γ— π‘Ÿ) Β· 𝑀))
6750oveq2d 7424 . . . . . . . . . . 11 (𝑧 = 𝑀 β†’ (π‘₯ Β· (π‘Ÿ Β· 𝑧)) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)))
6866, 67eqeq12d 2748 . . . . . . . . . 10 (𝑧 = 𝑀 β†’ (((π‘₯ Γ— π‘Ÿ) Β· 𝑧) = (π‘₯ Β· (π‘Ÿ Β· 𝑧)) ↔ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
6965, 68rspc2v 3622 . . . . . . . . 9 ((π‘Ÿ ∈ 𝐡 ∧ 𝑀 ∈ 𝑉) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
7041, 42, 69syl2anc 584 . . . . . . . 8 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑉 ((π‘₯ Γ— 𝑦) Β· 𝑧) = (π‘₯ Β· (𝑦 Β· 𝑧)) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀))))
7161, 70mpd 15 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)))
72 islmodd.g . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑉) β†’ ( 1 Β· π‘₯) = π‘₯)
7372ralrimiva 3146 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯)
74 oveq2 7416 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ ( 1 Β· π‘₯) = ( 1 Β· 𝑀))
75 id 22 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ π‘₯ = 𝑀)
7674, 75eqeq12d 2748 . . . . . . . . . 10 (π‘₯ = 𝑀 β†’ (( 1 Β· π‘₯) = π‘₯ ↔ ( 1 Β· 𝑀) = 𝑀))
7776rspcv 3608 . . . . . . . . 9 (𝑀 ∈ 𝑉 β†’ (βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯ β†’ ( 1 Β· 𝑀) = 𝑀))
7877ad2antll 727 . . . . . . . 8 (((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (βˆ€π‘₯ ∈ 𝑉 ( 1 Β· π‘₯) = π‘₯ β†’ ( 1 Β· 𝑀) = 𝑀))
7973, 78mpan9 507 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ ( 1 Β· 𝑀) = 𝑀)
8056, 71, 79jca32 516 . . . . . 6 ((πœ‘ ∧ ((π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉))) β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8180anassrs 468 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡)) ∧ (𝑒 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉)) β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8281ralrimivva 3200 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡)) β†’ βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
8382ralrimivva 3200 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
84 islmodd.b . . . . 5 (πœ‘ β†’ 𝐡 = (Baseβ€˜πΉ))
852fveq2d 6895 . . . . 5 (πœ‘ β†’ (Baseβ€˜πΉ) = (Baseβ€˜(Scalarβ€˜π‘Š)))
8684, 85eqtrd 2772 . . . 4 (πœ‘ β†’ 𝐡 = (Baseβ€˜(Scalarβ€˜π‘Š)))
87 islmodd.v . . . . . 6 (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘Š))
88 islmodd.s . . . . . . . . . . 11 (πœ‘ β†’ Β· = ( ·𝑠 β€˜π‘Š))
8988oveqd 7425 . . . . . . . . . 10 (πœ‘ β†’ (π‘Ÿ Β· 𝑀) = (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))
9089, 87eleq12d 2827 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ↔ (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š)))
91 eqidd 2733 . . . . . . . . . . 11 (πœ‘ β†’ π‘Ÿ = π‘Ÿ)
92 islmodd.a . . . . . . . . . . . 12 (πœ‘ β†’ + = (+gβ€˜π‘Š))
9392oveqd 7425 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀 + 𝑒) = (𝑀(+gβ€˜π‘Š)𝑒))
9488, 91, 93oveq123d 7429 . . . . . . . . . 10 (πœ‘ β†’ (π‘Ÿ Β· (𝑀 + 𝑒)) = (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)))
9588oveqd 7425 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Ÿ Β· 𝑒) = (π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒))
9692, 89, 95oveq123d 7429 . . . . . . . . . 10 (πœ‘ β†’ ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)))
9794, 96eqeq12d 2748 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ↔ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒))))
98 islmodd.p . . . . . . . . . . . . 13 (πœ‘ β†’ ⨣ = (+gβ€˜πΉ))
992fveq2d 6895 . . . . . . . . . . . . 13 (πœ‘ β†’ (+gβ€˜πΉ) = (+gβ€˜(Scalarβ€˜π‘Š)))
10098, 99eqtrd 2772 . . . . . . . . . . . 12 (πœ‘ β†’ ⨣ = (+gβ€˜(Scalarβ€˜π‘Š)))
101100oveqd 7425 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ⨣ π‘Ÿ) = (π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ))
102 eqidd 2733 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 = 𝑀)
10388, 101, 102oveq123d 7429 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀))
10488oveqd 7425 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ Β· 𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)𝑀))
10592, 104, 89oveq123d 7429 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))
106103, 105eqeq12d 2748 . . . . . . . . 9 (πœ‘ β†’ (((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀)) ↔ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))))
10790, 97, 1063anbi123d 1436 . . . . . . . 8 (πœ‘ β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ↔ ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))))
108 islmodd.t . . . . . . . . . . . . 13 (πœ‘ β†’ Γ— = (.rβ€˜πΉ))
1092fveq2d 6895 . . . . . . . . . . . . 13 (πœ‘ β†’ (.rβ€˜πΉ) = (.rβ€˜(Scalarβ€˜π‘Š)))
110108, 109eqtrd 2772 . . . . . . . . . . . 12 (πœ‘ β†’ Γ— = (.rβ€˜(Scalarβ€˜π‘Š)))
111110oveqd 7425 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ Γ— π‘Ÿ) = (π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ))
11288, 111, 102oveq123d 7429 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = ((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀))
113 eqidd 2733 . . . . . . . . . . 11 (πœ‘ β†’ π‘₯ = π‘₯)
11488, 113, 89oveq123d 7429 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ Β· (π‘Ÿ Β· 𝑀)) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)))
115112, 114eqeq12d 2748 . . . . . . . . 9 (πœ‘ β†’ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ↔ ((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))))
116 islmodd.u . . . . . . . . . . . 12 (πœ‘ β†’ 1 = (1rβ€˜πΉ))
1172fveq2d 6895 . . . . . . . . . . . 12 (πœ‘ β†’ (1rβ€˜πΉ) = (1rβ€˜(Scalarβ€˜π‘Š)))
118116, 117eqtrd 2772 . . . . . . . . . . 11 (πœ‘ β†’ 1 = (1rβ€˜(Scalarβ€˜π‘Š)))
11988, 118, 102oveq123d 7429 . . . . . . . . . 10 (πœ‘ β†’ ( 1 Β· 𝑀) = ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀))
120119eqeq1d 2734 . . . . . . . . 9 (πœ‘ β†’ (( 1 Β· 𝑀) = 𝑀 ↔ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))
121115, 120anbi12d 631 . . . . . . . 8 (πœ‘ β†’ ((((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀) ↔ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀)))
122107, 121anbi12d 631 . . . . . . 7 (πœ‘ β†’ ((((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ (((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12387, 122raleqbidv 3342 . . . . . 6 (πœ‘ β†’ (βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12487, 123raleqbidv 3342 . . . . 5 (πœ‘ β†’ (βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12586, 124raleqbidv 3342 . . . 4 (πœ‘ β†’ (βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘’ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + 𝑒)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· 𝑒)) ∧ ((π‘₯ ⨣ π‘Ÿ) Β· 𝑀) = ((π‘₯ Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘₯ Γ— π‘Ÿ) Β· 𝑀) = (π‘₯ Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)) ↔ βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘’ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)𝑒)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑒)) ∧ ((π‘₯(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘₯( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘₯(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘₯( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
12686, 125raleqbidv 3342 . . 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 2732 . . 3 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
129 eqid 2732 . . 3 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
130 eqid 2732 . . 3 ( ·𝑠 β€˜π‘Š) = ( ·𝑠 β€˜π‘Š)
131 eqid 2732 . . 3 (Scalarβ€˜π‘Š) = (Scalarβ€˜π‘Š)
132 eqid 2732 . . 3 (Baseβ€˜(Scalarβ€˜π‘Š)) = (Baseβ€˜(Scalarβ€˜π‘Š))
133 eqid 2732 . . 3 (+gβ€˜(Scalarβ€˜π‘Š)) = (+gβ€˜(Scalarβ€˜π‘Š))
134 eqid 2732 . . 3 (.rβ€˜(Scalarβ€˜π‘Š)) = (.rβ€˜(Scalarβ€˜π‘Š))
135 eqid 2732 . . 3 (1rβ€˜(Scalarβ€˜π‘Š)) = (1rβ€˜(Scalarβ€˜π‘Š))
136128, 129, 130, 131, 132, 133, 134, 135islmod 20474 . 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 1343 1 (πœ‘ β†’ π‘Š ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  β€˜cfv 6543  (class class class)co 7408  Basecbs 17143  +gcplusg 17196  .rcmulr 17197  Scalarcsca 17199   ·𝑠 cvsca 17200  Grpcgrp 18818  1rcur 20003  Ringcrg 20055  LModclmod 20470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411  df-lmod 20472
This theorem is referenced by:  rmodislmod  20539  rmodislmodOLD  20540  islss3  20569  prdslmodd  20579  sralmod  20808  zlmlmod  21075  psrlmod  21520  cnlmod  24655  imaslmod  32463  lduallmodlem  38017  dvalveclem  39891  dvhlveclem  39974  mendlmod  41925
  Copyright terms: Public domain W3C validator