Step |
Hyp |
Ref |
Expression |
1 |
|
lpival.p |
⊢ 𝑃 = ( LPIdeal ‘ 𝑅 ) |
2 |
|
lpiss.u |
⊢ 𝑈 = ( LIdeal ‘ 𝑅 ) |
3 |
|
eqid |
⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 ) |
4 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
5 |
1 3 4
|
islpidl |
⊢ ( 𝑅 ∈ Ring → ( 𝑎 ∈ 𝑃 ↔ ∃ 𝑔 ∈ ( Base ‘ 𝑅 ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ) ) |
6 |
|
snssi |
⊢ ( 𝑔 ∈ ( Base ‘ 𝑅 ) → { 𝑔 } ⊆ ( Base ‘ 𝑅 ) ) |
7 |
3 4 2
|
rspcl |
⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑔 } ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ∈ 𝑈 ) |
8 |
6 7
|
sylan2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑔 ∈ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ∈ 𝑈 ) |
9 |
|
eleq1 |
⊢ ( 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) → ( 𝑎 ∈ 𝑈 ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ∈ 𝑈 ) ) |
10 |
8 9
|
syl5ibrcom |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑔 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) → 𝑎 ∈ 𝑈 ) ) |
11 |
10
|
rexlimdva |
⊢ ( 𝑅 ∈ Ring → ( ∃ 𝑔 ∈ ( Base ‘ 𝑅 ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) → 𝑎 ∈ 𝑈 ) ) |
12 |
5 11
|
sylbid |
⊢ ( 𝑅 ∈ Ring → ( 𝑎 ∈ 𝑃 → 𝑎 ∈ 𝑈 ) ) |
13 |
12
|
ssrdv |
⊢ ( 𝑅 ∈ Ring → 𝑃 ⊆ 𝑈 ) |