Metamath Proof Explorer


Theorem lidldvgen

Description: An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lidldvgen.b B = Base R
lidldvgen.u U = LIdeal R
lidldvgen.k K = RSpan R
lidldvgen.d ˙ = r R
Assertion lidldvgen R Ring I U G B I = K G G I x I G ˙ x

Proof

Step Hyp Ref Expression
1 lidldvgen.b B = Base R
2 lidldvgen.u U = LIdeal R
3 lidldvgen.k K = RSpan R
4 lidldvgen.d ˙ = r R
5 simp1 R Ring I U G B R Ring
6 simp3 R Ring I U G B G B
7 6 snssd R Ring I U G B G B
8 3 1 rspssid R Ring G B G K G
9 5 7 8 syl2anc R Ring I U G B G K G
10 snssg G B G K G G K G
11 10 3ad2ant3 R Ring I U G B G K G G K G
12 9 11 mpbird R Ring I U G B G K G
13 1 3 4 rspsn R Ring G B K G = y | G ˙ y
14 13 3adant2 R Ring I U G B K G = y | G ˙ y
15 14 eleq2d R Ring I U G B x K G x y | G ˙ y
16 vex x V
17 breq2 y = x G ˙ y G ˙ x
18 16 17 elab x y | G ˙ y G ˙ x
19 15 18 bitrdi R Ring I U G B x K G G ˙ x
20 19 biimpd R Ring I U G B x K G G ˙ x
21 20 ralrimiv R Ring I U G B x K G G ˙ x
22 12 21 jca R Ring I U G B G K G x K G G ˙ x
23 eleq2 I = K G G I G K G
24 raleq I = K G x I G ˙ x x K G G ˙ x
25 23 24 anbi12d I = K G G I x I G ˙ x G K G x K G G ˙ x
26 22 25 syl5ibrcom R Ring I U G B I = K G G I x I G ˙ x
27 df-ral x I G ˙ x x x I G ˙ x
28 ssab I x | G ˙ x x x I G ˙ x
29 27 28 sylbb2 x I G ˙ x I x | G ˙ x
30 29 ad2antll R Ring I U G B G I x I G ˙ x I x | G ˙ x
31 1 3 4 rspsn R Ring G B K G = x | G ˙ x
32 31 3adant2 R Ring I U G B K G = x | G ˙ x
33 32 adantr R Ring I U G B G I x I G ˙ x K G = x | G ˙ x
34 30 33 sseqtrrd R Ring I U G B G I x I G ˙ x I K G
35 simpl1 R Ring I U G B G I R Ring
36 simpl2 R Ring I U G B G I I U
37 snssi G I G I
38 37 adantl R Ring I U G B G I G I
39 3 2 rspssp R Ring I U G I K G I
40 35 36 38 39 syl3anc R Ring I U G B G I K G I
41 40 adantrr R Ring I U G B G I x I G ˙ x K G I
42 34 41 eqssd R Ring I U G B G I x I G ˙ x I = K G
43 42 ex R Ring I U G B G I x I G ˙ x I = K G
44 26 43 impbid R Ring I U G B I = K G G I x I G ˙ x