Step
*
of Lemma
ideal_of_prime
∀r:CRng. ∀u:|r|.  (r-Prime(u) 
⇐⇒ IsPrimeIdeal(r;(u)r))
BY
{ UnivCD 
THENM Unfold `prime_ideal_p` 0 
THENA Auto }
1
1. r : CRng@i'
2. u : |r|@i
⊢ r-Prime(u) 
⇐⇒ (¬((u)r 1)) ∧ (∀a,b:|r|.  (((u)r (a * b)) 
⇒ (((u)r a) ∨ ((u)r b))))
Latex:
Latex:
\mforall{}r:CRng.  \mforall{}u:|r|.    (r-Prime(u)  \mLeftarrow{}{}\mRightarrow{}  IsPrimeIdeal(r;(u)r))
By
Latex:
UnivCD 
THENM  Unfold  `prime\_ideal\_p`  0 
THENA  Auto
Home
Index