Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  slmdlema Structured version   Visualization version   GIF version

Theorem slmdlema 32854
Description: Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
Hypotheses
Ref Expression
isslmd.v 𝑉 = (Baseβ€˜π‘Š)
isslmd.a + = (+gβ€˜π‘Š)
isslmd.s Β· = ( ·𝑠 β€˜π‘Š)
isslmd.0 0 = (0gβ€˜π‘Š)
isslmd.f 𝐹 = (Scalarβ€˜π‘Š)
isslmd.k 𝐾 = (Baseβ€˜πΉ)
isslmd.p ⨣ = (+gβ€˜πΉ)
isslmd.t Γ— = (.rβ€˜πΉ)
isslmd.u 1 = (1rβ€˜πΉ)
isslmd.o 𝑂 = (0gβ€˜πΉ)
Assertion
Ref Expression
slmdlema ((π‘Š ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ π‘Œ ∈ 𝑉)) β†’ (((𝑅 Β· π‘Œ) ∈ 𝑉 ∧ (𝑅 Β· (π‘Œ + 𝑋)) = ((𝑅 Β· π‘Œ) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· π‘Œ) = ((𝑄 Β· π‘Œ) + (𝑅 Β· π‘Œ))) ∧ (((𝑄 Γ— 𝑅) Β· π‘Œ) = (𝑄 Β· (𝑅 Β· π‘Œ)) ∧ ( 1 Β· π‘Œ) = π‘Œ ∧ (𝑂 Β· π‘Œ) = 0 )))

Proof of Theorem slmdlema
Dummy variables π‘ž π‘Ÿ 𝑀 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isslmd.v . . . . . 6 𝑉 = (Baseβ€˜π‘Š)
2 isslmd.a . . . . . 6 + = (+gβ€˜π‘Š)
3 isslmd.s . . . . . 6 Β· = ( ·𝑠 β€˜π‘Š)
4 isslmd.0 . . . . . 6 0 = (0gβ€˜π‘Š)
5 isslmd.f . . . . . 6 𝐹 = (Scalarβ€˜π‘Š)
6 isslmd.k . . . . . 6 𝐾 = (Baseβ€˜πΉ)
7 isslmd.p . . . . . 6 ⨣ = (+gβ€˜πΉ)
8 isslmd.t . . . . . 6 Γ— = (.rβ€˜πΉ)
9 isslmd.u . . . . . 6 1 = (1rβ€˜πΉ)
10 isslmd.o . . . . . 6 𝑂 = (0gβ€˜πΉ)
111, 2, 3, 4, 5, 6, 7, 8, 9, 10isslmd 32853 . . . . 5 (π‘Š ∈ SLMod ↔ (π‘Š ∈ CMnd ∧ 𝐹 ∈ SRing ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
1211simp3bi 1144 . . . 4 (π‘Š ∈ SLMod β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))
13 oveq1 7412 . . . . . . . . . 10 (π‘ž = 𝑄 β†’ (π‘ž ⨣ π‘Ÿ) = (𝑄 ⨣ π‘Ÿ))
1413oveq1d 7420 . . . . . . . . 9 (π‘ž = 𝑄 β†’ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 ⨣ π‘Ÿ) Β· 𝑀))
15 oveq1 7412 . . . . . . . . . 10 (π‘ž = 𝑄 β†’ (π‘ž Β· 𝑀) = (𝑄 Β· 𝑀))
1615oveq1d 7420 . . . . . . . . 9 (π‘ž = 𝑄 β†’ ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀)) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
1714, 16eqeq12d 2742 . . . . . . . 8 (π‘ž = 𝑄 β†’ (((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀)) ↔ ((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
18173anbi3d 1438 . . . . . . 7 (π‘ž = 𝑄 β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ↔ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀)))))
19 oveq1 7412 . . . . . . . . . 10 (π‘ž = 𝑄 β†’ (π‘ž Γ— π‘Ÿ) = (𝑄 Γ— π‘Ÿ))
2019oveq1d 7420 . . . . . . . . 9 (π‘ž = 𝑄 β†’ ((π‘ž Γ— π‘Ÿ) Β· 𝑀) = ((𝑄 Γ— π‘Ÿ) Β· 𝑀))
21 oveq1 7412 . . . . . . . . 9 (π‘ž = 𝑄 β†’ (π‘ž Β· (π‘Ÿ Β· 𝑀)) = (𝑄 Β· (π‘Ÿ Β· 𝑀)))
2220, 21eqeq12d 2742 . . . . . . . 8 (π‘ž = 𝑄 β†’ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ↔ ((𝑄 Γ— π‘Ÿ) Β· 𝑀) = (𝑄 Β· (π‘Ÿ Β· 𝑀))))
23223anbi1d 1436 . . . . . . 7 (π‘ž = 𝑄 β†’ ((((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ) ↔ (((𝑄 Γ— π‘Ÿ) Β· 𝑀) = (𝑄 Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))
2418, 23anbi12d 630 . . . . . 6 (π‘ž = 𝑄 β†’ ((((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )) ↔ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((𝑄 Γ— π‘Ÿ) Β· 𝑀) = (𝑄 Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
25242ralbidv 3212 . . . . 5 (π‘ž = 𝑄 β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((𝑄 Γ— π‘Ÿ) Β· 𝑀) = (𝑄 Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
26 oveq1 7412 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ (π‘Ÿ Β· 𝑀) = (𝑅 Β· 𝑀))
2726eleq1d 2812 . . . . . . . 8 (π‘Ÿ = 𝑅 β†’ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ↔ (𝑅 Β· 𝑀) ∈ 𝑉))
28 oveq1 7412 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ (π‘Ÿ Β· (𝑀 + π‘₯)) = (𝑅 Β· (𝑀 + π‘₯)))
29 oveq1 7412 . . . . . . . . . 10 (π‘Ÿ = 𝑅 β†’ (π‘Ÿ Β· π‘₯) = (𝑅 Β· π‘₯))
3026, 29oveq12d 7423 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)))
3128, 30eqeq12d 2742 . . . . . . . 8 (π‘Ÿ = 𝑅 β†’ ((π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ↔ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯))))
32 oveq2 7413 . . . . . . . . . 10 (π‘Ÿ = 𝑅 β†’ (𝑄 ⨣ π‘Ÿ) = (𝑄 ⨣ 𝑅))
3332oveq1d 7420 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ ((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 ⨣ 𝑅) Β· 𝑀))
3426oveq2d 7421 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀)) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀)))
3533, 34eqeq12d 2742 . . . . . . . 8 (π‘Ÿ = 𝑅 β†’ (((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀)) ↔ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))))
3627, 31, 353anbi123d 1432 . . . . . . 7 (π‘Ÿ = 𝑅 β†’ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ↔ ((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀)))))
37 oveq2 7413 . . . . . . . . . 10 (π‘Ÿ = 𝑅 β†’ (𝑄 Γ— π‘Ÿ) = (𝑄 Γ— 𝑅))
3837oveq1d 7420 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ ((𝑄 Γ— π‘Ÿ) Β· 𝑀) = ((𝑄 Γ— 𝑅) Β· 𝑀))
3926oveq2d 7421 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ (𝑄 Β· (π‘Ÿ Β· 𝑀)) = (𝑄 Β· (𝑅 Β· 𝑀)))
4038, 39eqeq12d 2742 . . . . . . . 8 (π‘Ÿ = 𝑅 β†’ (((𝑄 Γ— π‘Ÿ) Β· 𝑀) = (𝑄 Β· (π‘Ÿ Β· 𝑀)) ↔ ((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀))))
41403anbi1d 1436 . . . . . . 7 (π‘Ÿ = 𝑅 β†’ ((((𝑄 Γ— π‘Ÿ) Β· 𝑀) = (𝑄 Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ) ↔ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))
4236, 41anbi12d 630 . . . . . 6 (π‘Ÿ = 𝑅 β†’ ((((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((𝑄 Γ— π‘Ÿ) Β· 𝑀) = (𝑄 Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )) ↔ (((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
43422ralbidv 3212 . . . . 5 (π‘Ÿ = 𝑅 β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((𝑄 ⨣ π‘Ÿ) Β· 𝑀) = ((𝑄 Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((𝑄 Γ— π‘Ÿ) Β· 𝑀) = (𝑄 Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
4425, 43rspc2v 3617 . . . 4 ((𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
4512, 44mpan9 506 . . 3 ((π‘Š ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))
46 oveq2 7413 . . . . . . . 8 (π‘₯ = 𝑋 β†’ (𝑀 + π‘₯) = (𝑀 + 𝑋))
4746oveq2d 7421 . . . . . . 7 (π‘₯ = 𝑋 β†’ (𝑅 Β· (𝑀 + π‘₯)) = (𝑅 Β· (𝑀 + 𝑋)))
48 oveq2 7413 . . . . . . . 8 (π‘₯ = 𝑋 β†’ (𝑅 Β· π‘₯) = (𝑅 Β· 𝑋))
4948oveq2d 7421 . . . . . . 7 (π‘₯ = 𝑋 β†’ ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· 𝑋)))
5047, 49eqeq12d 2742 . . . . . 6 (π‘₯ = 𝑋 β†’ ((𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ↔ (𝑅 Β· (𝑀 + 𝑋)) = ((𝑅 Β· 𝑀) + (𝑅 Β· 𝑋))))
51503anbi2d 1437 . . . . 5 (π‘₯ = 𝑋 β†’ (((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ↔ ((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + 𝑋)) = ((𝑅 Β· 𝑀) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀)))))
5251anbi1d 629 . . . 4 (π‘₯ = 𝑋 β†’ ((((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )) ↔ (((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + 𝑋)) = ((𝑅 Β· 𝑀) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
53 oveq2 7413 . . . . . . 7 (𝑀 = π‘Œ β†’ (𝑅 Β· 𝑀) = (𝑅 Β· π‘Œ))
5453eleq1d 2812 . . . . . 6 (𝑀 = π‘Œ β†’ ((𝑅 Β· 𝑀) ∈ 𝑉 ↔ (𝑅 Β· π‘Œ) ∈ 𝑉))
55 oveq1 7412 . . . . . . . 8 (𝑀 = π‘Œ β†’ (𝑀 + 𝑋) = (π‘Œ + 𝑋))
5655oveq2d 7421 . . . . . . 7 (𝑀 = π‘Œ β†’ (𝑅 Β· (𝑀 + 𝑋)) = (𝑅 Β· (π‘Œ + 𝑋)))
5753oveq1d 7420 . . . . . . 7 (𝑀 = π‘Œ β†’ ((𝑅 Β· 𝑀) + (𝑅 Β· 𝑋)) = ((𝑅 Β· π‘Œ) + (𝑅 Β· 𝑋)))
5856, 57eqeq12d 2742 . . . . . 6 (𝑀 = π‘Œ β†’ ((𝑅 Β· (𝑀 + 𝑋)) = ((𝑅 Β· 𝑀) + (𝑅 Β· 𝑋)) ↔ (𝑅 Β· (π‘Œ + 𝑋)) = ((𝑅 Β· π‘Œ) + (𝑅 Β· 𝑋))))
59 oveq2 7413 . . . . . . 7 (𝑀 = π‘Œ β†’ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 ⨣ 𝑅) Β· π‘Œ))
60 oveq2 7413 . . . . . . . 8 (𝑀 = π‘Œ β†’ (𝑄 Β· 𝑀) = (𝑄 Β· π‘Œ))
6160, 53oveq12d 7423 . . . . . . 7 (𝑀 = π‘Œ β†’ ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀)) = ((𝑄 Β· π‘Œ) + (𝑅 Β· π‘Œ)))
6259, 61eqeq12d 2742 . . . . . 6 (𝑀 = π‘Œ β†’ (((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀)) ↔ ((𝑄 ⨣ 𝑅) Β· π‘Œ) = ((𝑄 Β· π‘Œ) + (𝑅 Β· π‘Œ))))
6354, 58, 623anbi123d 1432 . . . . 5 (𝑀 = π‘Œ β†’ (((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + 𝑋)) = ((𝑅 Β· 𝑀) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ↔ ((𝑅 Β· π‘Œ) ∈ 𝑉 ∧ (𝑅 Β· (π‘Œ + 𝑋)) = ((𝑅 Β· π‘Œ) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· π‘Œ) = ((𝑄 Β· π‘Œ) + (𝑅 Β· π‘Œ)))))
64 oveq2 7413 . . . . . . 7 (𝑀 = π‘Œ β†’ ((𝑄 Γ— 𝑅) Β· 𝑀) = ((𝑄 Γ— 𝑅) Β· π‘Œ))
6553oveq2d 7421 . . . . . . 7 (𝑀 = π‘Œ β†’ (𝑄 Β· (𝑅 Β· 𝑀)) = (𝑄 Β· (𝑅 Β· π‘Œ)))
6664, 65eqeq12d 2742 . . . . . 6 (𝑀 = π‘Œ β†’ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ↔ ((𝑄 Γ— 𝑅) Β· π‘Œ) = (𝑄 Β· (𝑅 Β· π‘Œ))))
67 oveq2 7413 . . . . . . 7 (𝑀 = π‘Œ β†’ ( 1 Β· 𝑀) = ( 1 Β· π‘Œ))
68 id 22 . . . . . . 7 (𝑀 = π‘Œ β†’ 𝑀 = π‘Œ)
6967, 68eqeq12d 2742 . . . . . 6 (𝑀 = π‘Œ β†’ (( 1 Β· 𝑀) = 𝑀 ↔ ( 1 Β· π‘Œ) = π‘Œ))
70 oveq2 7413 . . . . . . 7 (𝑀 = π‘Œ β†’ (𝑂 Β· 𝑀) = (𝑂 Β· π‘Œ))
7170eqeq1d 2728 . . . . . 6 (𝑀 = π‘Œ β†’ ((𝑂 Β· 𝑀) = 0 ↔ (𝑂 Β· π‘Œ) = 0 ))
7266, 69, 713anbi123d 1432 . . . . 5 (𝑀 = π‘Œ β†’ ((((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ) ↔ (((𝑄 Γ— 𝑅) Β· π‘Œ) = (𝑄 Β· (𝑅 Β· π‘Œ)) ∧ ( 1 Β· π‘Œ) = π‘Œ ∧ (𝑂 Β· π‘Œ) = 0 )))
7363, 72anbi12d 630 . . . 4 (𝑀 = π‘Œ β†’ ((((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + 𝑋)) = ((𝑅 Β· 𝑀) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )) ↔ (((𝑅 Β· π‘Œ) ∈ 𝑉 ∧ (𝑅 Β· (π‘Œ + 𝑋)) = ((𝑅 Β· π‘Œ) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· π‘Œ) = ((𝑄 Β· π‘Œ) + (𝑅 Β· π‘Œ))) ∧ (((𝑄 Γ— 𝑅) Β· π‘Œ) = (𝑄 Β· (𝑅 Β· π‘Œ)) ∧ ( 1 Β· π‘Œ) = π‘Œ ∧ (𝑂 Β· π‘Œ) = 0 ))))
7452, 73rspc2v 3617 . . 3 ((𝑋 ∈ 𝑉 ∧ π‘Œ ∈ 𝑉) β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑅 Β· 𝑀) ∈ 𝑉 ∧ (𝑅 Β· (𝑀 + π‘₯)) = ((𝑅 Β· 𝑀) + (𝑅 Β· π‘₯)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑀) = ((𝑄 Β· 𝑀) + (𝑅 Β· 𝑀))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑀) = (𝑄 Β· (𝑅 Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )) β†’ (((𝑅 Β· π‘Œ) ∈ 𝑉 ∧ (𝑅 Β· (π‘Œ + 𝑋)) = ((𝑅 Β· π‘Œ) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· π‘Œ) = ((𝑄 Β· π‘Œ) + (𝑅 Β· π‘Œ))) ∧ (((𝑄 Γ— 𝑅) Β· π‘Œ) = (𝑄 Β· (𝑅 Β· π‘Œ)) ∧ ( 1 Β· π‘Œ) = π‘Œ ∧ (𝑂 Β· π‘Œ) = 0 ))))
7545, 74syl5com 31 . 2 ((π‘Š ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) β†’ ((𝑋 ∈ 𝑉 ∧ π‘Œ ∈ 𝑉) β†’ (((𝑅 Β· π‘Œ) ∈ 𝑉 ∧ (𝑅 Β· (π‘Œ + 𝑋)) = ((𝑅 Β· π‘Œ) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· π‘Œ) = ((𝑄 Β· π‘Œ) + (𝑅 Β· π‘Œ))) ∧ (((𝑄 Γ— 𝑅) Β· π‘Œ) = (𝑄 Β· (𝑅 Β· π‘Œ)) ∧ ( 1 Β· π‘Œ) = π‘Œ ∧ (𝑂 Β· π‘Œ) = 0 ))))
76753impia 1114 1 ((π‘Š ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ π‘Œ ∈ 𝑉)) β†’ (((𝑅 Β· π‘Œ) ∈ 𝑉 ∧ (𝑅 Β· (π‘Œ + 𝑋)) = ((𝑅 Β· π‘Œ) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· π‘Œ) = ((𝑄 Β· π‘Œ) + (𝑅 Β· π‘Œ))) ∧ (((𝑄 Γ— 𝑅) Β· π‘Œ) = (𝑄 Β· (𝑅 Β· π‘Œ)) ∧ ( 1 Β· π‘Œ) = π‘Œ ∧ (𝑂 Β· π‘Œ) = 0 )))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  β€˜cfv 6537  (class class class)co 7405  Basecbs 17153  +gcplusg 17206  .rcmulr 17207  Scalarcsca 17209   ·𝑠 cvsca 17210  0gc0g 17394  CMndccmn 19700  1rcur 20086  SRingcsrg 20091  SLModcslmd 32851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-nul 5299
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6489  df-fv 6545  df-ov 7408  df-slmd 32852
This theorem is referenced by:  slmdvscl  32865  slmdvsdi  32866  slmdvsdir  32867  slmdvsass  32868  slmdvs1  32871  slmd0vs  32875
  Copyright terms: Public domain W3C validator