ssdifidlprm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ssdifidlprm		Structured version Visualization version GIF version

Theorem ssdifidlprm 21622

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

**Hypotheses**
Ref	Expression
ssdifidlprm.1	⊢ 𝐵 = (Base‘𝑅)
ssdifidlprm.2	⊢ (𝜑 → 𝑅 ∈ CRing)
ssdifidlprm.3	⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
ssdifidlprm.4	⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))
ssdifidlprm.5	⊢ 𝑀 = (mulGrp‘𝑅)
ssdifidlprm.6	⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)
ssdifidlprm.7	⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}

**Assertion**
Ref	Expression
ssdifidlprm	⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))

Distinct variable groups: 𝑗,𝐼,𝑝 𝑃,𝑖,𝑗 𝑅,𝑗,𝑝 𝑆,𝑗,𝑝 𝜑,𝑖,𝑗 𝑖,𝑝,𝑗 Allowed substitution hints: 𝜑(𝑝) 𝐵(𝑖, 𝑗, 𝑝) 𝑃(𝑝) 𝑅(𝑖) 𝑆(𝑖) 𝐼(𝑖) 𝑀(𝑖, 𝑗, 𝑝)

Proof of Theorem ssdifidlprm Dummy variables 𝑎 𝑏 𝑒 𝑓 𝑚 𝑛 𝑜 𝑞 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssdifidlprm.2	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CRing)
2	1	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑅 ∈ CRing)
3		ssdifidlprm.7	. . . . . . . 8 ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}
4	3	ssrab3 4030	. . . . . . 7 ⊢ 𝑃 ⊆ (LIdeal‘𝑅)
5		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ 𝑃)
6	4, 5	sselid 3929	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (LIdeal‘𝑅))
7	6	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (LIdeal‘𝑅))
8	1	crngringd 20453	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
9		ssdifidlprm.1	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
10		eqid 2761	. . . . . . . . . 10 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
11	9, 10	ringidcl 20474	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝐵)
12	8, 11	syl 18	. . . . . . . 8 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝐵)
13	12	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1_r‘𝑅) ∈ 𝐵)
14		eqid 2761	. . . . . . . . . . . 12 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
15	9, 14	lidlss 21470	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵)
16	6, 15	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ⊆ 𝐵)
17	16	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ 𝐵)
18		incom 4155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ 𝑝) = (𝑝 ∩ 𝑆)
19	18	eqeq1i 2766	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑝 ∩ 𝑆) = ∅)
20		ineq1 4159	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑖 → (𝑝 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	eqeq1d 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑖 → ((𝑝 ∩ 𝑆) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
22	19, 21	bitrid 286	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
23		sseq2 3957	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑖))
24	22, 23	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑖 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
25	24, 3	elrab2 3649	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝑃 ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
26	25	biimpi 219	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑃 → (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
27	26	simprd 501	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝑃 → ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖))
28	27	simpld 500	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑃 → (𝑖 ∩ 𝑆) = ∅)
29	28	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (𝑖 ∩ 𝑆) = ∅)
30		reldisj 4406	. . . . . . . . . 10 ⊢ (𝑖 ⊆ 𝐵 → ((𝑖 ∩ 𝑆) = ∅ ↔ 𝑖 ⊆ (𝐵 ∖ 𝑆)))
31	30	biimpa 482	. . . . . . . . 9 ⊢ ((𝑖 ⊆ 𝐵 ∧ (𝑖 ∩ 𝑆) = ∅) → 𝑖 ⊆ (𝐵 ∖ 𝑆))
32	17, 29, 31	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ (𝐵 ∖ 𝑆))
33		ssdifidlprm.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))
34		ssdifidlprm.5	. . . . . . . . . . . . 13 ⊢ 𝑀 = (mulGrp‘𝑅)
35	34, 10	ringidval 20389	. . . . . . . . . . . 12 ⊢ (1_r‘𝑅) = (0_g‘𝑀)
36	35	subm0cl 18986	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → (1_r‘𝑅) ∈ 𝑆)
37	33, 36	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝑆)
38	37	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1_r‘𝑅) ∈ 𝑆)
39		elndif 4080	. . . . . . . . 9 ⊢ ((1_r‘𝑅) ∈ 𝑆 → ¬ (1_r‘𝑅) ∈ (𝐵 ∖ 𝑆))
40	38, 39	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1_r‘𝑅) ∈ (𝐵 ∖ 𝑆))
41	32, 40	ssneldd 3934	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1_r‘𝑅) ∈ 𝑖)
42		nelne1 3053	. . . . . . 7 ⊢ (((1_r‘𝑅) ∈ 𝐵 ∧ ¬ (1_r‘𝑅) ∈ 𝑖) → 𝐵 ≠ 𝑖)
43	13, 41, 42	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝐵 ≠ 𝑖)
44	43	necomd 3011	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ≠ 𝐵)
45	29	ad4antr 745	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) = ∅)
46		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖) ↔ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖))
47	14	lidlsubg 21482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) → 𝑖 ∈ (SubGrp‘𝑅))
48	8, 6, 47	syl2an2r 698	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (SubGrp‘𝑅))
49	48	ad6antr 749	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (SubGrp‘𝑅))
50	8	ad7antr 751	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑅 ∈ Ring)
51		simp-5r 798	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ 𝐵)
52	51	snssd 4747	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑎} ⊆ 𝐵)
53		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (RSpan‘𝑅) = (RSpan‘𝑅)
54	53, 9, 14	rspcl 21498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ {𝑎} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
55	50, 52, 54	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
56	14	lidlsubg 21482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
57	50, 55, 56	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
58		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (LSSum‘𝑅) = (LSSum‘𝑅)
59	58	lsmub1 19851	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
60	49, 57, 59	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
61	58	lsmub2 19852	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
62	49, 57, 61	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
63	9, 53	rspsnid 21507	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
64	50, 51, 63	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
65	62, 64	sseldd 3932	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
66		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑎 ∈ 𝑖)
67	60, 65, 66	ssnelpssd 4064	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
68	7	ad5antr 747	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
69	9, 58, 53, 50, 68, 55	lsmidl 21518	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅))
70	27	simprd 501	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑃 → 𝐼 ⊆ 𝑖)
71	70	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝐼 ⊆ 𝑖)
72	71	ad6antr 749	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ 𝑖)
73	72, 60	sstrd 3941	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
74	69, 73	jca 521	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
75		simp-6r 800	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
76		df-ral 3078	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗))
77		con2b 362	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ (𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
78	77	albii 1852	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
79	76, 78	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
80	75, 79	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
81		ineq2 4160	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 = 𝑗 → (𝑆 ∩ 𝑝) = (𝑆 ∩ 𝑗))
82	81	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅))
83		sseq2 3957	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑗))
84	82, 83	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑗 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
85	84, 3	elrab2 3649	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ 𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
86	85	baib 545	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (LIdeal‘𝑅) → (𝑗 ∈ 𝑃 ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
87	86	rbaibd 550	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → (𝑗 ∈ 𝑃 ↔ (𝑆 ∩ 𝑗) = ∅))
88	87	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → (¬ 𝑗 ∈ 𝑃 ↔ ¬ (𝑆 ∩ 𝑗) = ∅))
89	88	biimpcd 252	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑗 ∈ 𝑃 → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → ¬ (𝑆 ∩ 𝑗) = ∅))
90	89	imim2i 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → (𝑖 ⊊ 𝑗 → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → ¬ (𝑆 ∩ 𝑗) = ∅)))
91	90	impd 416	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
92	91	alimi 1844	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
93		ovex 7445	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ V
94		psseq2 4039	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
95		eleq1 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅)))
96		sseq2 3957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
97	95, 96	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) ↔ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))))
98	94, 97	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) ↔ (𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))))
99		ineq2 4160	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
100	99	eqeq1d 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑆 ∩ 𝑗) = ∅ ↔ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
101	100	notbid 321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (¬ (𝑆 ∩ 𝑗) = ∅ ↔ ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
102	98, 101	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) ↔ ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅)))
103	93, 102	spcv 3560	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) → ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
104	80, 92, 103	3syl 19	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
105	67, 74, 104	mp2and 712	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅)
106		neq0 4299	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅ ↔ ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
107	105, 106	sylib 221	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
108		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ 𝐵)
109	108	snssd 4747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑏} ⊆ 𝐵)
110	53, 9, 14	rspcl 21498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ {𝑏} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
111	50, 109, 110	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
112	14	lidlsubg 21482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
113	50, 111, 112	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
114	58	lsmub1 19851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
115	49, 113, 114	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
116	58	lsmub2 19852	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
117	49, 113, 116	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
118	9, 53	rspsnid 21507	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
119	50, 108, 118	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
120	117, 119	sseldd 3932	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
121		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑏 ∈ 𝑖)
122	115, 120, 121	ssnelpssd 4064	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
123	9, 58, 53, 50, 68, 111	lsmidl 21518	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅))
124	72, 115	sstrd 3941	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
125	123, 124	jca 521	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
126		ovex 7445	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ V
127		psseq2 4039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
128		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅)))
129		sseq2 3957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
130	128, 129	anbi12d 644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) ↔ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))))
131	127, 130	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) ↔ (𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))))
132		ineq2 4160	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
133	132	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑆 ∩ 𝑗) = ∅ ↔ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
134	133	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (¬ (𝑆 ∩ 𝑗) = ∅ ↔ ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
135	131, 134	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) ↔ ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅)))
136	126, 135	spcv 3560	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) → ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
137	80, 92, 136	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
138	122, 125, 137	mp2and 712	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅)
139		neq0 4299	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅ ↔ ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
140	138, 139	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
141	140	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
142	50	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑅 ∈ Ring)
143	142	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) → 𝑅 ∈ Ring)
144	51	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑎 ∈ 𝐵)
145	144	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) → 𝑎 ∈ 𝐵)
146		eqid 2761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._r‘𝑅) = (._r‘𝑅)
147	9, 146, 53	elrspsn 21505	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → (𝑚 ∈ ((RSpan‘𝑅)‘{𝑎}) ↔ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(._r‘𝑅)𝑎)))
148	143, 145, 147	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) → (𝑚 ∈ ((RSpan‘𝑅)‘{𝑎}) ↔ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(._r‘𝑅)𝑎)))
149	142	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) → 𝑅 ∈ Ring)
150	108	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑏 ∈ 𝐵)
151	150	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) → 𝑏 ∈ 𝐵)
152	9, 146, 53	elrspsn 21505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → (𝑛 ∈ ((RSpan‘𝑅)‘{𝑏}) ↔ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(._r‘𝑅)𝑏)))
153	149, 151, 152	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) → (𝑛 ∈ ((RSpan‘𝑅)‘{𝑏}) ↔ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(._r‘𝑅)𝑏)))
154		simp-7r 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑒 = (𝑥(+_g‘𝑅)𝑚))
155		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑓 = (𝑦(+_g‘𝑅)𝑛))
156	154, 155	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑒(._r‘𝑅)𝑓) = ((𝑥(+_g‘𝑅)𝑚)(._r‘𝑅)(𝑦(+_g‘𝑅)𝑛)))
157		simp-5r 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑚 = (𝑜(._r‘𝑅)𝑎))
158	157	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑥(+_g‘𝑅)𝑚) = (𝑥(+_g‘𝑅)(𝑜(._r‘𝑅)𝑎)))
159		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑛 = (𝑞(._r‘𝑅)𝑏))
160	159	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑦(+_g‘𝑅)𝑛) = (𝑦(+_g‘𝑅)(𝑞(._r‘𝑅)𝑏)))
161	158, 160	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑥(+_g‘𝑅)𝑚)(._r‘𝑅)(𝑦(+_g‘𝑅)𝑛)) = ((𝑥(+_g‘𝑅)(𝑜(._r‘𝑅)𝑎))(._r‘𝑅)(𝑦(+_g‘𝑅)(𝑞(._r‘𝑅)𝑏))))
162		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
163	149	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑅 ∈ Ring)
164	17	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑖 ⊆ 𝐵)
165	164	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) → 𝑖 ⊆ 𝐵)
166	165	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑖 ⊆ 𝐵)
167		simp-8r 804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑥 ∈ 𝑖)
168	166, 167	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑥 ∈ 𝐵)
169		simp-6r 800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑜 ∈ 𝐵)
170	144	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑎 ∈ 𝐵)
171	9, 146, 163, 169, 170	ringcld 20464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑜(._r‘𝑅)𝑎) ∈ 𝐵)
172		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑦 ∈ 𝑖)
173	166, 172	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑦 ∈ 𝐵)
174		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑞 ∈ 𝐵)
175	151	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑏 ∈ 𝐵)
176	9, 146, 163, 174, 175	ringcld 20464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑞(._r‘𝑅)𝑏) ∈ 𝐵)
177	9, 162, 146, 163, 168, 171, 173, 176	ringdi22 20473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑥(+_g‘𝑅)(𝑜(._r‘𝑅)𝑎))(._r‘𝑅)(𝑦(+_g‘𝑅)(𝑞(._r‘𝑅)𝑏))) = (((𝑥(._r‘𝑅)𝑦)(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)𝑦))(+_g‘𝑅)((𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏))(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)))))
178	156, 161, 177	3eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑒(._r‘𝑅)𝑓) = (((𝑥(._r‘𝑅)𝑦)(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)𝑦))(+_g‘𝑅)((𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏))(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)))))
179	68	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑖 ∈ (LIdeal‘𝑅))
180	179	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑖 ∈ (LIdeal‘𝑅))
181	163, 180, 47	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑖 ∈ (SubGrp‘𝑅))
182	14, 9, 146, 163, 180, 168, 172	lidlmcld 21486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑥(._r‘𝑅)𝑦) ∈ 𝑖)
183	14, 9, 146, 163, 180, 171, 172	lidlmcld 21486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)𝑦) ∈ 𝑖)
184	162, 181, 182, 183	subgcld 19327	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑥(._r‘𝑅)𝑦)(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)𝑦)) ∈ 𝑖)
185	2	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑅 ∈ CRing)
186	185	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) → 𝑅 ∈ CRing)
187	186	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → 𝑅 ∈ CRing)
188	9, 146, 187, 168, 176	crngcomd 20462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)) = ((𝑞(._r‘𝑅)𝑏)(._r‘𝑅)𝑥))
189	14, 9, 146, 163, 180, 176, 167	lidlmcld 21486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑞(._r‘𝑅)𝑏)(._r‘𝑅)𝑥) ∈ 𝑖)
190	188, 189	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)) ∈ 𝑖)
191	9, 146	cringm4 21607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ CRing ∧ (𝑜 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑞 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)) = ((𝑜(._r‘𝑅)𝑞)(._r‘𝑅)(𝑎(._r‘𝑅)𝑏)))
192	187, 169, 170, 174, 175, 191	syl122anc 1406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)) = ((𝑜(._r‘𝑅)𝑞)(._r‘𝑅)(𝑎(._r‘𝑅)𝑏)))
193	9, 146, 163, 169, 174	ringcld 20464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑜(._r‘𝑅)𝑞) ∈ 𝐵)
194		simp-5r 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑎(._r‘𝑅)𝑏) ∈ 𝑖)
195	194	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑎(._r‘𝑅)𝑏) ∈ 𝑖)
196	14, 9, 146, 163, 180, 193, 195	lidlmcld 21486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑜(._r‘𝑅)𝑞)(._r‘𝑅)(𝑎(._r‘𝑅)𝑏)) ∈ 𝑖)
197	192, 196	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)) ∈ 𝑖)
198	162, 181, 190, 197	subgcld 19327	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏))(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏))) ∈ 𝑖)
199	162, 181, 184, 198	subgcld 19327	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (((𝑥(._r‘𝑅)𝑦)(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)𝑦))(+_g‘𝑅)((𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏))(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)))) ∈ 𝑖)
200	178, 199	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
201	200	r19.29an 3167	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
202	153, 201	sylbida 604	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
203	202	an32s 665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
204	203	r19.29an 3167	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+_g‘𝑅)𝑛)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
205	111	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
206	9, 14	lidlss 21470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
207	205, 206	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
208	207	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
209		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
210	209	elin2d 4151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
211	210	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) → 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
212	9, 162, 58	lsmelvalx 19834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵) → (𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ↔ ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+_g‘𝑅)𝑛)))
213	212	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵) ∧ 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) → ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+_g‘𝑅)𝑛))
214	186, 165, 208, 211, 213	syl31anc 1400	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) → ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+_g‘𝑅)𝑛))
215	204, 214	r19.29a 3171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
216	215	r19.29an 3167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(._r‘𝑅)𝑎)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
217	148, 216	sylbida 604	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
218	217	an32s 665	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
219	218	r19.29an 3167	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+_g‘𝑅)𝑚)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
220	55	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
221	9, 14	lidlss 21470	. . . . . . . . . . . . . . . . . . 19 ⊢ (((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵)
222	220, 221	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵)
223		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
224	223	elin2d 4151	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
225	9, 162, 58	lsmelvalx 19834	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵) → (𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ↔ ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+_g‘𝑅)𝑚)))
226	225	biimpa 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵) ∧ 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) → ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+_g‘𝑅)𝑚))
227	185, 164, 222, 224, 226	syl31anc 1400	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+_g‘𝑅)𝑚))
228	219, 227	r19.29a 3171	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
229	34, 146	mgpplusg 20344	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝑅) = (+_g‘𝑀)
230	33	ad9antr 755	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑆 ∈ (SubMnd‘𝑀))
231	223	elin1d 4150	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ 𝑆)
232	209	elin1d 4150	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ 𝑆)
233	229, 230, 231, 232	submcld 18988	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑆)
234	228, 233	elind 4146	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(._r‘𝑅)𝑓) ∈ (𝑖 ∩ 𝑆))
235	234	ne0d 4288	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑖 ∩ 𝑆) ≠ ∅)
236	141, 235	exlimddv 1968	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → (𝑖 ∩ 𝑆) ≠ ∅)
237	107, 236	exlimddv 1968	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖 ∩ 𝑆) ≠ ∅)
238	237	anasss 472	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
239	46, 238	sylan2b 606	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
240	239	neneqd 2961	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → ¬ (𝑖 ∩ 𝑆) = ∅)
241	45, 240	condan 830	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖))
242	241	ex 418	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → ((𝑎(._r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
243	242	anasss 472	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(._r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
244	243	ralrimivva 3206	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(._r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
245	9, 146	isprmidlc 21608	. . . . . 6 ⊢ (𝑅 ∈ CRing → (𝑖 ∈ (PrmIdeal‘𝑅) ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(._r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))))
246	245	biimpar 483	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(._r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))) → 𝑖 ∈ (PrmIdeal‘𝑅))
247	2, 7, 44, 244, 246	syl13anc 1399	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (PrmIdeal‘𝑅))
248	247	anasss 472	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → 𝑖 ∈ (PrmIdeal‘𝑅))
249		simprr 785	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
250	248, 249	jca 521	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))
251		ssdifidlprm.3	. . 3 ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
252	34, 9	mgpbas 20345	. . . . 5 ⊢ 𝐵 = (Base‘𝑀)
253	252	submss 18984	. . . 4 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
254	33, 253	syl 18	. . 3 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
255		ssdifidlprm.6	. . 3 ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)
256	9, 8, 251, 254, 255, 3	ssdifidl 21621	. 2 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
257	250, 256	reximddv 3179	1 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 ⊊ wpss 3900 ∅c0 4279 {csn 4584 ‘cfv 6531 (class class class)co 7412 Basecbs 17367 +_gcplusg 17408 ._rcmulr 17409 SubMndcsubmnd 18957 SubGrpcsubg 19310 LSSumclsm 19828 mulGrpcmgp 20340 1_rcur 20387 Ringcrg 20439 CRingccrg 20440 LIdealclidl 21464 RSpancrsp 21465 PrmIdealcprmidl 21596

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-ac2 10522 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-rpss 7728 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-oadd 8464 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-dju 9963 df-card 10001 df-ac 10176 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-sets 17322 df-slot 17340 df-ndx 17352 df-base 17368 df-ress 17389 df-plusg 17421 df-mulr 17422 df-sca 17424 df-vsca 17425 df-ip 17426 df-0g 17592 df-mgm 18796 df-sgrp 18888 df-mnd 18904 df-submnd 18959 df-grp 19127 df-minusg 19128 df-sbg 19129 df-subg 19313 df-cntz 19511 df-lsm 19830 df-cmn 19976 df-abl 19977 df-mgp 20341 df-rng 20355 df-ur 20388 df-ring 20441 df-cring 20442 df-subrg 20802 df-lmod 21117 df-lss 21187 df-lsp 21227 df-sra 21428 df-rgmod 21429 df-lidl 21466 df-rsp 21467 df-prmidl 21597

This theorem is used by: 1arithufdlem4 34061

W3C validator