Metamath Proof Explorer

Theorem rspprop

Description: Properties of a class to be the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 30-Jun-2026)

Ref Expression
Hypotheses rspvalint.v ⊢ 𝐵 = ( Base ‘ 𝑅 )
rspvalint.i ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
rspvalint.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
Assertion rspprop ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝐾 ‘ 𝑆 ) = 𝑋 ↔ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 rspvalint.v ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rspvalint.i ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
3 rspvalint.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4 3 1 2 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑆 ) ∈ 𝐼 )
5 3 1 rspssid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ⊆ ( 𝐾 ‘ 𝑆 ) )
6 3 2 rspssp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑖 ) → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 )
7 6 3expia ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ) → ( 𝑆 ⊆ 𝑖 → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 ) )
8 7 ralrimiva ⊢ ( 𝑅 ∈ Ring → ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 ) )
9 8 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 ) )
10 4 5 9 3jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝐾 ‘ 𝑆 ) ∈ 𝐼 ∧ 𝑆 ⊆ ( 𝐾 ‘ 𝑆 ) ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 ) ) )
11 eleq1 ⊢ ( ( 𝐾 ‘ 𝑆 ) = 𝑋 → ( ( 𝐾 ‘ 𝑆 ) ∈ 𝐼 ↔ 𝑋 ∈ 𝐼 ) )
12 sseq2 ⊢ ( ( 𝐾 ‘ 𝑆 ) = 𝑋 → ( 𝑆 ⊆ ( 𝐾 ‘ 𝑆 ) ↔ 𝑆 ⊆ 𝑋 ) )
13 sseq1 ⊢ ( ( 𝐾 ‘ 𝑆 ) = 𝑋 → ( ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 ↔ 𝑋 ⊆ 𝑖 ) )
14 13 imbi2d ⊢ ( ( 𝐾 ‘ 𝑆 ) = 𝑋 → ( ( 𝑆 ⊆ 𝑖 → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 ) ↔ ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) )
15 14 ralbidv ⊢ ( ( 𝐾 ‘ 𝑆 ) = 𝑋 → ( ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) )
16 11 12 15 3anbi123d ⊢ ( ( 𝐾 ‘ 𝑆 ) = 𝑋 → ( ( ( 𝐾 ‘ 𝑆 ) ∈ 𝐼 ∧ 𝑆 ⊆ ( 𝐾 ‘ 𝑆 ) ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑖 ) ) ↔ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) )
17 10 16 syl5ibcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝐾 ‘ 𝑆 ) = 𝑋 → ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) )
18 3 2 rspssp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑋 )
19 18 3adant3r3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑋 )
20 19 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) → ( 𝐾 ‘ 𝑆 ) ⊆ 𝑋 )
21 ssint ⊢ ( 𝑋 ⊆ ∩ { 𝑗 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑗 } ↔ ∀ 𝑖 ∈ { 𝑗 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑗 } 𝑋 ⊆ 𝑖 )
22 sseq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑆 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝑖 ) )
23 22 ralrab ⊢ ( ∀ 𝑖 ∈ { 𝑗 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑗 } 𝑋 ⊆ 𝑖 ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) )
24 21 23 sylbbr ⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) → 𝑋 ⊆ ∩ { 𝑗 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑗 } )
25 24 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) → 𝑋 ⊆ ∩ { 𝑗 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑗 } )
26 25 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) → 𝑋 ⊆ ∩ { 𝑗 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑗 } )
27 1 2 3 rspvalint ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑆 ) = ∩ { 𝑗 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑗 } )
28 27 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) → ( 𝐾 ‘ 𝑆 ) = ∩ { 𝑗 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑗 } )
29 26 28 sseqtrrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) → 𝑋 ⊆ ( 𝐾 ‘ 𝑆 ) )
30 20 29 eqssd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) → ( 𝐾 ‘ 𝑆 ) = 𝑋 )
31 30 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) → ( 𝐾 ‘ 𝑆 ) = 𝑋 ) )
32 17 31 impbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝐾 ‘ 𝑆 ) = 𝑋 ↔ ( 𝑋 ∈ 𝐼 ∧ 𝑆 ⊆ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑆 ⊆ 𝑖 → 𝑋 ⊆ 𝑖 ) ) ) )