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	$$⊢\underset{\dot{}}{\times }=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
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	$$⊢\underset{\dot{}}{\times }=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
2		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{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	$$⊢{\mathrm{Base}}_R={\mathrm{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	$$⊢{\cdot }_R={\cdot }_R$$
18		eqid	$$⊢1_R=1_R$$
19	4 17 18	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge y\in {\mathrm{Base}}_R\right)\to 1_R{\cdot }_{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	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
22	4 21	lidlss	$$⊢M\in \mathrm{LIdeal}\left(R\right)\to M\subseteq {\mathrm{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	$$⊢\left(R\in \mathrm{Ring}\wedge a\in {\mathrm{Base}}_R\wedge x\in {\mathrm{Base}}_R\right)\to a{\cdot }_{R}x\in {\mathrm{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	$$⊢\left(R\in \mathrm{Ring}\wedge \left(u\in {\mathrm{Base}}_R\wedge a{\cdot }_{R}x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to \left(u{+}_R\left(a{\cdot }_{R}x\right)\right){\cdot }_{R}y=\left(u{\cdot }_{R}y\right){+}_R\left(\left(a{\cdot }_{R}x\right){\cdot }_{R}y\right)$$
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	$$⊢\left(R\in \mathrm{CRing}\wedge y\in {\mathrm{Base}}_R\wedge u\in {\mathrm{Base}}_R\right)\to y{\cdot }_{R}u=u{\cdot }_{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	$$⊢\left(\left(R\in \mathrm{Ring}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\wedge \left(y\in {\mathrm{Base}}_R\wedge u\in M\right)\right)\to y{\cdot }_{R}u\in 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	$$⊢\left(R\in \mathrm{Ring}\wedge \left(a\in {\mathrm{Base}}_R\wedge x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to \left(a{\cdot }_{R}x\right){\cdot }_{R}y=a{\cdot }_R\left(x{\cdot }_{R}y\right)$$
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	$$⊢\left(\left(R\in \mathrm{Ring}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\wedge \left(a\in {\mathrm{Base}}_R\wedge x{\cdot }_{R}y\in M\right)\right)\to a{\cdot }_R\left(x{\cdot }_{R}y\right)\in 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	$$⊢\left(\left(R\in \mathrm{Ring}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\wedge \left(u{\cdot }_{R}y\in M\wedge \left(a{\cdot }_{R}x\right){\cdot }_{R}y\in M\right)\right)\to \left(u{\cdot }_{R}y\right){+}_R\left(\left(a{\cdot }_{R}x\right){\cdot }_{R}y\right)\in 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	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
57	56 4	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
58	56 17	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{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\in \mathrm{Ring}\to 1_R\in {\mathrm{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	$$⊢\mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(R\right)$$
68		eqid	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{RSpan}\left(R\right)$$
69		eqid	$$⊢\mathrm{LPIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)$$
70	69 21	lpiss	$$⊢R\in \mathrm{Ring}\to \mathrm{LPIdeal}\left(R\right)\subseteq \mathrm{LIdeal}\left(R\right)$$
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\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{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	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
78		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
79	77 78	lspssid	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\wedge M\subseteq {\mathrm{Base}}_R\right)\to M\subseteq \mathrm{RSpan}\left(R\right)\left(M\right)$$
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\subseteq M\cup \left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)$$
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	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\wedge M\cup \left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)\subseteq {\mathrm{Base}}_R\wedge M\subseteq M\cup \left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)\right)\to \mathrm{RSpan}\left(R\right)\left(M\right)\subseteq \mathrm{RSpan}\left(R\right)\left(M\cup \left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)\right)$$
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	$$⊢\left(R\in \mathrm{Ring}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\to 0_R\in 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\to a{+}_{R}b=0_R{+}_{R}b$$
97	96	eqeq2d	$$⊢a=0_R\to \left(x=a{+}_{R}b\leftrightarrow x=0_R{+}_{R}b\right)$$
98	97	rexbidv	$$⊢a=0_R\to \left(\exists b\in \left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)x=a{+}_{R}b\leftrightarrow \exists b\in \left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)x=0_R{+}_{R}b\right)$$
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\to a{\cdot }_{R}x=1_R{\cdot }_{R}x$$
101	100	eqeq2d	$$⊢a=1_R\to \left(x=a{\cdot }_{R}x\leftrightarrow x=1_R{\cdot }_{R}x\right)$$
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	$$⊢\left(R\in \mathrm{Ring}\wedge x\in {\mathrm{Base}}_R\right)\to 1_R{\cdot }_{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\to 0_R{+}_{R}b=0_R{+}_{R}x$$
110	109	eqeq2d	$$⊢b=x\to \left(x=0_R{+}_{R}b\leftrightarrow x=0_R{+}_{R}x\right)$$
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\in \mathrm{Ring}\to R\in \mathrm{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	$$⊢\left(R\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_R\right)\to 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	$$⊢\left(R\in \mathrm{CRing}\wedge M\subseteq {\mathrm{Base}}_R\wedge {\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\subseteq {\mathrm{Base}}_R\right)\to \left(x\in \left(M\mathrm{LSSum}\left(R\right)\left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)\right)\leftrightarrow \exists a\in M\exists b\in \left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)x=a{+}_{R}b\right)$$
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	$$⊢\left(x\in \left(M\mathrm{LSSum}\left(R\right)\left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)\right)\wedge \neg x\in M\right)\to M\mathrm{LSSum}\left(R\right)\left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)\ne 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	$$⊢\left(R\in \mathrm{CRing}\wedge M\subseteq {\mathrm{Base}}_R\wedge {\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\subseteq {\mathrm{Base}}_R\right)\to \left(1_R\in \left(M\mathrm{LSSum}\left(R\right)\left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)\right)\leftrightarrow \exists u\in M\exists k\in \left({\mathrm{Base}}_R\underset{\dot{}}{\times }\left\{x\right\}\right)1_R=u{+}_{R}k\right)$$
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 |-