Theorem ssdifidlprm 33270

Description: If the set 𝑆 of ssdifidl 33269 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 724	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑅 ∈ CRing)
3		ssdifidlprm.7	. . . . . . . 8 ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}
4	3	ssrab3 4076	. . . . . . 7 ⊢ 𝑃 ⊆ (LIdeal‘𝑅)
5		simpr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ 𝑃)
6	4, 5	sselid 3974	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (LIdeal‘𝑅))
7	6	adantr 479	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (LIdeal‘𝑅))
8	1	crngringd 20198	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
9		ssdifidlprm.1	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
10		eqid 2725	. . . . . . . . . 10 ⊢ (1r‘𝑅) = (1r‘𝑅)
11	9, 10	ringidcl 20214	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵)
12	8, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵)
13	12	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1r‘𝑅) ∈ 𝐵)
14		eqid 2725	. . . . . . . . . . . 12 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
15	9, 14	lidlss 21120	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵)
16	6, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ⊆ 𝐵)
17	16	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ 𝐵)
18		incom 4199	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ 𝑝) = (𝑝 ∩ 𝑆)
19	18	eqeq1i 2730	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑝 ∩ 𝑆) = ∅)
20		ineq1 4203	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑖 → (𝑝 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	eqeq1d 2727	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑖 → ((𝑝 ∩ 𝑆) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
22	19, 21	bitrid 282	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
23		sseq2 4003	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑖))
24	22, 23	anbi12d 630	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑖 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
25	24, 3	elrab2 3682	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝑃 ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
26	25	biimpi 215	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑃 → (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
27	26	simprd 494	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝑃 → ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖))
28	27	simpld 493	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑃 → (𝑖 ∩ 𝑆) = ∅)
29	28	ad2antlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (𝑖 ∩ 𝑆) = ∅)
30		reldisj 4453	. . . . . . . . . 10 ⊢ (𝑖 ⊆ 𝐵 → ((𝑖 ∩ 𝑆) = ∅ ↔ 𝑖 ⊆ (𝐵 ∖ 𝑆)))
31	30	biimpa 475	. . . . . . . . 9 ⊢ ((𝑖 ⊆ 𝐵 ∧ (𝑖 ∩ 𝑆) = ∅) → 𝑖 ⊆ (𝐵 ∖ 𝑆))
32	17, 29, 31	syl2anc 582	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ (𝐵 ∖ 𝑆))
33		ssdifidlprm.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))
34		ssdifidlprm.5	. . . . . . . . . . . . 13 ⊢ 𝑀 = (mulGrp‘𝑅)
35	34, 10	ringidval 20135	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (0g‘𝑀)
36	35	subm0cl 18771	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → (1r‘𝑅) ∈ 𝑆)
37	33, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆)
38	37	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1r‘𝑅) ∈ 𝑆)
39		elndif 4125	. . . . . . . . 9 ⊢ ((1r‘𝑅) ∈ 𝑆 → ¬ (1r‘𝑅) ∈ (𝐵 ∖ 𝑆))
40	38, 39	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1r‘𝑅) ∈ (𝐵 ∖ 𝑆))
41	32, 40	ssneldd 3979	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1r‘𝑅) ∈ 𝑖)
42		nelne1 3028	. . . . . . 7 ⊢ (((1r‘𝑅) ∈ 𝐵 ∧ ¬ (1r‘𝑅) ∈ 𝑖) → 𝐵 ≠ 𝑖)
43	13, 41, 42	syl2anc 582	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝐵 ≠ 𝑖)
44	43	necomd 2985	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ≠ 𝐵)
45	29	ad4antr 730	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) = ∅)
46		ioran 981	. . . . . . . . . . 11 ⊢ (¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖) ↔ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖))
47	14	lidlsubg 21131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) → 𝑖 ∈ (SubGrp‘𝑅))
48	8, 6, 47	syl2an2r 683	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (SubGrp‘𝑅))
49	48	ad6antr 734	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (SubGrp‘𝑅))
50	8	ad7antr 736	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑅 ∈ Ring)
51		simp-5r 784	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ 𝐵)
52	51	snssd 4814	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑎} ⊆ 𝐵)
53		eqid 2725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (RSpan‘𝑅) = (RSpan‘𝑅)
54	53, 9, 14	rspcl 21143	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ {𝑎} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
55	50, 52, 54	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
56	14	lidlsubg 21131	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
57	50, 55, 56	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
58		eqid 2725	. . . . . . . . . . . . . . . . . 18 ⊢ (LSSum‘𝑅) = (LSSum‘𝑅)
59	58	lsmub1 19624	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
60	49, 57, 59	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
61	58	lsmub2 19625	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
62	49, 57, 61	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
63	9, 53	rspsnid 33183	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
64	50, 51, 63	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
65	62, 64	sseldd 3977	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
66		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑎 ∈ 𝑖)
67	60, 65, 66	ssnelpssd 4108	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
68	7	ad5antr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
69	9, 58, 53, 50, 68, 55	lsmidl 33213	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅))
70	27	simprd 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑃 → 𝐼 ⊆ 𝑖)
71	70	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝐼 ⊆ 𝑖)
72	71	ad6antr 734	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ 𝑖)
73	72, 60	sstrd 3987	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
74	69, 73	jca 510	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
75		simp-6r 786	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
76		df-ral 3051	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗))
77		con2b 358	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ (𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
78	77	albii 1813	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
79	76, 78	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
80	75, 79	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
81		ineq2 4204	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 = 𝑗 → (𝑆 ∩ 𝑝) = (𝑆 ∩ 𝑗))
82	81	eqeq1d 2727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅))
83		sseq2 4003	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑗))
84	82, 83	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑗 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
85	84, 3	elrab2 3682	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ 𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
86	85	baib 534	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (LIdeal‘𝑅) → (𝑗 ∈ 𝑃 ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
87	86	rbaibd 539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → (𝑗 ∈ 𝑃 ↔ (𝑆 ∩ 𝑗) = ∅))
88	87	notbid 317	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → (¬ 𝑗 ∈ 𝑃 ↔ ¬ (𝑆 ∩ 𝑗) = ∅))
89	88	biimpcd 248	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑗 ∈ 𝑃 → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → ¬ (𝑆 ∩ 𝑗) = ∅))
90	89	imim2i 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → (𝑖 ⊊ 𝑗 → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → ¬ (𝑆 ∩ 𝑗) = ∅)))
91	90	impd 409	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
92	91	alimi 1805	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
93		ovex 7452	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ V
94		psseq2 4084	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
95		eleq1 2813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅)))
96		sseq2 4003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
97	95, 96	anbi12d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) ↔ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))))
98	94, 97	anbi12d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) ↔ (𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))))
99		ineq2 4204	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
100	99	eqeq1d 2727	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑆 ∩ 𝑗) = ∅ ↔ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
101	100	notbid 317	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (¬ (𝑆 ∩ 𝑗) = ∅ ↔ ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
102	98, 101	imbi12d 343	. . . . . . . . . . . . . . . . 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 697	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅)
106		neq0 4345	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅ ↔ ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
107	105, 106	sylib 217	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
108		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ 𝐵)
109	108	snssd 4814	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑏} ⊆ 𝐵)
110	53, 9, 14	rspcl 21143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ {𝑏} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
111	50, 109, 110	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
112	14	lidlsubg 21131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
113	50, 111, 112	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
114	58	lsmub1 19624	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
115	49, 113, 114	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
116	58	lsmub2 19625	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
117	49, 113, 116	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
118	9, 53	rspsnid 33183	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
119	50, 108, 118	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
120	117, 119	sseldd 3977	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
121		simpr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑏 ∈ 𝑖)
122	115, 120, 121	ssnelpssd 4108	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
123	9, 58, 53, 50, 68, 111	lsmidl 33213	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅))
124	72, 115	sstrd 3987	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
125	123, 124	jca 510	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
126		ovex 7452	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ V
127		psseq2 4084	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
128		eleq1 2813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅)))
129		sseq2 4003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
130	128, 129	anbi12d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) ↔ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))))
131	127, 130	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) ↔ (𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))))
132		ineq2 4204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
133	132	eqeq1d 2727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑆 ∩ 𝑗) = ∅ ↔ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
134	133	notbid 317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (¬ (𝑆 ∩ 𝑗) = ∅ ↔ ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
135	131, 134	imbi12d 343	. . . . . . . . . . . . . . . . . . 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 697	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅)
139		neq0 4345	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅ ↔ ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
140	138, 139	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
141	140	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
142	50	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑅 ∈ Ring)
143	142	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → 𝑅 ∈ Ring)
144	51	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑎 ∈ 𝐵)
145	144	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → 𝑎 ∈ 𝐵)
146		eqid 2725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (.r‘𝑅) = (.r‘𝑅)
147	9, 146, 53	rspsnel 33182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → (𝑚 ∈ ((RSpan‘𝑅)‘{𝑎}) ↔ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)))
148	143, 145, 147	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑚 ∈ ((RSpan‘𝑅)‘{𝑎}) ↔ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)))
149	142	ad6antr 734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → 𝑅 ∈ Ring)
150	108	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑏 ∈ 𝐵)
151	150	ad6antr 734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → 𝑏 ∈ 𝐵)
152	9, 146, 53	rspsnel 33182	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → (𝑛 ∈ ((RSpan‘𝑅)‘{𝑏}) ↔ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)))
153	149, 151, 152	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑛 ∈ ((RSpan‘𝑅)‘{𝑏}) ↔ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)))
154		simp-7r 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑒 = (𝑥(+g‘𝑅)𝑚))
155		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑓 = (𝑦(+g‘𝑅)𝑛))
156	154, 155	oveq12d 7437	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) = ((𝑥(+g‘𝑅)𝑚)(.r‘𝑅)(𝑦(+g‘𝑅)𝑛)))
157		simp-5r 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑚 = (𝑜(.r‘𝑅)𝑎))
158	157	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(+g‘𝑅)𝑚) = (𝑥(+g‘𝑅)(𝑜(.r‘𝑅)𝑎)))
159		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑛 = (𝑞(.r‘𝑅)𝑏))
160	159	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑦(+g‘𝑅)𝑛) = (𝑦(+g‘𝑅)(𝑞(.r‘𝑅)𝑏)))
161	158, 160	oveq12d 7437	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(+g‘𝑅)𝑚)(.r‘𝑅)(𝑦(+g‘𝑅)𝑛)) = ((𝑥(+g‘𝑅)(𝑜(.r‘𝑅)𝑎))(.r‘𝑅)(𝑦(+g‘𝑅)(𝑞(.r‘𝑅)𝑏))))
162		eqid 2725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (+g‘𝑅) = (+g‘𝑅)
163	149	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑅 ∈ Ring)
164	17	ad7antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑖 ⊆ 𝐵)
165	164	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑖 ⊆ 𝐵)
166	165	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ⊆ 𝐵)
167		simp-8r 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑥 ∈ 𝑖)
168	166, 167	sseldd 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑥 ∈ 𝐵)
169		simp-6r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑜 ∈ 𝐵)
170	144	ad8antr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑎 ∈ 𝐵)
171	9, 146, 163, 169, 170	ringcld 20211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑜(.r‘𝑅)𝑎) ∈ 𝐵)
172		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑦 ∈ 𝑖)
173	166, 172	sseldd 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑦 ∈ 𝐵)
174		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑞 ∈ 𝐵)
175	151	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑏 ∈ 𝐵)
176	9, 146, 163, 174, 175	ringcld 20211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑞(.r‘𝑅)𝑏) ∈ 𝐵)
177	9, 162, 146, 163, 168, 171, 173, 176	ringdi22 33031	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑖 ∈ (LIdeal‘𝑅))
180	179	ad8antr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ∈ (LIdeal‘𝑅))
181	163, 180, 47	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ∈ (SubGrp‘𝑅))
182	14, 9, 146, 163, 180, 168, 172	lidlmcld 33231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑖)
183	14, 9, 146, 163, 180, 171, 172	lidlmcld 33231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦) ∈ 𝑖)
184	162, 181, 182, 183	subgcld 32849	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦)) ∈ 𝑖)
185	2	ad7antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑅 ∈ CRing)
186	185	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑅 ∈ CRing)
187	186	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑅 ∈ CRing)
188	9, 146, 187, 168, 176	crngcomd 20207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑞(.r‘𝑅)𝑏)(.r‘𝑅)𝑥))
189	14, 9, 146, 163, 180, 176, 167	lidlmcld 33231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑞(.r‘𝑅)𝑏)(.r‘𝑅)𝑥) ∈ 𝑖)
190	188, 189	eqeltrd 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) ∈ 𝑖)
191	9, 146	cringm4 33258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ CRing ∧ (𝑜 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑞 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)))
192	187, 169, 170, 174, 175, 191	syl122anc 1376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)))
193	9, 146, 163, 169, 174	ringcld 20211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑜(.r‘𝑅)𝑞) ∈ 𝐵)
194		simp-5r 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑎(.r‘𝑅)𝑏) ∈ 𝑖)
195	194	ad8antr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑎(.r‘𝑅)𝑏) ∈ 𝑖)
196	14, 9, 146, 163, 180, 193, 195	lidlmcld 33231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)) ∈ 𝑖)
197	192, 196	eqeltrd 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) ∈ 𝑖)
198	162, 181, 190, 197	subgcld 32849	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))) ∈ 𝑖)
199	162, 181, 184, 198	subgcld 32849	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2825	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
201	200	r19.29an 3147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
202	153, 201	sylbida 590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
203	202	an32s 650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
204	203	r19.29an 3147	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
205	111	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
206	9, 14	lidlss 21120	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
207	205, 206	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
208	207	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
209		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
210	209	elin2d 4197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
211	210	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
212	9, 162, 58	lsmelvalx 19607	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵) → (𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ↔ ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛)))
213	212	biimpa 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵) ∧ 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) → ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛))
214	186, 165, 208, 211, 213	syl31anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛))
215	204, 214	r19.29a 3151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
216	215	r19.29an 3147	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
217	148, 216	sylbida 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
218	217	an32s 650	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
219	218	r19.29an 3147	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
220	55	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
221	9, 14	lidlss 21120	. . . . . . . . . . . . . . . . . . 19 ⊢ (((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵)
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵)
223		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
224	223	elin2d 4197	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
225	9, 162, 58	lsmelvalx 19607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵) → (𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ↔ ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚)))
226	225	biimpa 475	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵) ∧ 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) → ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚))
227	185, 164, 222, 224, 226	syl31anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚))
228	219, 227	r19.29a 3151	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
229	34, 146	mgpplusg 20090	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘𝑅) = (+g‘𝑀)
230	33	ad9antr 740	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑆 ∈ (SubMnd‘𝑀))
231	223	elin1d 4196	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ 𝑆)
232	209	elin1d 4196	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ 𝑆)
233	229, 230, 231, 232	submcld 32844	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑆)
234	228, 233	elind 4192	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ (𝑖 ∩ 𝑆))
235	234	ne0d 4335	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑖 ∩ 𝑆) ≠ ∅)
236	141, 235	exlimddv 1930	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → (𝑖 ∩ 𝑆) ≠ ∅)
237	107, 236	exlimddv 1930	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖 ∩ 𝑆) ≠ ∅)
238	237	anasss 465	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
239	46, 238	sylan2b 592	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
240	239	neneqd 2934	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → ¬ (𝑖 ∩ 𝑆) = ∅)
241	45, 240	condan 816	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖))
242	241	ex 411	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
243	242	anasss 465	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
244	243	ralrimivva 3190	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
245	9, 146	isprmidlc 33259	. . . . . 6 ⊢ (𝑅 ∈ CRing → (𝑖 ∈ (PrmIdeal‘𝑅) ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))))
246	245	biimpar 476	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))) → 𝑖 ∈ (PrmIdeal‘𝑅))
247	2, 7, 44, 244, 246	syl13anc 1369	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (PrmIdeal‘𝑅))
248	247	anasss 465	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → 𝑖 ∈ (PrmIdeal‘𝑅))
249		simprr 771	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
250	248, 249	jca 510	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))
251		ssdifidlprm.3	. . 3 ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
252	34, 9	mgpbas 20092	. . . . 5 ⊢ 𝐵 = (Base‘𝑀)
253	252	submss 18769	. . . 4 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
254	33, 253	syl 17	. . 3 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
255		ssdifidlprm.6	. . 3 ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)
256	9, 8, 251, 254, 255, 3	ssdifidl 33269	. 2 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
257	250, 256	reximddv 3160	1 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084  ∀wal 1531   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2929  ∀wral 3050  ∃wrex 3059  {crab 3418   ∖ cdif 3941   ∩ cin 3943   ⊆ wss 3944   ⊊ wpss 3945  ∅c0 4322  {csn 4630  ‘cfv 6549  (class class class)co 7419  Basecbs 17183  +_gcplusg 17236  ._rcmulr 17237  SubMndcsubmnd 18742  SubGrpcsubg 19083  LSSumclsm 19601  mulGrpcmgp 20086  1_rcur 20133  Ringcrg 20185  CRingccrg 20186  LIdealclidl 21114  RSpancrsp 21115  PrmIdealcprmidl 33247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-ac2 10488  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-rpss 7729  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-oadd 8491  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-dju 9926  df-card 9964  df-ac 10141  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  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 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-mulr 17250  df-sca 17252  df-vsca 17253  df-ip 17254  df-0g 17426  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-submnd 18744  df-grp 18901  df-minusg 18902  df-sbg 18903  df-subg 19086  df-cntz 19280  df-lsm 19603  df-cmn 19749  df-abl 19750  df-mgp 20087  df-rng 20105  df-ur 20134  df-ring 20187  df-cring 20188  df-subrg 20520  df-lmod 20757  df-lss 20828  df-lsp 20868  df-sra 21070  df-rgmod 21071  df-lidl 21116  df-rsp 21117  df-prmidl 33248

This theorem is referenced by:  1arithufdlem4  33362