Theorem ssdifidlprm 33478

Description: If the set 𝑆 of ssdifidl 33477 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 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑅 ∈ CRing)
3		ssdifidlprm.7	. . . . . . . 8 ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}
4	3	ssrab3 4062	. . . . . . 7 ⊢ 𝑃 ⊆ (LIdeal‘𝑅)
5		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ 𝑃)
6	4, 5	sselid 3961	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (LIdeal‘𝑅))
7	6	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (LIdeal‘𝑅))
8	1	crngringd 20211	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
9		ssdifidlprm.1	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
10		eqid 2736	. . . . . . . . . 10 ⊢ (1r‘𝑅) = (1r‘𝑅)
11	9, 10	ringidcl 20230	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵)
12	8, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵)
13	12	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1r‘𝑅) ∈ 𝐵)
14		eqid 2736	. . . . . . . . . . . 12 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
15	9, 14	lidlss 21178	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵)
16	6, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ⊆ 𝐵)
17	16	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ 𝐵)
18		incom 4189	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ 𝑝) = (𝑝 ∩ 𝑆)
19	18	eqeq1i 2741	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑝 ∩ 𝑆) = ∅)
20		ineq1 4193	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑖 → (𝑝 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑖 → ((𝑝 ∩ 𝑆) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
22	19, 21	bitrid 283	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
23		sseq2 3990	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑖))
24	22, 23	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑖 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
25	24, 3	elrab2 3679	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝑃 ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
26	25	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑃 → (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
27	26	simprd 495	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝑃 → ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖))
28	27	simpld 494	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑃 → (𝑖 ∩ 𝑆) = ∅)
29	28	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (𝑖 ∩ 𝑆) = ∅)
30		reldisj 4433	. . . . . . . . . 10 ⊢ (𝑖 ⊆ 𝐵 → ((𝑖 ∩ 𝑆) = ∅ ↔ 𝑖 ⊆ (𝐵 ∖ 𝑆)))
31	30	biimpa 476	. . . . . . . . 9 ⊢ ((𝑖 ⊆ 𝐵 ∧ (𝑖 ∩ 𝑆) = ∅) → 𝑖 ⊆ (𝐵 ∖ 𝑆))
32	17, 29, 31	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ (𝐵 ∖ 𝑆))
33		ssdifidlprm.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))
34		ssdifidlprm.5	. . . . . . . . . . . . 13 ⊢ 𝑀 = (mulGrp‘𝑅)
35	34, 10	ringidval 20148	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (0g‘𝑀)
36	35	subm0cl 18794	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → (1r‘𝑅) ∈ 𝑆)
37	33, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆)
38	37	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1r‘𝑅) ∈ 𝑆)
39		elndif 4113	. . . . . . . . 9 ⊢ ((1r‘𝑅) ∈ 𝑆 → ¬ (1r‘𝑅) ∈ (𝐵 ∖ 𝑆))
40	38, 39	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1r‘𝑅) ∈ (𝐵 ∖ 𝑆))
41	32, 40	ssneldd 3966	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1r‘𝑅) ∈ 𝑖)
42		nelne1 3030	. . . . . . 7 ⊢ (((1r‘𝑅) ∈ 𝐵 ∧ ¬ (1r‘𝑅) ∈ 𝑖) → 𝐵 ≠ 𝑖)
43	13, 41, 42	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝐵 ≠ 𝑖)
44	43	necomd 2988	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ≠ 𝐵)
45	29	ad4antr 732	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) = ∅)
46		ioran 985	. . . . . . . . . . 11 ⊢ (¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖) ↔ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖))
47	14	lidlsubg 21189	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) → 𝑖 ∈ (SubGrp‘𝑅))
48	8, 6, 47	syl2an2r 685	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (SubGrp‘𝑅))
49	48	ad6antr 736	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (SubGrp‘𝑅))
50	8	ad7antr 738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑅 ∈ Ring)
51		simp-5r 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ 𝐵)
52	51	snssd 4790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑎} ⊆ 𝐵)
53		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (RSpan‘𝑅) = (RSpan‘𝑅)
54	53, 9, 14	rspcl 21201	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ {𝑎} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
55	50, 52, 54	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
56	14	lidlsubg 21189	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
57	50, 55, 56	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
58		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (LSSum‘𝑅) = (LSSum‘𝑅)
59	58	lsmub1 19643	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
60	49, 57, 59	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
61	58	lsmub2 19644	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
62	49, 57, 61	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
63	9, 53	rspsnid 33391	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
64	50, 51, 63	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
65	62, 64	sseldd 3964	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
66		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑎 ∈ 𝑖)
67	60, 65, 66	ssnelpssd 4095	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
68	7	ad5antr 734	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
69	9, 58, 53, 50, 68, 55	lsmidl 33421	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅))
70	27	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑃 → 𝐼 ⊆ 𝑖)
71	70	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝐼 ⊆ 𝑖)
72	71	ad6antr 736	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ 𝑖)
73	72, 60	sstrd 3974	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
74	69, 73	jca 511	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
75		simp-6r 787	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
76		df-ral 3053	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗))
77		con2b 359	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ (𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
78	77	albii 1819	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
79	76, 78	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
80	75, 79	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
81		ineq2 4194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 = 𝑗 → (𝑆 ∩ 𝑝) = (𝑆 ∩ 𝑗))
82	81	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅))
83		sseq2 3990	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑗))
84	82, 83	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑗 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
85	84, 3	elrab2 3679	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ 𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
86	85	baib 535	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (LIdeal‘𝑅) → (𝑗 ∈ 𝑃 ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
87	86	rbaibd 540	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → (𝑗 ∈ 𝑃 ↔ (𝑆 ∩ 𝑗) = ∅))
88	87	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → (¬ 𝑗 ∈ 𝑃 ↔ ¬ (𝑆 ∩ 𝑗) = ∅))
89	88	biimpcd 249	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑗 ∈ 𝑃 → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → ¬ (𝑆 ∩ 𝑗) = ∅))
90	89	imim2i 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → (𝑖 ⊊ 𝑗 → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → ¬ (𝑆 ∩ 𝑗) = ∅)))
91	90	impd 410	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
92	91	alimi 1811	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
93		ovex 7443	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ V
94		psseq2 4071	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
95		eleq1 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅)))
96		sseq2 3990	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
97	95, 96	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) ↔ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))))
98	94, 97	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) ↔ (𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))))
99		ineq2 4194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
100	99	eqeq1d 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑆 ∩ 𝑗) = ∅ ↔ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
101	100	notbid 318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (¬ (𝑆 ∩ 𝑗) = ∅ ↔ ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
102	98, 101	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) ↔ ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅)))
103	93, 102	spcv 3589	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) → ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
104	80, 92, 103	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
105	67, 74, 104	mp2and 699	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅)
106		neq0 4332	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅ ↔ ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
107	105, 106	sylib 218	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
108		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ 𝐵)
109	108	snssd 4790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑏} ⊆ 𝐵)
110	53, 9, 14	rspcl 21201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ {𝑏} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
111	50, 109, 110	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
112	14	lidlsubg 21189	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
113	50, 111, 112	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
114	58	lsmub1 19643	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
115	49, 113, 114	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
116	58	lsmub2 19644	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
117	49, 113, 116	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
118	9, 53	rspsnid 33391	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
119	50, 108, 118	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
120	117, 119	sseldd 3964	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
121		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑏 ∈ 𝑖)
122	115, 120, 121	ssnelpssd 4095	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
123	9, 58, 53, 50, 68, 111	lsmidl 33421	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅))
124	72, 115	sstrd 3974	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
125	123, 124	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
126		ovex 7443	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ V
127		psseq2 4071	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
128		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅)))
129		sseq2 3990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
130	128, 129	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) ↔ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))))
131	127, 130	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) ↔ (𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))))
132		ineq2 4194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
133	132	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑆 ∩ 𝑗) = ∅ ↔ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
134	133	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (¬ (𝑆 ∩ 𝑗) = ∅ ↔ ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
135	131, 134	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) ↔ ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅)))
136	126, 135	spcv 3589	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) → ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
137	80, 92, 136	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
138	122, 125, 137	mp2and 699	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅)
139		neq0 4332	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅ ↔ ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
140	138, 139	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
141	140	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
142	50	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑅 ∈ Ring)
143	142	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → 𝑅 ∈ Ring)
144	51	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑎 ∈ 𝐵)
145	144	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → 𝑎 ∈ 𝐵)
146		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (.r‘𝑅) = (.r‘𝑅)
147	9, 146, 53	elrspsn 21206	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → (𝑚 ∈ ((RSpan‘𝑅)‘{𝑎}) ↔ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)))
148	143, 145, 147	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑚 ∈ ((RSpan‘𝑅)‘{𝑎}) ↔ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)))
149	142	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → 𝑅 ∈ Ring)
150	108	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑏 ∈ 𝐵)
151	150	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → 𝑏 ∈ 𝐵)
152	9, 146, 53	elrspsn 21206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → (𝑛 ∈ ((RSpan‘𝑅)‘{𝑏}) ↔ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)))
153	149, 151, 152	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑛 ∈ ((RSpan‘𝑅)‘{𝑏}) ↔ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)))
154		simp-7r 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑒 = (𝑥(+g‘𝑅)𝑚))
155		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑓 = (𝑦(+g‘𝑅)𝑛))
156	154, 155	oveq12d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) = ((𝑥(+g‘𝑅)𝑚)(.r‘𝑅)(𝑦(+g‘𝑅)𝑛)))
157		simp-5r 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑚 = (𝑜(.r‘𝑅)𝑎))
158	157	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(+g‘𝑅)𝑚) = (𝑥(+g‘𝑅)(𝑜(.r‘𝑅)𝑎)))
159		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑛 = (𝑞(.r‘𝑅)𝑏))
160	159	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑦(+g‘𝑅)𝑛) = (𝑦(+g‘𝑅)(𝑞(.r‘𝑅)𝑏)))
161	158, 160	oveq12d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(+g‘𝑅)𝑚)(.r‘𝑅)(𝑦(+g‘𝑅)𝑛)) = ((𝑥(+g‘𝑅)(𝑜(.r‘𝑅)𝑎))(.r‘𝑅)(𝑦(+g‘𝑅)(𝑞(.r‘𝑅)𝑏))))
162		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (+g‘𝑅) = (+g‘𝑅)
163	149	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑅 ∈ Ring)
164	17	ad7antr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑖 ⊆ 𝐵)
165	164	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑖 ⊆ 𝐵)
166	165	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ⊆ 𝐵)
167		simp-8r 791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑥 ∈ 𝑖)
168	166, 167	sseldd 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑥 ∈ 𝐵)
169		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑜 ∈ 𝐵)
170	144	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑎 ∈ 𝐵)
171	9, 146, 163, 169, 170	ringcld 20225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑜(.r‘𝑅)𝑎) ∈ 𝐵)
172		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑦 ∈ 𝑖)
173	166, 172	sseldd 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑦 ∈ 𝐵)
174		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑞 ∈ 𝐵)
175	151	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑏 ∈ 𝐵)
176	9, 146, 163, 174, 175	ringcld 20225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑞(.r‘𝑅)𝑏) ∈ 𝐵)
177	9, 162, 146, 163, 168, 171, 173, 176	ringdi22 33231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑖 ∈ (LIdeal‘𝑅))
180	179	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ∈ (LIdeal‘𝑅))
181	163, 180, 47	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ∈ (SubGrp‘𝑅))
182	14, 9, 146, 163, 180, 168, 172	lidlmcld 33439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑖)
183	14, 9, 146, 163, 180, 171, 172	lidlmcld 33439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦) ∈ 𝑖)
184	162, 181, 182, 183	subgcld 33041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦)) ∈ 𝑖)
185	2	ad7antr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑅 ∈ CRing)
186	185	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑅 ∈ CRing)
187	186	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑅 ∈ CRing)
188	9, 146, 187, 168, 176	crngcomd 20220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑞(.r‘𝑅)𝑏)(.r‘𝑅)𝑥))
189	14, 9, 146, 163, 180, 176, 167	lidlmcld 33439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑞(.r‘𝑅)𝑏)(.r‘𝑅)𝑥) ∈ 𝑖)
190	188, 189	eqeltrd 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) ∈ 𝑖)
191	9, 146	cringm4 33466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ CRing ∧ (𝑜 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑞 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)))
192	187, 169, 170, 174, 175, 191	syl122anc 1381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)))
193	9, 146, 163, 169, 174	ringcld 20225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑜(.r‘𝑅)𝑞) ∈ 𝐵)
194		simp-5r 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑎(.r‘𝑅)𝑏) ∈ 𝑖)
195	194	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑎(.r‘𝑅)𝑏) ∈ 𝑖)
196	14, 9, 146, 163, 180, 193, 195	lidlmcld 33439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)) ∈ 𝑖)
197	192, 196	eqeltrd 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) ∈ 𝑖)
198	162, 181, 190, 197	subgcld 33041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))) ∈ 𝑖)
199	162, 181, 184, 198	subgcld 33041	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
201	200	r19.29an 3145	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
202	153, 201	sylbida 592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
203	202	an32s 652	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
204	203	r19.29an 3145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
205	111	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
206	9, 14	lidlss 21178	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
207	205, 206	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
208	207	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
209		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
210	209	elin2d 4185	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
211	210	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
212	9, 162, 58	lsmelvalx 19626	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵) → (𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ↔ ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛)))
213	212	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵) ∧ 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) → ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛))
214	186, 165, 208, 211, 213	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛))
215	204, 214	r19.29a 3149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
216	215	r19.29an 3145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
217	148, 216	sylbida 592	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
218	217	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
219	218	r19.29an 3145	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
220	55	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
221	9, 14	lidlss 21178	. . . . . . . . . . . . . . . . . . 19 ⊢ (((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵)
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵)
223		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
224	223	elin2d 4185	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
225	9, 162, 58	lsmelvalx 19626	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵) → (𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ↔ ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚)))
226	225	biimpa 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵) ∧ 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) → ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚))
227	185, 164, 222, 224, 226	syl31anc 1375	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚))
228	219, 227	r19.29a 3149	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
229	34, 146	mgpplusg 20109	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘𝑅) = (+g‘𝑀)
230	33	ad9antr 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑆 ∈ (SubMnd‘𝑀))
231	223	elin1d 4184	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ 𝑆)
232	209	elin1d 4184	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ 𝑆)
233	229, 230, 231, 232	submcld 33035	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑆)
234	228, 233	elind 4180	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ (𝑖 ∩ 𝑆))
235	234	ne0d 4322	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑖 ∩ 𝑆) ≠ ∅)
236	141, 235	exlimddv 1935	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → (𝑖 ∩ 𝑆) ≠ ∅)
237	107, 236	exlimddv 1935	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖 ∩ 𝑆) ≠ ∅)
238	237	anasss 466	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
239	46, 238	sylan2b 594	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
240	239	neneqd 2938	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → ¬ (𝑖 ∩ 𝑆) = ∅)
241	45, 240	condan 817	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖))
242	241	ex 412	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
243	242	anasss 466	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
244	243	ralrimivva 3188	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
245	9, 146	isprmidlc 33467	. . . . . 6 ⊢ (𝑅 ∈ CRing → (𝑖 ∈ (PrmIdeal‘𝑅) ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))))
246	245	biimpar 477	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))) → 𝑖 ∈ (PrmIdeal‘𝑅))
247	2, 7, 44, 244, 246	syl13anc 1374	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (PrmIdeal‘𝑅))
248	247	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → 𝑖 ∈ (PrmIdeal‘𝑅))
249		simprr 772	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
250	248, 249	jca 511	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))
251		ssdifidlprm.3	. . 3 ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
252	34, 9	mgpbas 20110	. . . . 5 ⊢ 𝐵 = (Base‘𝑀)
253	252	submss 18792	. . . 4 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
254	33, 253	syl 17	. . 3 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
255		ssdifidlprm.6	. . 3 ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)
256	9, 8, 251, 254, 255, 3	ssdifidl 33477	. 2 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
257	250, 256	reximddv 3157	1 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3420   ∖ cdif 3928   ∩ cin 3930   ⊆ wss 3931   ⊊ wpss 3932  ∅c0 4313  {csn 4606  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  +_gcplusg 17276  ._rcmulr 17277  SubMndcsubmnd 18765  SubGrpcsubg 19108  LSSumclsm 19620  mulGrpcmgp 20105  1_rcur 20146  Ringcrg 20198  CRingccrg 20199  LIdealclidl 21172  RSpancrsp 21173  PrmIdealcprmidl 33455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-ac2 10482  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-rpss 7722  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-oadd 8489  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-dju 9920  df-card 9958  df-ac 10135  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-sets 17188  df-slot 17206  df-ndx 17218  df-base 17234  df-ress 17257  df-plusg 17289  df-mulr 17290  df-sca 17292  df-vsca 17293  df-ip 17294  df-0g 17460  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-submnd 18767  df-grp 18924  df-minusg 18925  df-sbg 18926  df-subg 19111  df-cntz 19305  df-lsm 19622  df-cmn 19768  df-abl 19769  df-mgp 20106  df-rng 20118  df-ur 20147  df-ring 20200  df-cring 20201  df-subrg 20535  df-lmod 20824  df-lss 20894  df-lsp 20934  df-sra 21136  df-rgmod 21137  df-lidl 21174  df-rsp 21175  df-prmidl 33456

This theorem is referenced by:  1arithufdlem4  33567