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 21647

Description: If the set 𝑆 of ssdifidl 21646 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 4007	. . . . . . 7 ⊢ 𝑃 ⊆ (LIdeal‘𝑅)
5		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ 𝑃)
6	4, 5	sselid 3906	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (LIdeal‘𝑅))
7	6	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (LIdeal‘𝑅))
8	1	crngringd 20478	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
9		ssdifidlprm.1	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
10		eqid 2760	. . . . . . . . . 10 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
11	9, 10	ringidcl 20499	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝐵)
12	8, 11	syl 18	. . . . . . . 8 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝐵)
13	12	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1_r‘𝑅) ∈ 𝐵)
14		eqid 2760	. . . . . . . . . . . 12 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
15	9, 14	lidlss 21495	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵)
16	6, 15	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ⊆ 𝐵)
17	16	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ 𝐵)
18		incom 4106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ 𝑝) = (𝑝 ∩ 𝑆)
19	18	eqeq1i 2765	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑝 ∩ 𝑆) = ∅)
20		ineq1 4110	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑖 → (𝑝 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	eqeq1d 2762	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑖 → ((𝑝 ∩ 𝑆) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
22	19, 21	bitrid 286	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
23		sseq2 3934	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑖))
24	22, 23	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑖 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
25	24, 3	elrab2 3648	. . . . . . . . . . . . 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 4405	. . . . . . . . . 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 20414	. . . . . . . . . . . 12 ⊢ (1_r‘𝑅) = (0_g‘𝑀)
36	35	subm0cl 19011	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → (1_r‘𝑅) ∈ 𝑆)
37	33, 36	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝑆)
38	37	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1_r‘𝑅) ∈ 𝑆)
39		elndif 4069	. . . . . . . . 9 ⊢ ((1_r‘𝑅) ∈ 𝑆 → ¬ (1_r‘𝑅) ∈ (𝐵 ∖ 𝑆))
40	38, 39	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1_r‘𝑅) ∈ (𝐵 ∖ 𝑆))
41	32, 40	ssneldd 3911	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1_r‘𝑅) ∈ 𝑖)
42		nelne1 3052	. . . . . . 7 ⊢ (((1_r‘𝑅) ∈ 𝐵 ∧ ¬ (1_r‘𝑅) ∈ 𝑖) → 𝐵 ≠ 𝑖)
43	13, 41, 42	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝐵 ≠ 𝑖)
44	43	necomd 3010	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ≠ 𝐵)
45	29	ad4antr 745	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) = ∅)
46		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖) ↔ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖))
47	14	lidlsubg 21507	. . . . . . . . . . . . . . . . . . 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 4743	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑎} ⊆ 𝐵)
53		eqid 2760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (RSpan‘𝑅) = (RSpan‘𝑅)
54	53, 9, 14	rspcl 21523	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ {𝑎} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
55	50, 52, 54	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
56	14	lidlsubg 21507	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
57	50, 55, 56	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
58		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (LSSum‘𝑅) = (LSSum‘𝑅)
59	58	lsmub1 19876	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
60	49, 57, 59	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
61	58	lsmub2 19877	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
62	49, 57, 61	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
63	9, 53	rspsnid 21532	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
64	50, 51, 63	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
65	62, 64	sseldd 3909	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
66		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑎 ∈ 𝑖)
67	60, 65, 66	ssnelpssd 4043	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
68	7	ad5antr 747	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
69	9, 58, 53, 50, 68, 55	lsmidl 21543	. . . . . . . . . . . . . . . 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 3918	. . . . . . . . . . . . . . . 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 3077	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗))
77		con2b 362	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ (𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
78	77	albii 1851	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
79	76, 78	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
80	75, 79	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
81		ineq2 4111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 = 𝑗 → (𝑆 ∩ 𝑝) = (𝑆 ∩ 𝑗))
82	81	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅))
83		sseq2 3934	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑗))
84	82, 83	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑗 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
85	84, 3	elrab2 3648	. . . . . . . . . . . . . . . . . . . . . . 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 1843	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
93		ovex 7453	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ V
94		psseq2 4018	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
95		eleq1 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅)))
96		sseq2 3934	. . . . . . . . . . . . . . . . . . . 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 4111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
100	99	eqeq1d 2762	. . . . . . . . . . . . . . . . . . 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 3559	. . . . . . . . . . . . . . . 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 4298	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅ ↔ ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
107	105, 106	sylib 221	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
108		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ 𝐵)
109	108	snssd 4743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑏} ⊆ 𝐵)
110	53, 9, 14	rspcl 21523	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ {𝑏} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
111	50, 109, 110	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
112	14	lidlsubg 21507	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
113	50, 111, 112	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
114	58	lsmub1 19876	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
115	49, 113, 114	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
116	58	lsmub2 19877	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
117	49, 113, 116	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
118	9, 53	rspsnid 21532	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
119	50, 108, 118	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
120	117, 119	sseldd 3909	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
121		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑏 ∈ 𝑖)
122	115, 120, 121	ssnelpssd 4043	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
123	9, 58, 53, 50, 68, 111	lsmidl 21543	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅))
124	72, 115	sstrd 3918	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
125	123, 124	jca 521	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
126		ovex 7453	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ V
127		psseq2 4018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
128		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅)))
129		sseq2 3934	. . . . . . . . . . . . . . . . . . . . . 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 4111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
133	132	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . 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 3559	. . . . . . . . . . . . . . . . . 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 4298	. . . . . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._r‘𝑅) = (._r‘𝑅)
147	9, 146, 53	elrspsn 21530	. . . . . . . . . . . . . . . . . . . . 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 21530	. . . . . . . . . . . . . . . . . . . . . . . . . 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 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑦(+_g‘𝑅)𝑛) = (𝑦(+_g‘𝑅)(𝑞(._r‘𝑅)𝑏)))
161	158, 160	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑥(+_g‘𝑅)𝑚)(._r‘𝑅)(𝑦(+_g‘𝑅)𝑛)) = ((𝑥(+_g‘𝑅)(𝑜(._r‘𝑅)𝑎))(._r‘𝑅)(𝑦(+_g‘𝑅)(𝑞(._r‘𝑅)𝑏))))
162		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 20489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 20489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑞(._r‘𝑅)𝑏) ∈ 𝐵)
177	9, 162, 146, 163, 168, 171, 173, 176	ringdi22 20498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 21511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑥(._r‘𝑅)𝑦) ∈ 𝑖)
183	14, 9, 146, 163, 180, 171, 172	lidlmcld 21511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)𝑦) ∈ 𝑖)
184	162, 181, 182, 183	subgcld 19352	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 20487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)) = ((𝑞(._r‘𝑅)𝑏)(._r‘𝑅)𝑥))
189	14, 9, 146, 163, 180, 176, 167	lidlmcld 21511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑞(._r‘𝑅)𝑏)(._r‘𝑅)𝑥) ∈ 𝑖)
190	188, 189	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)) ∈ 𝑖)
191	9, 146	cringm4 21632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 20489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 21511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑜(._r‘𝑅)𝑞)(._r‘𝑅)(𝑎(._r‘𝑅)𝑏)) ∈ 𝑖)
197	192, 196	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏)) ∈ 𝑖)
198	162, 181, 190, 197	subgcld 19352	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → ((𝑥(._r‘𝑅)(𝑞(._r‘𝑅)𝑏))(+_g‘𝑅)((𝑜(._r‘𝑅)𝑎)(._r‘𝑅)(𝑞(._r‘𝑅)𝑏))) ∈ 𝑖)
199	162, 181, 184, 198	subgcld 19352	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2860	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+_g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(._r‘𝑅)𝑏)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
201	200	r19.29an 3166	. . . . . . . . . . . . . . . . . . . . . . . . 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 3166	. . . . . . . . . . . . . . . . . . . . . 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 21495	. . . . . . . . . . . . . . . . . . . . . . . . 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 4102	. . . . . . . . . . . . . . . . . . . . . . . 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 19859	. . . . . . . . . . . . . . . . . . . . . . . 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 3170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+_g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(._r‘𝑅)𝑎)) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
216	215	r19.29an 3166	. . . . . . . . . . . . . . . . . . . 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 3166	. . . . . . . . . . . . . . . . 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 21495	. . . . . . . . . . . . . . . . . . 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 4102	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
225	9, 162, 58	lsmelvalx 19859	. . . . . . . . . . . . . . . . . . 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 3170	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑖)
229	34, 146	mgpplusg 20369	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝑅) = (+_g‘𝑀)
230	33	ad9antr 755	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑆 ∈ (SubMnd‘𝑀))
231	223	elin1d 4101	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ 𝑆)
232	209	elin1d 4101	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ 𝑆)
233	229, 230, 231, 232	submcld 19013	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(._r‘𝑅)𝑓) ∈ 𝑆)
234	228, 233	elind 4097	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(._r‘𝑅)𝑓) ∈ (𝑖 ∩ 𝑆))
235	234	ne0d 4287	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑖 ∩ 𝑆) ≠ ∅)
236	141, 235	exlimddv 1967	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → (𝑖 ∩ 𝑆) ≠ ∅)
237	107, 236	exlimddv 1967	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖 ∩ 𝑆) ≠ ∅)
238	237	anasss 472	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
239	46, 238	sylan2b 606	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
240	239	neneqd 2960	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → ¬ (𝑖 ∩ 𝑆) = ∅)
241	45, 240	condan 830	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(._r‘𝑅)𝑏) ∈ 𝑖) → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖))
242	241	ex 418	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → ((𝑎(._r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
243	242	anasss 472	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(._r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
244	243	ralrimivva 3205	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(._r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
245	9, 146	isprmidlc 21633	. . . . . 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 20370	. . . . 5 ⊢ 𝐵 = (Base‘𝑀)
253	252	submss 19009	. . . 4 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
254	33, 253	syl 18	. . 3 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
255		ssdifidlprm.6	. . 3 ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)
256	9, 8, 251, 254, 255, 3	ssdifidl 21646	. 2 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
257	250, 256	reximddv 3178	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 1567 = wceq 1569 ∃wex 1811 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 ⊆ wss 3895 ⊊ wpss 4013 ∖ cdif 4045 ∩ cin 4089 ∅c0 4278 {csn 4584 ‘cfv 6538 (class class class)co 7420 Basecbs 17392 +_gcplusg 17433 ._rcmulr 17434 SubMndcsubmnd 18982 SubGrpcsubg 19335 LSSumclsm 19853 mulGrpcmgp 20365 1_rcur 20412 Ringcrg 20464 CRingccrg 20465 LIdealclidl 21489 RSpancrsp 21490 PrmIdealcprmidl 21621

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-ac2 10544 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-rpss 7739 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-oadd 8483 df-er 8720 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-dju 9985 df-card 10023 df-ac 10198 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-5 12411 df-6 12412 df-7 12413 df-8 12414 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-ress 17414 df-plusg 17446 df-mulr 17447 df-sca 17449 df-vsca 17450 df-ip 17451 df-0g 17617 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-submnd 18984 df-grp 19152 df-minusg 19153 df-sbg 19154 df-subg 19338 df-cntz 19536 df-lsm 19855 df-cmn 20001 df-abl 20002 df-mgp 20366 df-rng 20380 df-ur 20413 df-ring 20466 df-cring 20467 df-subrg 20827 df-lmod 21142 df-lss 21212 df-lsp 21252 df-sra 21453 df-rgmod 21454 df-lidl 21491 df-rsp 21492 df-prmidl 21622

This theorem is used by: 1arithufdlem4 34125

W3C validator