Step |
Hyp |
Ref |
Expression |
1 |
|
lidlcl.u |
⊢ 𝑈 = ( LIdeal ‘ 𝑅 ) |
2 |
|
lidlcl.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
3 |
|
lidlmcl.t |
⊢ · = ( .r ‘ 𝑅 ) |
4 |
|
rlmvsca |
⊢ ( .r ‘ 𝑅 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) |
5 |
3 4
|
eqtri |
⊢ · = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) |
6 |
5
|
oveqi |
⊢ ( 𝑋 · 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 ) |
7 |
|
rlmlmod |
⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod ) |
8 |
7
|
ad2antrr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( ringLMod ‘ 𝑅 ) ∈ LMod ) |
9 |
|
simpr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ 𝑈 ) |
10 |
|
lidlval |
⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) |
11 |
1 10
|
eqtri |
⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) |
12 |
9 11
|
eleqtrdi |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ) |
13 |
12
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ) |
14 |
|
rlmsca |
⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) |
15 |
14
|
fveq2d |
⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ) |
16 |
2 15
|
syl5eq |
⊢ ( 𝑅 ∈ Ring → 𝐵 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ) |
17 |
16
|
eleq2d |
⊢ ( 𝑅 ∈ Ring → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ) ) |
18 |
17
|
biimpa |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ) |
19 |
18
|
ad2ant2r |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ) |
20 |
|
simprr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑌 ∈ 𝐼 ) |
21 |
|
eqid |
⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) |
22 |
|
eqid |
⊢ ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) |
23 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) |
24 |
|
eqid |
⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) |
25 |
21 22 23 24
|
lssvscl |
⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ) ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 ) |
26 |
8 13 19 20 25
|
syl22anc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 ) |
27 |
6 26
|
eqeltrid |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) |