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 
|- .X. = ( LSSum ` ( mulGrp ` R ) )
Assertion mxidlprm 
|- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( PrmIdeal ` R ) )

Proof

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