Metamath Proof Explorer


Theorem issubrg2

Description: Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Hypotheses issubrg2.b B = Base R
issubrg2.o 1 ˙ = 1 R
issubrg2.t · ˙ = R
Assertion issubrg2 R Ring A SubRing R A SubGrp R 1 ˙ A x A y A x · ˙ y A

Proof

Step Hyp Ref Expression
1 issubrg2.b B = Base R
2 issubrg2.o 1 ˙ = 1 R
3 issubrg2.t · ˙ = R
4 subrgsubg A SubRing R A SubGrp R
5 2 subrg1cl A SubRing R 1 ˙ A
6 3 subrgmcl A SubRing R x A y A x · ˙ y A
7 6 3expb A SubRing R x A y A x · ˙ y A
8 7 ralrimivva A SubRing R x A y A x · ˙ y A
9 4 5 8 3jca A SubRing R A SubGrp R 1 ˙ A x A y A x · ˙ y A
10 simpl R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A R Ring
11 simpr1 R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A A SubGrp R
12 eqid R 𝑠 A = R 𝑠 A
13 12 subgbas A SubGrp R A = Base R 𝑠 A
14 11 13 syl R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A A = Base R 𝑠 A
15 eqid + R = + R
16 12 15 ressplusg A SubGrp R + R = + R 𝑠 A
17 11 16 syl R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A + R = + R 𝑠 A
18 12 3 ressmulr A SubGrp R · ˙ = R 𝑠 A
19 11 18 syl R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A · ˙ = R 𝑠 A
20 12 subggrp A SubGrp R R 𝑠 A Grp
21 11 20 syl R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A R 𝑠 A Grp
22 simpr3 R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A x A y A x · ˙ y A
23 oveq1 x = u x · ˙ y = u · ˙ y
24 23 eleq1d x = u x · ˙ y A u · ˙ y A
25 oveq2 y = v u · ˙ y = u · ˙ v
26 25 eleq1d y = v u · ˙ y A u · ˙ v A
27 24 26 rspc2v u A v A x A y A x · ˙ y A u · ˙ v A
28 22 27 syl5com R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A v A u · ˙ v A
29 28 3impib R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A v A u · ˙ v A
30 1 subgss A SubGrp R A B
31 11 30 syl R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A A B
32 31 sseld R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A u B
33 31 sseld R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A v A v B
34 31 sseld R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A w A w B
35 32 33 34 3anim123d R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A v A w A u B v B w B
36 35 imp R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A v A w A u B v B w B
37 1 3 ringass R Ring u B v B w B u · ˙ v · ˙ w = u · ˙ v · ˙ w
38 37 adantlr R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u B v B w B u · ˙ v · ˙ w = u · ˙ v · ˙ w
39 36 38 syldan R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A v A w A u · ˙ v · ˙ w = u · ˙ v · ˙ w
40 1 15 3 ringdi R Ring u B v B w B u · ˙ v + R w = u · ˙ v + R u · ˙ w
41 40 adantlr R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u B v B w B u · ˙ v + R w = u · ˙ v + R u · ˙ w
42 36 41 syldan R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A v A w A u · ˙ v + R w = u · ˙ v + R u · ˙ w
43 1 15 3 ringdir R Ring u B v B w B u + R v · ˙ w = u · ˙ w + R v · ˙ w
44 43 adantlr R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u B v B w B u + R v · ˙ w = u · ˙ w + R v · ˙ w
45 36 44 syldan R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A v A w A u + R v · ˙ w = u · ˙ w + R v · ˙ w
46 simpr2 R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A 1 ˙ A
47 32 imp R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A u B
48 1 3 2 ringlidm R Ring u B 1 ˙ · ˙ u = u
49 48 adantlr R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u B 1 ˙ · ˙ u = u
50 47 49 syldan R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A 1 ˙ · ˙ u = u
51 1 3 2 ringridm R Ring u B u · ˙ 1 ˙ = u
52 51 adantlr R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u B u · ˙ 1 ˙ = u
53 47 52 syldan R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A u A u · ˙ 1 ˙ = u
54 14 17 19 21 29 39 42 45 46 50 53 isringd R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A R 𝑠 A Ring
55 31 46 jca R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A A B 1 ˙ A
56 1 2 issubrg A SubRing R R Ring R 𝑠 A Ring A B 1 ˙ A
57 10 54 55 56 syl21anbrc R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A A SubRing R
58 57 ex R Ring A SubGrp R 1 ˙ A x A y A x · ˙ y A A SubRing R
59 9 58 impbid2 R Ring A SubRing R A SubGrp R 1 ˙ A x A y A x · ˙ y A