This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issubrng

Description: The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025)

Ref Expression
Hypothesis issubrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion issubrng ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 issubrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 df-subrng ⊢ SubRng = ( 𝑤 ∈ Rng ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ Rng } )
3 2 mptrcl ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝑅 ∈ Rng )
4 simp1 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) → 𝑅 ∈ Rng )
5 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
6 5 pweqd ⊢ ( 𝑟 = 𝑅 → 𝒫 ( Base ‘ 𝑟 ) = 𝒫 ( Base ‘ 𝑅 ) )
7 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↾s 𝑠 ) = ( 𝑅 ↾s 𝑠 ) )
8 7 eleq1d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ↾s 𝑠 ) ∈ Rng ↔ ( 𝑅 ↾s 𝑠 ) ∈ Rng ) )
9 6 8 rabeqbidv ⊢ ( 𝑟 = 𝑅 → { 𝑠 ∈ 𝒫 ( Base ‘ 𝑟 ) ∣ ( 𝑟 ↾s 𝑠 ) ∈ Rng } = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } )
10 df-subrng ⊢ SubRng = ( 𝑟 ∈ Rng ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑟 ) ∣ ( 𝑟 ↾s 𝑠 ) ∈ Rng } )
11 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
12 11 pwex ⊢ 𝒫 ( Base ‘ 𝑅 ) ∈ V
13 12 rabex ⊢ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } ∈ V
14 9 10 13 fvmpt ⊢ ( 𝑅 ∈ Rng → ( SubRng ‘ 𝑅 ) = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } )
15 14 eleq2d ⊢ ( 𝑅 ∈ Rng → ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ 𝐴 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } ) )
16 oveq2 ⊢ ( 𝑠 = 𝐴 → ( 𝑅 ↾s 𝑠 ) = ( 𝑅 ↾s 𝐴 ) )
17 16 eleq1d ⊢ ( 𝑠 = 𝐴 → ( ( 𝑅 ↾s 𝑠 ) ∈ Rng ↔ ( 𝑅 ↾s 𝐴 ) ∈ Rng ) )
18 17 elrab ⊢ ( 𝐴 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } ↔ ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ) )
19 1 eqcomi ⊢ ( Base ‘ 𝑅 ) = 𝐵
20 19 sseq2i ⊢ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ↔ 𝐴 ⊆ 𝐵 )
21 20 anbi2i ⊢ ( ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ ( Base ‘ 𝑅 ) ) ↔ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) )
22 ibar ⊢ ( 𝑅 ∈ Rng → ( ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ↔ ( 𝑅 ∈ Rng ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) ) )
23 21 22 bitrid ⊢ ( 𝑅 ∈ Rng → ( ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ ( Base ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ Rng ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) ) )
24 11 elpw2 ⊢ ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ↔ 𝐴 ⊆ ( Base ‘ 𝑅 ) )
25 24 anbi2ci ⊢ ( ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ) ↔ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ ( Base ‘ 𝑅 ) ) )
26 3anass ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ↔ ( 𝑅 ∈ Rng ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) )
27 23 25 26 3bitr4g ⊢ ( 𝑅 ∈ Rng → ( ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) )
28 18 27 bitrid ⊢ ( 𝑅 ∈ Rng → ( 𝐴 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) )
29 15 28 bitrd ⊢ ( 𝑅 ∈ Rng → ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) )
30 3 4 29 pm5.21nii ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) )