Metamath Proof Explorer


Theorem cnsubrglem

Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses cnsubglem.1 xAx
cnsubglem.2 xAyAx+yA
cnsubglem.3 xAxA
cnsubrglem.4 1A
cnsubrglem.5 xAyAxyA
Assertion cnsubrglem ASubRingfld

Proof

Step Hyp Ref Expression
1 cnsubglem.1 xAx
2 cnsubglem.2 xAyAx+yA
3 cnsubglem.3 xAxA
4 cnsubrglem.4 1A
5 cnsubrglem.5 xAyAxyA
6 1 2 3 4 cnsubglem ASubGrpfld
7 5 rgen2 xAyAxyA
8 cnring fldRing
9 cnfldbas =Basefld
10 cnfld1 1=1fld
11 cnfldmul ×=fld
12 9 10 11 issubrg2 fldRingASubRingfldASubGrpfld1AxAyAxyA
13 8 12 ax-mp ASubRingfldASubGrpfld1AxAyAxyA
14 6 4 7 13 mpbir3an ASubRingfld