ssdifidlprm

Description: If the set S of ssdifidl is multiplicatively closed, then the ideal i is prime. (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	ssdifidlprm.1	$⊢ B = {Base}_{R}$
	ssdifidlprm.2	$⊢ φ \to R \in CRing$
	ssdifidlprm.3	$⊢ φ \to I \in LIdeal (R)$
	ssdifidlprm.4	$⊢ φ \to S \in SubMnd (M)$
	ssdifidlprm.5	$⊢ M = {mulGrp}_{R}$
	ssdifidlprm.6	$⊢ φ \to S \cap I = \emptyset$
	ssdifidlprm.7	$⊢ P = \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\}$
Assertion	ssdifidlprm	$⊢ φ \to \exists i \in P (i \in PrmIdeal (R) \land \forall j \in P \neg i \subset j)$

Proof

Step	Hyp	Ref	Expression
1		ssdifidlprm.1	$⊢ B = {Base}_{R}$
2		ssdifidlprm.2	$⊢ φ \to R \in CRing$
3		ssdifidlprm.3	$⊢ φ \to I \in LIdeal (R)$
4		ssdifidlprm.4	$⊢ φ \to S \in SubMnd (M)$
5		ssdifidlprm.5	$⊢ M = {mulGrp}_{R}$
6		ssdifidlprm.6	$⊢ φ \to S \cap I = \emptyset$
7		ssdifidlprm.7	$⊢ P = \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\}$
8	2	ad2antrr	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to R \in CRing$
9	7	ssrab3	$⊢ P \subseteq LIdeal (R)$
10		simpr	$⊢ (φ \land i \in P) \to i \in P$
11	9 10	sselid	$⊢ (φ \land i \in P) \to i \in LIdeal (R)$
12	11	adantr	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to i \in LIdeal (R)$
13	2	crngringd	$⊢ φ \to R \in Ring$
14		eqid	$⊢ 1_{R} = 1_{R}$
15	1 14	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
16	13 15	syl	$⊢ φ \to 1_{R} \in B$
17	16	ad2antrr	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to 1_{R} \in B$
18		eqid	$⊢ LIdeal (R) = LIdeal (R)$
19	1 18	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq B$
20	11 19	syl	$⊢ (φ \land i \in P) \to i \subseteq B$
21	20	adantr	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to i \subseteq B$
22		incom	$⊢ S \cap p = p \cap S$
23	22	eqeq1i	$⊢ S \cap p = \emptyset \leftrightarrow p \cap S = \emptyset$
24		ineq1	$⊢ p = i \to p \cap S = i \cap S$
25	24	eqeq1d	$⊢ p = i \to (p \cap S = \emptyset \leftrightarrow i \cap S = \emptyset)$
26	23 25	bitrid	$⊢ p = i \to (S \cap p = \emptyset \leftrightarrow i \cap S = \emptyset)$
27		sseq2	$⊢ p = i \to (I \subseteq p \leftrightarrow I \subseteq i)$
28	26 27	anbi12d	$⊢ p = i \to ((S \cap p = \emptyset \land I \subseteq p) \leftrightarrow (i \cap S = \emptyset \land I \subseteq i))$
29	28 7	elrab2	$⊢ i \in P \leftrightarrow (i \in LIdeal (R) \land (i \cap S = \emptyset \land I \subseteq i))$
30	29	biimpi	$⊢ i \in P \to (i \in LIdeal (R) \land (i \cap S = \emptyset \land I \subseteq i))$
31	30	simprd	$⊢ i \in P \to (i \cap S = \emptyset \land I \subseteq i)$
32	31	simpld	$⊢ i \in P \to i \cap S = \emptyset$
33	32	ad2antlr	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to i \cap S = \emptyset$
34		reldisj	$⊢ i \subseteq B \to (i \cap S = \emptyset \leftrightarrow i \subseteq B ∖ S)$
35	34	biimpa	$⊢ (i \subseteq B \land i \cap S = \emptyset) \to i \subseteq B ∖ S$
36	21 33 35	syl2anc	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to i \subseteq B ∖ S$
37	5 14	ringidval	$⊢ 1_{R} = 0_{M}$
38	37	subm0cl	$⊢ S \in SubMnd (M) \to 1_{R} \in S$
39	4 38	syl	$⊢ φ \to 1_{R} \in S$
40	39	ad2antrr	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to 1_{R} \in S$
41		elndif	$⊢ 1_{R} \in S \to \neg 1_{R} \in (B ∖ S)$
42	40 41	syl	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to \neg 1_{R} \in (B ∖ S)$
43	36 42	ssneldd	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to \neg 1_{R} \in i$
44		nelne1	$⊢ (1_{R} \in B \land \neg 1_{R} \in i) \to B \neq i$
45	17 43 44	syl2anc	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to B \neq i$
46	45	necomd	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to i \neq B$
47	33	ad4antr	$⊢ ((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg (a \in i \lor b \in i)) \to i \cap S = \emptyset$
48		ioran	$⊢ \neg (a \in i \lor b \in i) \leftrightarrow (\neg a \in i \land \neg b \in i)$
49	18	lidlsubg	$⊢ (R \in Ring \land i \in LIdeal (R)) \to i \in SubGrp (R)$
50	13 11 49	syl2an2r	$⊢ (φ \land i \in P) \to i \in SubGrp (R)$
51	50	ad6antr	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i \in SubGrp (R)$
52	13	ad7antr	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to R \in Ring$
53		simp-5r	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to a \in B$
54	53	snssd	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \{a\} \subseteq B$
55		eqid	$⊢ RSpan (R) = RSpan (R)$
56	55 1 18	rspcl	$⊢ (R \in Ring \land \{a\} \subseteq B) \to RSpan (R) (\{a\}) \in LIdeal (R)$
57	52 54 56	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to RSpan (R) (\{a\}) \in LIdeal (R)$
58	18	lidlsubg	$⊢ (R \in Ring \land RSpan (R) (\{a\}) \in LIdeal (R)) \to RSpan (R) (\{a\}) \in SubGrp (R)$
59	52 57 58	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to RSpan (R) (\{a\}) \in SubGrp (R)$
60		eqid	$⊢ LSSum (R) = LSSum (R)$
61	60	lsmub1	$⊢ (i \in SubGrp (R) \land RSpan (R) (\{a\}) \in SubGrp (R)) \to i \subseteq i LSSum (R) RSpan (R) (\{a\})$
62	51 59 61	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i \subseteq i LSSum (R) RSpan (R) (\{a\})$
63	60	lsmub2	$⊢ (i \in SubGrp (R) \land RSpan (R) (\{a\}) \in SubGrp (R)) \to RSpan (R) (\{a\}) \subseteq i LSSum (R) RSpan (R) (\{a\})$
64	51 59 63	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to RSpan (R) (\{a\}) \subseteq i LSSum (R) RSpan (R) (\{a\})$
65	1 55	rspsnid	$⊢ (R \in Ring \land a \in B) \to a \in RSpan (R) (\{a\})$
66	52 53 65	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to a \in RSpan (R) (\{a\})$
67	64 66	sseldd	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to a \in (i LSSum (R) RSpan (R) (\{a\}))$
68		simplr	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \neg a \in i$
69	62 67 68	ssnelpssd	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i \subset i LSSum (R) RSpan (R) (\{a\})$
70	12	ad5antr	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i \in LIdeal (R)$
71	1 60 55 52 70 57	lsmidl	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i LSSum (R) RSpan (R) (\{a\}) \in LIdeal (R)$
72	31	simprd	$⊢ i \in P \to I \subseteq i$
73	72	adantl	$⊢ (φ \land i \in P) \to I \subseteq i$
74	73	ad6antr	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to I \subseteq i$
75	74 62	sstrd	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to I \subseteq i LSSum (R) RSpan (R) (\{a\})$
76	71 75	jca	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to (i LSSum (R) RSpan (R) (\{a\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{a\}))$
77		simp-6r	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \forall j \in P \neg i \subset j$
78		df-ral	$⊢ \forall j \in P \neg i \subset j \leftrightarrow \forall j (j \in P \to \neg i \subset j)$
79		con2b	$⊢ (j \in P \to \neg i \subset j) \leftrightarrow (i \subset j \to \neg j \in P)$
80	79	albii	$⊢ \forall j (j \in P \to \neg i \subset j) \leftrightarrow \forall j (i \subset j \to \neg j \in P)$
81	78 80	bitri	$⊢ \forall j \in P \neg i \subset j \leftrightarrow \forall j (i \subset j \to \neg j \in P)$
82	77 81	sylib	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \forall j (i \subset j \to \neg j \in P)$
83		ineq2	$⊢ p = j \to S \cap p = S \cap j$
84	83	eqeq1d	$⊢ p = j \to (S \cap p = \emptyset \leftrightarrow S \cap j = \emptyset)$
85		sseq2	$⊢ p = j \to (I \subseteq p \leftrightarrow I \subseteq j)$
86	84 85	anbi12d	$⊢ p = j \to ((S \cap p = \emptyset \land I \subseteq p) \leftrightarrow (S \cap j = \emptyset \land I \subseteq j))$
87	86 7	elrab2	$⊢ j \in P \leftrightarrow (j \in LIdeal (R) \land (S \cap j = \emptyset \land I \subseteq j))$
88	87	baib	$⊢ j \in LIdeal (R) \to (j \in P \leftrightarrow (S \cap j = \emptyset \land I \subseteq j))$
89	88	rbaibd	$⊢ (j \in LIdeal (R) \land I \subseteq j) \to (j \in P \leftrightarrow S \cap j = \emptyset)$
90	89	notbid	$⊢ (j \in LIdeal (R) \land I \subseteq j) \to (\neg j \in P \leftrightarrow \neg S \cap j = \emptyset)$
91	90	biimpcd	$⊢ \neg j \in P \to ((j \in LIdeal (R) \land I \subseteq j) \to \neg S \cap j = \emptyset)$
92	91	imim2i	$⊢ (i \subset j \to \neg j \in P) \to (i \subset j \to ((j \in LIdeal (R) \land I \subseteq j) \to \neg S \cap j = \emptyset))$
93	92	impd	$⊢ (i \subset j \to \neg j \in P) \to ((i \subset j \land (j \in LIdeal (R) \land I \subseteq j)) \to \neg S \cap j = \emptyset)$
94	93	alimi	$⊢ \forall j (i \subset j \to \neg j \in P) \to \forall j ((i \subset j \land (j \in LIdeal (R) \land I \subseteq j)) \to \neg S \cap j = \emptyset)$
95		ovex	$⊢ i LSSum (R) RSpan (R) (\{a\}) \in V$
96		psseq2	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to (i \subset j \leftrightarrow i \subset i LSSum (R) RSpan (R) (\{a\}))$
97		eleq1	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to (j \in LIdeal (R) \leftrightarrow i LSSum (R) RSpan (R) (\{a\}) \in LIdeal (R))$
98		sseq2	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to (I \subseteq j \leftrightarrow I \subseteq i LSSum (R) RSpan (R) (\{a\}))$
99	97 98	anbi12d	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to ((j \in LIdeal (R) \land I \subseteq j) \leftrightarrow (i LSSum (R) RSpan (R) (\{a\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{a\})))$
100	96 99	anbi12d	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to ((i \subset j \land (j \in LIdeal (R) \land I \subseteq j)) \leftrightarrow (i \subset i LSSum (R) RSpan (R) (\{a\}) \land (i LSSum (R) RSpan (R) (\{a\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{a\}))))$
101		ineq2	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to S \cap j = S \cap (i LSSum (R) RSpan (R) (\{a\}))$
102	101	eqeq1d	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to (S \cap j = \emptyset \leftrightarrow S \cap (i LSSum (R) RSpan (R) (\{a\})) = \emptyset)$
103	102	notbid	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to (\neg S \cap j = \emptyset \leftrightarrow \neg S \cap (i LSSum (R) RSpan (R) (\{a\})) = \emptyset)$
104	100 103	imbi12d	$⊢ j = i LSSum (R) RSpan (R) (\{a\}) \to (((i \subset j \land (j \in LIdeal (R) \land I \subseteq j)) \to \neg S \cap j = \emptyset) \leftrightarrow ((i \subset i LSSum (R) RSpan (R) (\{a\}) \land (i LSSum (R) RSpan (R) (\{a\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{a\}))) \to \neg S \cap (i LSSum (R) RSpan (R) (\{a\})) = \emptyset))$
105	95 104	spcv	$⊢ \forall j ((i \subset j \land (j \in LIdeal (R) \land I \subseteq j)) \to \neg S \cap j = \emptyset) \to ((i \subset i LSSum (R) RSpan (R) (\{a\}) \land (i LSSum (R) RSpan (R) (\{a\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{a\}))) \to \neg S \cap (i LSSum (R) RSpan (R) (\{a\})) = \emptyset)$
106	82 94 105	3syl	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to ((i \subset i LSSum (R) RSpan (R) (\{a\}) \land (i LSSum (R) RSpan (R) (\{a\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{a\}))) \to \neg S \cap (i LSSum (R) RSpan (R) (\{a\})) = \emptyset)$
107	69 76 106	mp2and	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \neg S \cap (i LSSum (R) RSpan (R) (\{a\})) = \emptyset$
108		neq0	$⊢ \neg S \cap (i LSSum (R) RSpan (R) (\{a\})) = \emptyset \leftrightarrow \exists e e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))$
109	107 108	sylib	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \exists e e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))$
110		simp-4r	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to b \in B$
111	110	snssd	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \{b\} \subseteq B$
112	55 1 18	rspcl	$⊢ (R \in Ring \land \{b\} \subseteq B) \to RSpan (R) (\{b\}) \in LIdeal (R)$
113	52 111 112	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to RSpan (R) (\{b\}) \in LIdeal (R)$
114	18	lidlsubg	$⊢ (R \in Ring \land RSpan (R) (\{b\}) \in LIdeal (R)) \to RSpan (R) (\{b\}) \in SubGrp (R)$
115	52 113 114	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to RSpan (R) (\{b\}) \in SubGrp (R)$
116	60	lsmub1	$⊢ (i \in SubGrp (R) \land RSpan (R) (\{b\}) \in SubGrp (R)) \to i \subseteq i LSSum (R) RSpan (R) (\{b\})$
117	51 115 116	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i \subseteq i LSSum (R) RSpan (R) (\{b\})$
118	60	lsmub2	$⊢ (i \in SubGrp (R) \land RSpan (R) (\{b\}) \in SubGrp (R)) \to RSpan (R) (\{b\}) \subseteq i LSSum (R) RSpan (R) (\{b\})$
119	51 115 118	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to RSpan (R) (\{b\}) \subseteq i LSSum (R) RSpan (R) (\{b\})$
120	1 55	rspsnid	$⊢ (R \in Ring \land b \in B) \to b \in RSpan (R) (\{b\})$
121	52 110 120	syl2anc	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to b \in RSpan (R) (\{b\})$
122	119 121	sseldd	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to b \in (i LSSum (R) RSpan (R) (\{b\}))$
123		simpr	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \neg b \in i$
124	117 122 123	ssnelpssd	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i \subset i LSSum (R) RSpan (R) (\{b\})$
125	1 60 55 52 70 113	lsmidl	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i LSSum (R) RSpan (R) (\{b\}) \in LIdeal (R)$
126	74 117	sstrd	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to I \subseteq i LSSum (R) RSpan (R) (\{b\})$
127	125 126	jca	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to (i LSSum (R) RSpan (R) (\{b\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{b\}))$
128		ovex	$⊢ i LSSum (R) RSpan (R) (\{b\}) \in V$
129		psseq2	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to (i \subset j \leftrightarrow i \subset i LSSum (R) RSpan (R) (\{b\}))$
130		eleq1	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to (j \in LIdeal (R) \leftrightarrow i LSSum (R) RSpan (R) (\{b\}) \in LIdeal (R))$
131		sseq2	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to (I \subseteq j \leftrightarrow I \subseteq i LSSum (R) RSpan (R) (\{b\}))$
132	130 131	anbi12d	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to ((j \in LIdeal (R) \land I \subseteq j) \leftrightarrow (i LSSum (R) RSpan (R) (\{b\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{b\})))$
133	129 132	anbi12d	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to ((i \subset j \land (j \in LIdeal (R) \land I \subseteq j)) \leftrightarrow (i \subset i LSSum (R) RSpan (R) (\{b\}) \land (i LSSum (R) RSpan (R) (\{b\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{b\}))))$
134		ineq2	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to S \cap j = S \cap (i LSSum (R) RSpan (R) (\{b\}))$
135	134	eqeq1d	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to (S \cap j = \emptyset \leftrightarrow S \cap (i LSSum (R) RSpan (R) (\{b\})) = \emptyset)$
136	135	notbid	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to (\neg S \cap j = \emptyset \leftrightarrow \neg S \cap (i LSSum (R) RSpan (R) (\{b\})) = \emptyset)$
137	133 136	imbi12d	$⊢ j = i LSSum (R) RSpan (R) (\{b\}) \to (((i \subset j \land (j \in LIdeal (R) \land I \subseteq j)) \to \neg S \cap j = \emptyset) \leftrightarrow ((i \subset i LSSum (R) RSpan (R) (\{b\}) \land (i LSSum (R) RSpan (R) (\{b\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{b\}))) \to \neg S \cap (i LSSum (R) RSpan (R) (\{b\})) = \emptyset))$
138	128 137	spcv	$⊢ \forall j ((i \subset j \land (j \in LIdeal (R) \land I \subseteq j)) \to \neg S \cap j = \emptyset) \to ((i \subset i LSSum (R) RSpan (R) (\{b\}) \land (i LSSum (R) RSpan (R) (\{b\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{b\}))) \to \neg S \cap (i LSSum (R) RSpan (R) (\{b\})) = \emptyset)$
139	82 94 138	3syl	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to ((i \subset i LSSum (R) RSpan (R) (\{b\}) \land (i LSSum (R) RSpan (R) (\{b\}) \in LIdeal (R) \land I \subseteq i LSSum (R) RSpan (R) (\{b\}))) \to \neg S \cap (i LSSum (R) RSpan (R) (\{b\})) = \emptyset)$
140	124 127 139	mp2and	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \neg S \cap (i LSSum (R) RSpan (R) (\{b\})) = \emptyset$
141		neq0	$⊢ \neg S \cap (i LSSum (R) RSpan (R) (\{b\})) = \emptyset \leftrightarrow \exists f f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))$
142	140 141	sylib	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to \exists f f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))$
143	142	adantr	$⊢ ((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \to \exists f f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))$
144	52	ad2antrr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to R \in Ring$
145	144	ad2antrr	$⊢ (((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \to R \in Ring$
146	53	ad2antrr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to a \in B$
147	146	ad2antrr	$⊢ (((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \to a \in B$
148		eqid	$⊢ \cdot_{R} = \cdot_{R}$
149	1 148 55	elrspsn	$⊢ (R \in Ring \land a \in B) \to (m \in RSpan (R) (\{a\}) \leftrightarrow \exists o \in B m = o \cdot_{R} a)$
150	145 147 149	syl2anc	$⊢ (((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \to (m \in RSpan (R) (\{a\}) \leftrightarrow \exists o \in B m = o \cdot_{R} a)$
151	144	ad6antr	$⊢ (((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \to R \in Ring$
152	110	ad2antrr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to b \in B$
153	152	ad6antr	$⊢ (((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \to b \in B$
154	1 148 55	elrspsn	$⊢ (R \in Ring \land b \in B) \to (n \in RSpan (R) (\{b\}) \leftrightarrow \exists q \in B n = q \cdot_{R} b)$
155	151 153 154	syl2anc	$⊢ (((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \to (n \in RSpan (R) (\{b\}) \leftrightarrow \exists q \in B n = q \cdot_{R} b)$
156		simp-7r	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to e = x +_{R} m$
157		simpllr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to f = y +_{R} n$
158	156 157	oveq12d	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to e \cdot_{R} f = (x +_{R} m) \cdot_{R} (y +_{R} n)$
159		simp-5r	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to m = o \cdot_{R} a$
160	159	oveq2d	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to x +_{R} m = x +_{R} (o \cdot_{R} a)$
161		simpr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to n = q \cdot_{R} b$
162	161	oveq2d	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to y +_{R} n = y +_{R} (q \cdot_{R} b)$
163	160 162	oveq12d	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (x +_{R} m) \cdot_{R} (y +_{R} n) = (x +_{R} (o \cdot_{R} a)) \cdot_{R} (y +_{R} (q \cdot_{R} b))$
164		eqid	$⊢ +_{R} = +_{R}$
165	151	ad2antrr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to R \in Ring$
166	21	ad7antr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to i \subseteq B$
167	166	ad4antr	$⊢ (((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \to i \subseteq B$
168	167	ad4antr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to i \subseteq B$
169		simp-8r	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to x \in i$
170	168 169	sseldd	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to x \in B$
171		simp-6r	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to o \in B$
172	146	ad8antr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to a \in B$
173	1 148 165 171 172	ringcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to o \cdot_{R} a \in B$
174		simp-4r	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to y \in i$
175	168 174	sseldd	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to y \in B$
176		simplr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to q \in B$
177	153	ad2antrr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to b \in B$
178	1 148 165 176 177	ringcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to q \cdot_{R} b \in B$
179	1 164 148 165 170 173 175 178	ringdi22	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (x +_{R} (o \cdot_{R} a)) \cdot_{R} (y +_{R} (q \cdot_{R} b)) = ((x \cdot_{R} y) +_{R} ((o \cdot_{R} a) \cdot_{R} y)) +_{R} ((x \cdot_{R} (q \cdot_{R} b)) +_{R} ((o \cdot_{R} a) \cdot_{R} (q \cdot_{R} b)))$
180	158 163 179	3eqtrd	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to e \cdot_{R} f = ((x \cdot_{R} y) +_{R} ((o \cdot_{R} a) \cdot_{R} y)) +_{R} ((x \cdot_{R} (q \cdot_{R} b)) +_{R} ((o \cdot_{R} a) \cdot_{R} (q \cdot_{R} b)))$
181	70	ad2antrr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to i \in LIdeal (R)$
182	181	ad8antr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to i \in LIdeal (R)$
183	165 182 49	syl2anc	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to i \in SubGrp (R)$
184	18 1 148 165 182 170 174	lidlmcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to x \cdot_{R} y \in i$
185	18 1 148 165 182 173 174	lidlmcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (o \cdot_{R} a) \cdot_{R} y \in i$
186	164 183 184 185	subgcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (x \cdot_{R} y) +_{R} ((o \cdot_{R} a) \cdot_{R} y) \in i$
187	8	ad7antr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to R \in CRing$
188	187	ad4antr	$⊢ (((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \to R \in CRing$
189	188	ad4antr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to R \in CRing$
190	1 148 189 170 178	crngcomd	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to x \cdot_{R} (q \cdot_{R} b) = (q \cdot_{R} b) \cdot_{R} x$
191	18 1 148 165 182 178 169	lidlmcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (q \cdot_{R} b) \cdot_{R} x \in i$
192	190 191	eqeltrd	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to x \cdot_{R} (q \cdot_{R} b) \in i$
193	1 148	cringm4	$⊢ (R \in CRing \land (o \in B \land a \in B) \land (q \in B \land b \in B)) \to (o \cdot_{R} a) \cdot_{R} (q \cdot_{R} b) = (o \cdot_{R} q) \cdot_{R} (a \cdot_{R} b)$
194	189 171 172 176 177 193	syl122anc	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (o \cdot_{R} a) \cdot_{R} (q \cdot_{R} b) = (o \cdot_{R} q) \cdot_{R} (a \cdot_{R} b)$
195	1 148 165 171 176	ringcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to o \cdot_{R} q \in B$
196		simp-5r	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to a \cdot_{R} b \in i$
197	196	ad8antr	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to a \cdot_{R} b \in i$
198	18 1 148 165 182 195 197	lidlmcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (o \cdot_{R} q) \cdot_{R} (a \cdot_{R} b) \in i$
199	194 198	eqeltrd	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (o \cdot_{R} a) \cdot_{R} (q \cdot_{R} b) \in i$
200	164 183 192 199	subgcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to (x \cdot_{R} (q \cdot_{R} b)) +_{R} ((o \cdot_{R} a) \cdot_{R} (q \cdot_{R} b)) \in i$
201	164 183 186 200	subgcld	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to ((x \cdot_{R} y) +_{R} ((o \cdot_{R} a) \cdot_{R} y)) +_{R} ((x \cdot_{R} (q \cdot_{R} b)) +_{R} ((o \cdot_{R} a) \cdot_{R} (q \cdot_{R} b))) \in i$
202	180 201	eqeltrd	$⊢ (((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land q \in B) \land n = q \cdot_{R} b) \to e \cdot_{R} f \in i$
203	202	r19.29an	$⊢ ((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land \exists q \in B n = q \cdot_{R} b) \to e \cdot_{R} f \in i$
204	155 203	sylbida	$⊢ ((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land f = y +_{R} n) \land n \in RSpan (R) (\{b\})) \to e \cdot_{R} f \in i$
205	204	an32s	$⊢ ((((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land n \in RSpan (R) (\{b\})) \land f = y +_{R} n) \to e \cdot_{R} f \in i$
206	205	r19.29an	$⊢ (((((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \land y \in i) \land \exists n \in RSpan (R) (\{b\}) f = y +_{R} n) \to e \cdot_{R} f \in i$
207	113	ad2antrr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to RSpan (R) (\{b\}) \in LIdeal (R)$
208	1 18	lidlss	$⊢ RSpan (R) (\{b\}) \in LIdeal (R) \to RSpan (R) (\{b\}) \subseteq B$
209	207 208	syl	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to RSpan (R) (\{b\}) \subseteq B$
210	209	ad4antr	$⊢ (((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \to RSpan (R) (\{b\}) \subseteq B$
211		simpr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))$
212	211	elin2d	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to f \in (i LSSum (R) RSpan (R) (\{b\}))$
213	212	ad4antr	$⊢ (((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \to f \in (i LSSum (R) RSpan (R) (\{b\}))$
214	1 164 60	lsmelvalx	$⊢ (R \in CRing \land i \subseteq B \land RSpan (R) (\{b\}) \subseteq B) \to (f \in (i LSSum (R) RSpan (R) (\{b\})) \leftrightarrow \exists y \in i \exists n \in RSpan (R) (\{b\}) f = y +_{R} n)$
215	214	biimpa	$⊢ ((R \in CRing \land i \subseteq B \land RSpan (R) (\{b\}) \subseteq B) \land f \in (i LSSum (R) RSpan (R) (\{b\}))) \to \exists y \in i \exists n \in RSpan (R) (\{b\}) f = y +_{R} n$
216	188 167 210 213 215	syl31anc	$⊢ (((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \to \exists y \in i \exists n \in RSpan (R) (\{b\}) f = y +_{R} n$
217	206 216	r19.29a	$⊢ (((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land o \in B) \land m = o \cdot_{R} a) \to e \cdot_{R} f \in i$
218	217	r19.29an	$⊢ ((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land \exists o \in B m = o \cdot_{R} a) \to e \cdot_{R} f \in i$
219	150 218	sylbida	$⊢ ((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land e = x +_{R} m) \land m \in RSpan (R) (\{a\})) \to e \cdot_{R} f \in i$
220	219	an32s	$⊢ ((((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land m \in RSpan (R) (\{a\})) \land e = x +_{R} m) \to e \cdot_{R} f \in i$
221	220	r19.29an	$⊢ (((((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \land x \in i) \land \exists m \in RSpan (R) (\{a\}) e = x +_{R} m) \to e \cdot_{R} f \in i$
222	57	ad2antrr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to RSpan (R) (\{a\}) \in LIdeal (R)$
223	1 18	lidlss	$⊢ RSpan (R) (\{a\}) \in LIdeal (R) \to RSpan (R) (\{a\}) \subseteq B$
224	222 223	syl	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to RSpan (R) (\{a\}) \subseteq B$
225		simplr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))$
226	225	elin2d	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to e \in (i LSSum (R) RSpan (R) (\{a\}))$
227	1 164 60	lsmelvalx	$⊢ (R \in CRing \land i \subseteq B \land RSpan (R) (\{a\}) \subseteq B) \to (e \in (i LSSum (R) RSpan (R) (\{a\})) \leftrightarrow \exists x \in i \exists m \in RSpan (R) (\{a\}) e = x +_{R} m)$
228	227	biimpa	$⊢ ((R \in CRing \land i \subseteq B \land RSpan (R) (\{a\}) \subseteq B) \land e \in (i LSSum (R) RSpan (R) (\{a\}))) \to \exists x \in i \exists m \in RSpan (R) (\{a\}) e = x +_{R} m$
229	187 166 224 226 228	syl31anc	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to \exists x \in i \exists m \in RSpan (R) (\{a\}) e = x +_{R} m$
230	221 229	r19.29a	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to e \cdot_{R} f \in i$
231	5 148	mgpplusg	$⊢ \cdot_{R} = +_{M}$
232	4	ad9antr	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to S \in SubMnd (M)$
233	225	elin1d	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to e \in S$
234	211	elin1d	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to f \in S$
235	231 232 233 234	submcld	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to e \cdot_{R} f \in S$
236	230 235	elind	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to e \cdot_{R} f \in (i \cap S)$
237	236	ne0d	$⊢ (((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \land f \in (S \cap (i LSSum (R) RSpan (R) (\{b\})))) \to i \cap S \neq \emptyset$
238	143 237	exlimddv	$⊢ ((((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \land e \in (S \cap (i LSSum (R) RSpan (R) (\{a\})))) \to i \cap S \neq \emptyset$
239	109 238	exlimddv	$⊢ (((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg a \in i) \land \neg b \in i) \to i \cap S \neq \emptyset$
240	239	anasss	$⊢ ((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land (\neg a \in i \land \neg b \in i)) \to i \cap S \neq \emptyset$
241	48 240	sylan2b	$⊢ ((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg (a \in i \lor b \in i)) \to i \cap S \neq \emptyset$
242	241	neneqd	$⊢ ((((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \land \neg (a \in i \lor b \in i)) \to \neg i \cap S = \emptyset$
243	47 242	condan	$⊢ (((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \land a \cdot_{R} b \in i) \to (a \in i \lor b \in i)$
244	243	ex	$⊢ ((((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land a \in B) \land b \in B) \to (a \cdot_{R} b \in i \to (a \in i \lor b \in i))$
245	244	anasss	$⊢ (((φ \land i \in P) \land \forall j \in P \neg i \subset j) \land (a \in B \land b \in B)) \to (a \cdot_{R} b \in i \to (a \in i \lor b \in i))$
246	245	ralrimivva	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to \forall a \in B \forall b \in B (a \cdot_{R} b \in i \to (a \in i \lor b \in i))$
247	1 148	isprmidlc	$⊢ R \in CRing \to (i \in PrmIdeal (R) \leftrightarrow (i \in LIdeal (R) \land i \neq B \land \forall a \in B \forall b \in B (a \cdot_{R} b \in i \to (a \in i \lor b \in i))))$
248	247	biimpar	$⊢ (R \in CRing \land (i \in LIdeal (R) \land i \neq B \land \forall a \in B \forall b \in B (a \cdot_{R} b \in i \to (a \in i \lor b \in i)))) \to i \in PrmIdeal (R)$
249	8 12 46 246 248	syl13anc	$⊢ ((φ \land i \in P) \land \forall j \in P \neg i \subset j) \to i \in PrmIdeal (R)$
250	249	anasss	$⊢ (φ \land (i \in P \land \forall j \in P \neg i \subset j)) \to i \in PrmIdeal (R)$
251		simprr	$⊢ (φ \land (i \in P \land \forall j \in P \neg i \subset j)) \to \forall j \in P \neg i \subset j$
252	250 251	jca	$⊢ (φ \land (i \in P \land \forall j \in P \neg i \subset j)) \to (i \in PrmIdeal (R) \land \forall j \in P \neg i \subset j)$
253	5 1	mgpbas	$⊢ B = {Base}_{M}$
254	253	submss	$⊢ S \in SubMnd (M) \to S \subseteq B$
255	4 254	syl	$⊢ φ \to S \subseteq B$
256	1 13 3 255 6 7	ssdifidl	$⊢ φ \to \exists i \in P \forall j \in P \neg i \subset j$
257	252 256	reximddv	$⊢ φ \to \exists i \in P (i \in PrmIdeal (R) \land \forall j \in P \neg i \subset j)$

Metamath Proof Explorer

Theorem ssdifidlprm

Proof