---

Step * 1 2 of Lemma princ_ideal_wf

.....set predicate..... 
1. r : Rng
2. a : |r|
⊢ (a)r Ideal of r
BY
{ TACTIC:(RepUR ``ideal princ_ideal ideal_p subgrp_p`` 0 THEN Auto THEN ExRepD) }

1
1. r : Rng
2. a : |r|
⊢ ∃b:|r|. (0 = (a * b) ∈ |r|)

2
1. r : Rng
2. a : |r|
3. b1 : |r|
4. 0 = (a * b1) ∈ |r|
5. a@0 : |r|@i
6. b : |r|@i
7. a@0 = (a * b) ∈ |r|
⊢ ∃b:|r|. ((-r a@0) = (a * b) ∈ |r|)

3
1. r : Rng
2. a : |r|
3. b2 : |r|
4. 0 = (a * b2) ∈ |r|
5. ∀a@0:|r|. ((∃b:|r|. (a@0 = (a * b) ∈ |r|)) ⇒ (∃b:|r|. ((-r a@0) = (a * b) ∈ |r|)))
6. a@0 : |r|@i
7. b : |r|@i
8. b1 : |r|@i
9. a@0 = (a * b1) ∈ |r|
10. b@0 : |r|@i
11. b = (a * b@0) ∈ |r|
⊢ ∃b@0:|r|. ((a@0 +r b) = (a * b@0) ∈ |r|)

4
1. r : Rng
2. a : |r|
3. b2 : |r|
4. 0 = (a * b2) ∈ |r|
5. ∀a@0:|r|. ((∃b:|r|. (a@0 = (a * b) ∈ |r|)) ⇒ (∃b:|r|. ((-r a@0) = (a * b) ∈ |r|)))
6. ∀a@0,b:|r|.
     ((∃b:|r|. (a@0 = (a * b) ∈ |r|))
     ⇒ (∃b@0:|r|. (b = (a * b@0) ∈ |r|))
     ⇒ (∃b@0:|r|. ((a@0 +r b) = (a * b@0) ∈ |r|)))
7. a@0 : |r|@i
8. b : |r|@i
9. b1 : |r|@i
10. a@0 = (a * b1) ∈ |r|
⊢ ∃b@0:|r|. ((a@0 * b) = (a * b@0) ∈ |r|)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  r  :  Rng
2.  a  :  |r|
\mvdash{}  (a)r  Ideal  of  r


By

---

Latex:
TACTIC:(RepUR  ``ideal  princ\_ideal  ideal\_p  subgrp\_p``  0  THEN  Auto  THEN  ExRepD)

---

Home Index