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 B=BaseR
issubrg.i 1˙=1R
Assertion issubrg ASubRingRRRingR𝑠ARingAB1˙A

Proof

Step Hyp Ref Expression
1 issubrg.b B=BaseR
2 issubrg.i 1˙=1R
3 df-subrg SubRing=rRings𝒫Baser|r𝑠sRing1rs
4 3 mptrcl ASubRingRRRing
5 simpll RRingR𝑠ARingAB1˙ARRing
6 fveq2 r=RBaser=BaseR
7 6 1 eqtr4di r=RBaser=B
8 7 pweqd r=R𝒫Baser=𝒫B
9 oveq1 r=Rr𝑠s=R𝑠s
10 9 eleq1d r=Rr𝑠sRingR𝑠sRing
11 fveq2 r=R1r=1R
12 11 2 eqtr4di r=R1r=1˙
13 12 eleq1d r=R1rs1˙s
14 10 13 anbi12d r=Rr𝑠sRing1rsR𝑠sRing1˙s
15 8 14 rabeqbidv r=Rs𝒫Baser|r𝑠sRing1rs=s𝒫B|R𝑠sRing1˙s
16 1 fvexi BV
17 16 pwex 𝒫BV
18 17 rabex s𝒫B|R𝑠sRing1˙sV
19 15 3 18 fvmpt RRingSubRingR=s𝒫B|R𝑠sRing1˙s
20 19 eleq2d RRingASubRingRAs𝒫B|R𝑠sRing1˙s
21 oveq2 s=AR𝑠s=R𝑠A
22 21 eleq1d s=AR𝑠sRingR𝑠ARing
23 eleq2 s=A1˙s1˙A
24 22 23 anbi12d s=AR𝑠sRing1˙sR𝑠ARing1˙A
25 24 elrab As𝒫B|R𝑠sRing1˙sA𝒫BR𝑠ARing1˙A
26 16 elpw2 A𝒫BAB
27 26 anbi1i A𝒫BR𝑠ARing1˙AABR𝑠ARing1˙A
28 an12 ABR𝑠ARing1˙AR𝑠ARingAB1˙A
29 25 27 28 3bitri As𝒫B|R𝑠sRing1˙sR𝑠ARingAB1˙A
30 ibar RRingR𝑠ARingRRingR𝑠ARing
31 30 anbi1d RRingR𝑠ARingAB1˙ARRingR𝑠ARingAB1˙A
32 29 31 syl5bb RRingAs𝒫B|R𝑠sRing1˙sRRingR𝑠ARingAB1˙A
33 20 32 bitrd RRingASubRingRRRingR𝑠ARingAB1˙A
34 4 5 33 pm5.21nii ASubRingRRRingR𝑠ARingAB1˙A