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{˙}{\times} = LSSum ({mulGrp}_{R})$
	Assertion	mxidlprm	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to M \in PrmIdeal (R)$

Proof

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

Metamath Proof Explorer

Theorem mxidlprm

Proof