Metamath Proof Explorer

Theorem issubrg

Description: The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014) (Proof shortened by AV, 12-Oct-2020)

Ref Expression
Hypotheses issubrg.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
issubrg.i ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion issubrg ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 issubrg.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 issubrg.i ⊢ 1 = ( 1r ‘ 𝑅 )
3 df-subrg ⊢ SubRing = ( 𝑟 ∈ Ring ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑟 ) ∣ ( ( 𝑟 ↾s 𝑠 ) ∈ Ring ∧ ( 1r ‘ 𝑟 ) ∈ 𝑠 ) } )
4 3 mptrcl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
5 simpll ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) → 𝑅 ∈ Ring )
6 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
7 6 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
8 7 pweqd ⊢ ( 𝑟 = 𝑅 → 𝒫 ( Base ‘ 𝑟 ) = 𝒫 𝐵 )
9 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↾s 𝑠 ) = ( 𝑅 ↾s 𝑠 ) )
10 9 eleq1d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ↾s 𝑠 ) ∈ Ring ↔ ( 𝑅 ↾s 𝑠 ) ∈ Ring ) )
11 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) )
12 11 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = 1 )
13 12 eleq1d ⊢ ( 𝑟 = 𝑅 → ( ( 1r ‘ 𝑟 ) ∈ 𝑠 ↔ 1 ∈ 𝑠 ) )
14 10 13 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑟 ↾s 𝑠 ) ∈ Ring ∧ ( 1r ‘ 𝑟 ) ∈ 𝑠 ) ↔ ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) ) )
15 8 14 rabeqbidv ⊢ ( 𝑟 = 𝑅 → { 𝑠 ∈ 𝒫 ( Base ‘ 𝑟 ) ∣ ( ( 𝑟 ↾s 𝑠 ) ∈ Ring ∧ ( 1r ‘ 𝑟 ) ∈ 𝑠 ) } = { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) } )
16 1 fvexi ⊢ 𝐵 ∈ V
17 16 pwex ⊢ 𝒫 𝐵 ∈ V
18 17 rabex ⊢ { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) } ∈ V
19 15 3 18 fvmpt ⊢ ( 𝑅 ∈ Ring → ( SubRing ‘ 𝑅 ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) } )
20 19 eleq2d ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ 𝐴 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) } ) )
21 oveq2 ⊢ ( 𝑠 = 𝐴 → ( 𝑅 ↾s 𝑠 ) = ( 𝑅 ↾s 𝐴 ) )
22 21 eleq1d ⊢ ( 𝑠 = 𝐴 → ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ↔ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) )
23 eleq2 ⊢ ( 𝑠 = 𝐴 → ( 1 ∈ 𝑠 ↔ 1 ∈ 𝐴 ) )
24 22 23 anbi12d ⊢ ( 𝑠 = 𝐴 → ( ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) ↔ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ 1 ∈ 𝐴 ) ) )
25 24 elrab ⊢ ( 𝐴 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) } ↔ ( 𝐴 ∈ 𝒫 𝐵 ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ 1 ∈ 𝐴 ) ) )
26 16 elpw2 ⊢ ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 )
27 26 anbi1i ⊢ ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ 1 ∈ 𝐴 ) ) ↔ ( 𝐴 ⊆ 𝐵 ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ 1 ∈ 𝐴 ) ) )
28 an12 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ 1 ∈ 𝐴 ) ) ↔ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) )
29 25 27 28 3bitri ⊢ ( 𝐴 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) } ↔ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) )
30 ibar ⊢ ( 𝑅 ∈ Ring → ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ↔ ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ) )
31 30 anbi1d ⊢ ( 𝑅 ∈ Ring → ( ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) ) )
32 29 31 bitrid ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 𝑅 ↾s 𝑠 ) ∈ Ring ∧ 1 ∈ 𝑠 ) } ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) ) )
33 20 32 bitrd ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) ) )
34 4 5 33 pm5.21nii ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) )