Step * 1 1 1 1 1 of Lemma quot_by_prime_ideal

.....assertion..... 
1. CRng
2. Ideal(r){i}
3. detach_fun(|r|;p)
4. ∀u:|r|. SqStable(p u)
⊢ (p 1)) ∧ (∀u,v:|r|.  ((¬(p v))  (p (u v))  (p u)))
⇐⇒ (p 1)) ∧ (∀u,v:|r|.  ((p (u v))  ((p u) ∨ (p v))))
BY
Auto }

1
1. CRng
2. Ideal(r){i}
3. detach_fun(|r|;p)
4. ∀u:|r|. SqStable(p u)
5. ¬(p 1)
6. ∀u,v:|r|.  ((¬(p v))  (p (u v))  (p u))
7. |r|
8. |r|
9. (u v)
⊢ (p u) ∨ (p v)

2
1. CRng
2. Ideal(r){i}
3. detach_fun(|r|;p)
4. ∀u:|r|. SqStable(p u)
5. ¬(p 1)
6. ∀u,v:|r|.  ((p (u v))  ((p u) ∨ (p v)))
7. |r|
8. |r|
9. ¬(p v)
10. (u v)
⊢ u


Latex:


Latex:
.....assertion..... 
1.  r  :  CRng
2.  p  :  Ideal(r)\{i\}
3.  d  :  detach\_fun(|r|;p)
4.  \mforall{}u:|r|.  SqStable(p  u)
\mvdash{}  (\mneg{}(p  1))  \mwedge{}  (\mforall{}u,v:|r|.    ((\mneg{}(p  v))  {}\mRightarrow{}  (p  (u  *  v))  {}\mRightarrow{}  (p  u)))
\mLeftarrow{}{}\mRightarrow{}  (\mneg{}(p  1))  \mwedge{}  (\mforall{}u,v:|r|.    ((p  (u  *  v))  {}\mRightarrow{}  ((p  u)  \mvee{}  (p  v))))


By


Latex:
Auto




Home Index