Metamath Proof Explorer


Theorem mxidlprm

Description: Every maximal ideal is prime. Statement in Lang p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Hypothesis mxidlprm.1 × ˙ = LSSum mulGrp R
Assertion mxidlprm Could not format assertion : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( PrmIdeal ` R ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 mxidlprm.1 × ˙ = LSSum mulGrp R
2 crngring R CRing R Ring
3 2 adantr Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> R e. Ring ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> R e. Ring ) with typecode |-
4 eqid Base R = Base R
5 4 mxidlidl Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) with typecode |-
6 2 5 sylan Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) with typecode |-
7 4 mxidlnr Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) ) with typecode |-
8 2 7 sylan Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) ) with typecode |-
9 simpllr Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( 1r ` R ) = ( u ( +g ` R ) k ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( 1r ` R ) = ( u ( +g ` R ) k ) ) with typecode |-
10 simpr Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> k = ( a ( .r ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> k = ( a ( .r ` R ) x ) ) with typecode |-
11 10 oveq2d Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( u ( +g ` R ) k ) = ( u ( +g ` R ) ( a ( .r ` R ) x ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( u ( +g ` R ) k ) = ( u ( +g ` R ) ( a ( .r ` R ) x ) ) ) with typecode |-
12 9 11 eqtrd Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( 1r ` R ) = ( u ( +g ` R ) ( a ( .r ` R ) x ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( 1r ` R ) = ( u ( +g ` R ) ( a ( .r ` R ) x ) ) ) with typecode |-
13 12 oveq1d Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( 1r ` R ) ( .r ` R ) y ) = ( ( u ( +g ` R ) ( a ( .r ` R ) x ) ) ( .r ` R ) y ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( 1r ` R ) ( .r ` R ) y ) = ( ( u ( +g ` R ) ( a ( .r ` R ) x ) ) ( .r ` R ) y ) ) with typecode |-
14 3 ad4antr Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> R e. Ring ) with typecode |-
15 14 ad5antr Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> R e. Ring ) with typecode |-
16 simp-8r Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> y e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> y e. ( Base ` R ) ) with typecode |-
17 eqid R = R
18 eqid 1 R = 1 R
19 4 17 18 ringlidm R Ring y Base R 1 R R y = y
20 15 16 19 syl2anc Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( 1r ` R ) ( .r ` R ) y ) = y ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( 1r ` R ) ( .r ` R ) y ) = y ) with typecode |-
21 eqid LIdeal R = LIdeal R
22 4 21 lidlss M LIdeal R M Base R
23 6 22 syl Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M C_ ( Base ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M C_ ( Base ` R ) ) with typecode |-
24 23 ad4antr Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( Base ` R ) ) with typecode |-
25 24 ad5antr Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> M C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> M C_ ( Base ` R ) ) with typecode |-
26 simp-5r Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> u e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> u e. M ) with typecode |-
27 25 26 sseldd Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> u e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> u e. ( Base ` R ) ) with typecode |-
28 simplr Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> a e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> a e. ( Base ` R ) ) with typecode |-
29 simp-4r Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x e. ( Base ` R ) ) with typecode |-
30 29 ad5antr Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> x e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> x e. ( Base ` R ) ) with typecode |-
31 4 17 ringcl R Ring a Base R x Base R a R x Base R
32 15 28 30 31 syl3anc Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( a ( .r ` R ) x ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( a ( .r ` R ) x ) e. ( Base ` R ) ) with typecode |-
33 eqid + R = + R
34 4 33 17 ringdir R Ring u Base R a R x Base R y Base R u + R a R x R y = u R y + R a R x R y
35 15 27 32 16 34 syl13anc Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( u ( +g ` R ) ( a ( .r ` R ) x ) ) ( .r ` R ) y ) = ( ( u ( .r ` R ) y ) ( +g ` R ) ( ( a ( .r ` R ) x ) ( .r ` R ) y ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( u ( +g ` R ) ( a ( .r ` R ) x ) ) ( .r ` R ) y ) = ( ( u ( .r ` R ) y ) ( +g ` R ) ( ( a ( .r ` R ) x ) ( .r ` R ) y ) ) ) with typecode |-
36 13 20 35 3eqtr3d Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> y = ( ( u ( .r ` R ) y ) ( +g ` R ) ( ( a ( .r ` R ) x ) ( .r ` R ) y ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> y = ( ( u ( .r ` R ) y ) ( +g ` R ) ( ( a ( .r ` R ) x ) ( .r ` R ) y ) ) ) with typecode |-
37 simp-5r Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
38 14 37 5 syl2anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M e. ( LIdeal ` R ) ) with typecode |-
39 38 ad5antr Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> M e. ( LIdeal ` R ) ) with typecode |-
40 simp-10l Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> R e. CRing ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> R e. CRing ) with typecode |-
41 4 17 crngcom R CRing y Base R u Base R y R u = u R y
42 40 16 27 41 syl3anc Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( y ( .r ` R ) u ) = ( u ( .r ` R ) y ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( y ( .r ` R ) u ) = ( u ( .r ` R ) y ) ) with typecode |-
43 21 4 17 lidlmcl R Ring M LIdeal R y Base R u M y R u M
44 15 39 16 26 43 syl22anc Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( y ( .r ` R ) u ) e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( y ( .r ` R ) u ) e. M ) with typecode |-
45 42 44 eqeltrrd Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( u ( .r ` R ) y ) e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( u ( .r ` R ) y ) e. M ) with typecode |-
46 4 17 ringass R Ring a Base R x Base R y Base R a R x R y = a R x R y
47 15 28 30 16 46 syl13anc Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( a ( .r ` R ) x ) ( .r ` R ) y ) = ( a ( .r ` R ) ( x ( .r ` R ) y ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( a ( .r ` R ) x ) ( .r ` R ) y ) = ( a ( .r ` R ) ( x ( .r ` R ) y ) ) ) with typecode |-
48 simp-7r Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( x ( .r ` R ) y ) e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( x ( .r ` R ) y ) e. M ) with typecode |-
49 21 4 17 lidlmcl R Ring M LIdeal R a Base R x R y M a R x R y M
50 15 39 28 48 49 syl22anc Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( a ( .r ` R ) ( x ( .r ` R ) y ) ) e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( a ( .r ` R ) ( x ( .r ` R ) y ) ) e. M ) with typecode |-
51 47 50 eqeltrd Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( a ( .r ` R ) x ) ( .r ` R ) y ) e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( a ( .r ` R ) x ) ( .r ` R ) y ) e. M ) with typecode |-
52 21 33 lidlacl R Ring M LIdeal R u R y M a R x R y M u R y + R a R x R y M
53 15 39 45 51 52 syl22anc Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( u ( .r ` R ) y ) ( +g ` R ) ( ( a ( .r ` R ) x ) ( .r ` R ) y ) ) e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> ( ( u ( .r ` R ) y ) ( +g ` R ) ( ( a ( .r ` R ) x ) ( .r ` R ) y ) ) e. M ) with typecode |-
54 36 53 eqeltrd Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> y e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) /\ a e. ( Base ` R ) ) /\ k = ( a ( .r ` R ) x ) ) -> y e. M ) with typecode |-
55 simplr Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) -> k e. ( ( Base ` R ) .X. { x } ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) -> k e. ( ( Base ` R ) .X. { x } ) ) with typecode |-
56 eqid mulGrp R = mulGrp R
57 56 4 mgpbas Base R = Base mulGrp R
58 56 17 mgpplusg R = + mulGrp R
59 fvexd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( mulGrp ` R ) e. _V ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( mulGrp ` R ) e. _V ) with typecode |-
60 ssidd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( Base ` R ) C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( Base ` R ) C_ ( Base ` R ) ) with typecode |-
61 57 58 1 59 60 29 elgrplsmsn Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( k e. ( ( Base ` R ) .X. { x } ) <-> E. a e. ( Base ` R ) k = ( a ( .r ` R ) x ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( k e. ( ( Base ` R ) .X. { x } ) <-> E. a e. ( Base ` R ) k = ( a ( .r ` R ) x ) ) ) with typecode |-
62 61 ad3antrrr Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) -> ( k e. ( ( Base ` R ) .X. { x } ) <-> E. a e. ( Base ` R ) k = ( a ( .r ` R ) x ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) -> ( k e. ( ( Base ` R ) .X. { x } ) <-> E. a e. ( Base ` R ) k = ( a ( .r ` R ) x ) ) ) with typecode |-
63 55 62 mpbid Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) -> E. a e. ( Base ` R ) k = ( a ( .r ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) -> E. a e. ( Base ` R ) k = ( a ( .r ` R ) x ) ) with typecode |-
64 54 63 r19.29a Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) -> y e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ u e. M ) /\ k e. ( ( Base ` R ) .X. { x } ) ) /\ ( 1r ` R ) = ( u ( +g ` R ) k ) ) -> y e. M ) with typecode |-
65 4 18 ringidcl R Ring 1 R Base R
66 14 65 syl Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( 1r ` R ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( 1r ` R ) e. ( Base ` R ) ) with typecode |-
67 eqid LSSum R = LSSum R
68 eqid RSpan R = RSpan R
69 eqid LPIdeal R = LPIdeal R
70 69 21 lpiss R Ring LPIdeal R LIdeal R
71 14 70 syl Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( LPIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( LPIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
72 4 56 1 68 14 29 lsmsnidl Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( Base ` R ) .X. { x } ) e. ( LPIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( Base ` R ) .X. { x } ) e. ( LPIdeal ` R ) ) with typecode |-
73 71 72 sseldd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( Base ` R ) .X. { x } ) e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( Base ` R ) .X. { x } ) e. ( LIdeal ` R ) ) with typecode |-
74 4 67 68 14 38 73 lsmidl Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) e. ( LIdeal ` R ) ) with typecode |-
75 rlmlmod R Ring ringLMod R LMod
76 14 75 syl Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ringLMod ` R ) e. LMod ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ringLMod ` R ) e. LMod ) with typecode |-
77 rlmbas Base R = Base ringLMod R
78 rspval RSpan R = LSpan ringLMod R
79 77 78 lspssid ringLMod R LMod M Base R M RSpan R M
80 76 24 79 syl2anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( ( RSpan ` R ) ` M ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( ( RSpan ` R ) ` M ) ) with typecode |-
81 29 snssd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> { x } C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> { x } C_ ( Base ` R ) ) with typecode |-
82 4 56 1 14 60 81 ringlsmss Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( Base ` R ) .X. { x } ) C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( Base ` R ) .X. { x } ) C_ ( Base ` R ) ) with typecode |-
83 24 82 unssd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M u. ( ( Base ` R ) .X. { x } ) ) C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M u. ( ( Base ` R ) .X. { x } ) ) C_ ( Base ` R ) ) with typecode |-
84 ssun1 M M Base R × ˙ x
85 84 a1i Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( M u. ( ( Base ` R ) .X. { x } ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( M u. ( ( Base ` R ) .X. { x } ) ) ) with typecode |-
86 77 78 lspss ringLMod R LMod M Base R × ˙ x Base R M M Base R × ˙ x RSpan R M RSpan R M Base R × ˙ x
87 76 83 85 86 syl3anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( RSpan ` R ) ` M ) C_ ( ( RSpan ` R ) ` ( M u. ( ( Base ` R ) .X. { x } ) ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( RSpan ` R ) ` M ) C_ ( ( RSpan ` R ) ` ( M u. ( ( Base ` R ) .X. { x } ) ) ) ) with typecode |-
88 80 87 sstrd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( ( RSpan ` R ) ` ( M u. ( ( Base ` R ) .X. { x } ) ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( ( RSpan ` R ) ` ( M u. ( ( Base ` R ) .X. { x } ) ) ) ) with typecode |-
89 4 67 68 14 38 73 lsmidllsp Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = ( ( RSpan ` R ) ` ( M u. ( ( Base ` R ) .X. { x } ) ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = ( ( RSpan ` R ) ` ( M u. ( ( Base ` R ) .X. { x } ) ) ) ) with typecode |-
90 88 89 sseqtrrd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> M C_ ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) ) with typecode |-
91 4 mxidlmax Could not format ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) e. ( LIdeal ` R ) /\ M C_ ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) ) ) -> ( ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = M \/ ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = ( Base ` R ) ) ) : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) e. ( LIdeal ` R ) /\ M C_ ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) ) ) -> ( ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = M \/ ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = ( Base ` R ) ) ) with typecode |-
92 14 37 74 90 91 syl22anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = M \/ ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = ( Base ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = M \/ ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = ( Base ` R ) ) ) with typecode |-
93 eqid 0 R = 0 R
94 21 93 lidl0cl R Ring M LIdeal R 0 R M
95 14 38 94 syl2anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( 0g ` R ) e. M ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( 0g ` R ) e. M ) with typecode |-
96 oveq1 a = 0 R a + R b = 0 R + R b
97 96 eqeq2d a = 0 R x = a + R b x = 0 R + R b
98 97 rexbidv a = 0 R b Base R × ˙ x x = a + R b b Base R × ˙ x x = 0 R + R b
99 98 adantl Could not format ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ a = ( 0g ` R ) ) -> ( E. b e. ( ( Base ` R ) .X. { x } ) x = ( a ( +g ` R ) b ) <-> E. b e. ( ( Base ` R ) .X. { x } ) x = ( ( 0g ` R ) ( +g ` R ) b ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ a = ( 0g ` R ) ) -> ( E. b e. ( ( Base ` R ) .X. { x } ) x = ( a ( +g ` R ) b ) <-> E. b e. ( ( Base ` R ) .X. { x } ) x = ( ( 0g ` R ) ( +g ` R ) b ) ) ) with typecode |-
100 oveq1 a = 1 R a R x = 1 R R x
101 100 eqeq2d a = 1 R x = a R x x = 1 R R x
102 101 adantl Could not format ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ a = ( 1r ` R ) ) -> ( x = ( a ( .r ` R ) x ) <-> x = ( ( 1r ` R ) ( .r ` R ) x ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ a = ( 1r ` R ) ) -> ( x = ( a ( .r ` R ) x ) <-> x = ( ( 1r ` R ) ( .r ` R ) x ) ) ) with typecode |-
103 4 17 18 ringlidm R Ring x Base R 1 R R x = x
104 14 29 103 syl2anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x ) with typecode |-
105 104 eqcomd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x = ( ( 1r ` R ) ( .r ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x = ( ( 1r ` R ) ( .r ` R ) x ) ) with typecode |-
106 66 102 105 rspcedvd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> E. a e. ( Base ` R ) x = ( a ( .r ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> E. a e. ( Base ` R ) x = ( a ( .r ` R ) x ) ) with typecode |-
107 57 58 1 59 60 29 elgrplsmsn Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( x e. ( ( Base ` R ) .X. { x } ) <-> E. a e. ( Base ` R ) x = ( a ( .r ` R ) x ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( x e. ( ( Base ` R ) .X. { x } ) <-> E. a e. ( Base ` R ) x = ( a ( .r ` R ) x ) ) ) with typecode |-
108 106 107 mpbird Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x e. ( ( Base ` R ) .X. { x } ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x e. ( ( Base ` R ) .X. { x } ) ) with typecode |-
109 oveq2 b = x 0 R + R b = 0 R + R x
110 109 eqeq2d b = x x = 0 R + R b x = 0 R + R x
111 110 adantl Could not format ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ b = x ) -> ( x = ( ( 0g ` R ) ( +g ` R ) b ) <-> x = ( ( 0g ` R ) ( +g ` R ) x ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) /\ b = x ) -> ( x = ( ( 0g ` R ) ( +g ` R ) b ) <-> x = ( ( 0g ` R ) ( +g ` R ) x ) ) ) with typecode |-
112 ringgrp R Ring R Grp
113 14 112 syl Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> R e. Grp ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> R e. Grp ) with typecode |-
114 4 33 93 grplid R Grp x Base R 0 R + R x = x
115 113 29 114 syl2anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( 0g ` R ) ( +g ` R ) x ) = x ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( 0g ` R ) ( +g ` R ) x ) = x ) with typecode |-
116 115 eqcomd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x = ( ( 0g ` R ) ( +g ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x = ( ( 0g ` R ) ( +g ` R ) x ) ) with typecode |-
117 108 111 116 rspcedvd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> E. b e. ( ( Base ` R ) .X. { x } ) x = ( ( 0g ` R ) ( +g ` R ) b ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> E. b e. ( ( Base ` R ) .X. { x } ) x = ( ( 0g ` R ) ( +g ` R ) b ) ) with typecode |-
118 95 99 117 rspcedvd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> E. a e. M E. b e. ( ( Base ` R ) .X. { x } ) x = ( a ( +g ` R ) b ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> E. a e. M E. b e. ( ( Base ` R ) .X. { x } ) x = ( a ( +g ` R ) b ) ) with typecode |-
119 simp-5l Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> R e. CRing ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> R e. CRing ) with typecode |-
120 4 33 67 lsmelvalx R CRing M Base R Base R × ˙ x Base R x M LSSum R Base R × ˙ x a M b Base R × ˙ x x = a + R b
121 119 24 82 120 syl3anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( x e. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) <-> E. a e. M E. b e. ( ( Base ` R ) .X. { x } ) x = ( a ( +g ` R ) b ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( x e. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) <-> E. a e. M E. b e. ( ( Base ` R ) .X. { x } ) x = ( a ( +g ` R ) b ) ) ) with typecode |-
122 118 121 mpbird Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x e. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> x e. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) ) with typecode |-
123 simpr Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> -. x e. M ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> -. x e. M ) with typecode |-
124 nelne1 x M LSSum R Base R × ˙ x ¬ x M M LSSum R Base R × ˙ x M
125 122 123 124 syl2anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) =/= M ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) =/= M ) with typecode |-
126 125 neneqd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> -. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = M ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> -. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = M ) with typecode |-
127 92 126 orcnd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) = ( Base ` R ) ) with typecode |-
128 66 127 eleqtrrd Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( 1r ` R ) e. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( 1r ` R ) e. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) ) with typecode |-
129 4 33 67 lsmelvalx R CRing M Base R Base R × ˙ x Base R 1 R M LSSum R Base R × ˙ x u M k Base R × ˙ x 1 R = u + R k
130 119 24 82 129 syl3anc Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( 1r ` R ) e. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) <-> E. u e. M E. k e. ( ( Base ` R ) .X. { x } ) ( 1r ` R ) = ( u ( +g ` R ) k ) ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> ( ( 1r ` R ) e. ( M ( LSSum ` R ) ( ( Base ` R ) .X. { x } ) ) <-> E. u e. M E. k e. ( ( Base ` R ) .X. { x } ) ( 1r ` R ) = ( u ( +g ` R ) k ) ) ) with typecode |-
131 128 130 mpbid Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> E. u e. M E. k e. ( ( Base ` R ) .X. { x } ) ( 1r ` R ) = ( u ( +g ` R ) k ) ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> E. u e. M E. k e. ( ( Base ` R ) .X. { x } ) ( 1r ` R ) = ( u ( +g ` R ) k ) ) with typecode |-
132 64 131 r19.29vva Could not format ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> y e. M ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) /\ -. x e. M ) -> y e. M ) with typecode |-
133 132 ex Could not format ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) -> ( -. x e. M -> y e. M ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) -> ( -. x e. M -> y e. M ) ) with typecode |-
134 133 orrd Could not format ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) -> ( x e. M \/ y e. M ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. M ) -> ( x e. M \/ y e. M ) ) with typecode |-
135 134 ex Could not format ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) e. M -> ( x e. M \/ y e. M ) ) ) : No typesetting found for |- ( ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) e. M -> ( x e. M \/ y e. M ) ) ) with typecode |-
136 135 anasss Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( .r ` R ) y ) e. M -> ( x e. M \/ y e. M ) ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( .r ` R ) y ) e. M -> ( x e. M \/ y e. M ) ) ) with typecode |-
137 136 ralrimivva Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. M -> ( x e. M \/ y e. M ) ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. M -> ( x e. M \/ y e. M ) ) ) with typecode |-
138 4 17 prmidl2 Could not format ( ( ( R e. Ring /\ M e. ( LIdeal ` R ) ) /\ ( M =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. M -> ( x e. M \/ y e. M ) ) ) ) -> M e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( LIdeal ` R ) ) /\ ( M =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. M -> ( x e. M \/ y e. M ) ) ) ) -> M e. ( PrmIdeal ` R ) ) with typecode |-
139 3 6 8 137 138 syl22anc Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( PrmIdeal ` R ) ) with typecode |-