Step * of Lemma ideal_of_prime

r:CRng. ∀u:|r|.  (r-Prime(u) ⇐⇒ IsPrimeIdeal(r;(u)r))
BY
UnivCD 
THENM Unfold `prime_ideal_p` 
THENA Auto }

1
1. CRng@i'
2. |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