Theorem ssdifidlprm 33606

Description: If the set 𝑆 of ssdifidl 33605 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 736	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑅 ∈ CRing)
3		ssdifidlprm.7	. . . . . . . 8 ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}
4	3	ssrab3 4035	. . . . . . 7 ⊢ 𝑃 ⊆ (LIdeal‘𝑅)
5		simpr 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ 𝑃)
6	4, 5	sselid 3934	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (LIdeal‘𝑅))
7	6	adantr 484	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (LIdeal‘𝑅))
8	1	crngringd 20275	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
9		ssdifidlprm.1	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
10		eqid 2761	. . . . . . . . . 10 ⊢ (1r‘𝑅) = (1r‘𝑅)
11	9, 10	ringidcl 20294	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵)
12	8, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵)
13	12	ad2antrr 736	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1r‘𝑅) ∈ 𝐵)
14		eqid 2761	. . . . . . . . . . . 12 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
15	9, 14	lidlss 21262	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵)
16	6, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ⊆ 𝐵)
17	16	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ 𝐵)
18		incom 4161	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ 𝑝) = (𝑝 ∩ 𝑆)
19	18	eqeq1i 2766	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑝 ∩ 𝑆) = ∅)
20		ineq1 4165	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑖 → (𝑝 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	eqeq1d 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑖 → ((𝑝 ∩ 𝑆) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
22	19, 21	bitrid 285	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑖 ∩ 𝑆) = ∅))
23		sseq2 3962	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑖 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑖))
24	22, 23	anbi12d 641	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑖 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
25	24, 3	elrab2 3653	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝑃 ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
26	25	biimpi 218	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑃 → (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖)))
27	26	simprd 499	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝑃 → ((𝑖 ∩ 𝑆) = ∅ ∧ 𝐼 ⊆ 𝑖))
28	27	simpld 498	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑃 → (𝑖 ∩ 𝑆) = ∅)
29	28	ad2antlr 737	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (𝑖 ∩ 𝑆) = ∅)
30		reldisj 4406	. . . . . . . . . 10 ⊢ (𝑖 ⊆ 𝐵 → ((𝑖 ∩ 𝑆) = ∅ ↔ 𝑖 ⊆ (𝐵 ∖ 𝑆)))
31	30	biimpa 480	. . . . . . . . 9 ⊢ ((𝑖 ⊆ 𝐵 ∧ (𝑖 ∩ 𝑆) = ∅) → 𝑖 ⊆ (𝐵 ∖ 𝑆))
32	17, 29, 31	syl2anc 593	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ⊆ (𝐵 ∖ 𝑆))
33		ssdifidlprm.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))
34		ssdifidlprm.5	. . . . . . . . . . . . 13 ⊢ 𝑀 = (mulGrp‘𝑅)
35	34, 10	ringidval 20212	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (0g‘𝑀)
36	35	subm0cl 18828	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → (1r‘𝑅) ∈ 𝑆)
37	33, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆)
38	37	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → (1r‘𝑅) ∈ 𝑆)
39		elndif 4086	. . . . . . . . 9 ⊢ ((1r‘𝑅) ∈ 𝑆 → ¬ (1r‘𝑅) ∈ (𝐵 ∖ 𝑆))
40	38, 39	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1r‘𝑅) ∈ (𝐵 ∖ 𝑆))
41	32, 40	ssneldd 3939	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ¬ (1r‘𝑅) ∈ 𝑖)
42		nelne1 3053	. . . . . . 7 ⊢ (((1r‘𝑅) ∈ 𝐵 ∧ ¬ (1r‘𝑅) ∈ 𝑖) → 𝐵 ≠ 𝑖)
43	13, 41, 42	syl2anc 593	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝐵 ≠ 𝑖)
44	43	necomd 3011	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ≠ 𝐵)
45	29	ad4antr 742	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) = ∅)
46		ioran 996	. . . . . . . . . . 11 ⊢ (¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖) ↔ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖))
47	14	lidlsubg 21273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) → 𝑖 ∈ (SubGrp‘𝑅))
48	8, 6, 47	syl2an2r 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝑖 ∈ (SubGrp‘𝑅))
49	48	ad6antr 746	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (SubGrp‘𝑅))
50	8	ad7antr 748	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑅 ∈ Ring)
51		simp-5r 795	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ 𝐵)
52	51	snssd 4744	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑎} ⊆ 𝐵)
53		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (RSpan‘𝑅) = (RSpan‘𝑅)
54	53, 9, 14	rspcl 21285	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ {𝑎} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
55	50, 52, 54	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
56	14	lidlsubg 21273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
57	50, 55, 56	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅))
58		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (LSSum‘𝑅) = (LSSum‘𝑅)
59	58	lsmub1 19680	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
60	49, 57, 59	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
61	58	lsmub2 19681	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑎}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
62	49, 57, 61	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑎}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
63	9, 53	rspsnid 33518	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
64	50, 51, 63	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ ((RSpan‘𝑅)‘{𝑎}))
65	62, 64	sseldd 3937	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑎 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
66		simplr 778	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑎 ∈ 𝑖)
67	60, 65, 66	ssnelpssd 4069	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
68	7	ad5antr 744	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
69	9, 58, 53, 50, 68, 55	lsmidl 33548	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅))
70	27	simprd 499	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑃 → 𝐼 ⊆ 𝑖)
71	70	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃) → 𝐼 ⊆ 𝑖)
72	71	ad6antr 746	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ 𝑖)
73	72, 60	sstrd 3946	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
74	69, 73	jca 519	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
75		simp-6r 797	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
76		df-ral 3076	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗))
77		con2b 361	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ (𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
78	77	albii 1838	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗(𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗) ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
79	76, 78	bitri 277	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
80	75, 79	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃))
81		ineq2 4166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 = 𝑗 → (𝑆 ∩ 𝑝) = (𝑆 ∩ 𝑗))
82	81	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅))
83		sseq2 3962	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑗 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑗))
84	82, 83	anbi12d 641	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑗 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
85	84, 3	elrab2 3653	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ 𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
86	85	baib 543	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (LIdeal‘𝑅) → (𝑗 ∈ 𝑃 ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
87	86	rbaibd 548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → (𝑗 ∈ 𝑃 ↔ (𝑆 ∩ 𝑗) = ∅))
88	87	notbid 320	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → (¬ 𝑗 ∈ 𝑃 ↔ ¬ (𝑆 ∩ 𝑗) = ∅))
89	88	biimpcd 251	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑗 ∈ 𝑃 → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → ¬ (𝑆 ∩ 𝑗) = ∅))
90	89	imim2i 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → (𝑖 ⊊ 𝑗 → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) → ¬ (𝑆 ∩ 𝑗) = ∅)))
91	90	impd 414	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
92	91	alimi 1830	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑗(𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃) → ∀𝑗((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅))
93		ovex 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ V
94		psseq2 4044	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
95		eleq1 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅)))
96		sseq2 3962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
97	95, 96	anbi12d 641	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) ↔ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))))
98	94, 97	anbi12d 641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) ↔ (𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))))
99		ineq2 4166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
100	99	eqeq1d 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → ((𝑆 ∩ 𝑗) = ∅ ↔ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
101	100	notbid 320	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (¬ (𝑆 ∩ 𝑗) = ∅ ↔ ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅))
102	98, 101	imbi12d 346	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) → (((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) ↔ ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅)))
103	93, 102	spcv 3564	. . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅)
106		neq0 4304	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) = ∅ ↔ ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
107	105, 106	sylib 220	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑒 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
108		simp-4r 793	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ 𝐵)
109	108	snssd 4744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → {𝑏} ⊆ 𝐵)
110	53, 9, 14	rspcl 21285	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ {𝑏} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
111	50, 109, 110	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
112	14	lidlsubg 21273	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
113	50, 111, 112	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅))
114	58	lsmub1 19680	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
115	49, 113, 114	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
116	58	lsmub2 19681	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (SubGrp‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑏}) ∈ (SubGrp‘𝑅)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
117	49, 113, 116	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((RSpan‘𝑅)‘{𝑏}) ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
118	9, 53	rspsnid 33518	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
119	50, 108, 118	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ ((RSpan‘𝑅)‘{𝑏}))
120	117, 119	sseldd 3937	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑏 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
121		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ 𝑏 ∈ 𝑖)
122	115, 120, 121	ssnelpssd 4069	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
123	9, 58, 53, 50, 68, 111	lsmidl 33548	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅))
124	72, 115	sstrd 3946	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
125	123, 124	jca 519	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
126		ovex 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ V
127		psseq2 4044	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
128		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑗 ∈ (LIdeal‘𝑅) ↔ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅)))
129		sseq2 3962	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
130	128, 129	anbi12d 641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗) ↔ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))))
131	127, 130	anbi12d 641	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) ↔ (𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))))
132		ineq2 4166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (𝑆 ∩ 𝑗) = (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
133	132	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → ((𝑆 ∩ 𝑗) = ∅ ↔ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
134	133	notbid 320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (¬ (𝑆 ∩ 𝑗) = ∅ ↔ ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅))
135	131, 134	imbi12d 346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) → (((𝑖 ⊊ 𝑗 ∧ (𝑗 ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ 𝑗)) → ¬ (𝑆 ∩ 𝑗) = ∅) ↔ ((𝑖 ⊊ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∧ ((𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ∈ (LIdeal‘𝑅) ∧ 𝐼 ⊆ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅)))
136	126, 135	spcv 3564	. . . . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅)
139		neq0 4304	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) = ∅ ↔ ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
140	138, 139	sylib 220	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
141	140	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → ∃𝑓 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
142	50	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑅 ∈ Ring)
143	142	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → 𝑅 ∈ Ring)
144	51	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑎 ∈ 𝐵)
145	144	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → 𝑎 ∈ 𝐵)
146		eqid 2761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (.r‘𝑅) = (.r‘𝑅)
147	9, 146, 53	elrspsn 21290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → (𝑚 ∈ ((RSpan‘𝑅)‘{𝑎}) ↔ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)))
148	143, 145, 147	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑚 ∈ ((RSpan‘𝑅)‘{𝑎}) ↔ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)))
149	142	ad6antr 746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → 𝑅 ∈ Ring)
150	108	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑏 ∈ 𝐵)
151	150	ad6antr 746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → 𝑏 ∈ 𝐵)
152	9, 146, 53	elrspsn 21290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵) → (𝑛 ∈ ((RSpan‘𝑅)‘{𝑏}) ↔ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)))
153	149, 151, 152	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑛 ∈ ((RSpan‘𝑅)‘{𝑏}) ↔ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)))
154		simp-7r 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑒 = (𝑥(+g‘𝑅)𝑚))
155		simpllr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑓 = (𝑦(+g‘𝑅)𝑛))
156	154, 155	oveq12d 7410	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) = ((𝑥(+g‘𝑅)𝑚)(.r‘𝑅)(𝑦(+g‘𝑅)𝑛)))
157		simp-5r 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑚 = (𝑜(.r‘𝑅)𝑎))
158	157	oveq2d 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(+g‘𝑅)𝑚) = (𝑥(+g‘𝑅)(𝑜(.r‘𝑅)𝑎)))
159		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑛 = (𝑞(.r‘𝑅)𝑏))
160	159	oveq2d 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑦(+g‘𝑅)𝑛) = (𝑦(+g‘𝑅)(𝑞(.r‘𝑅)𝑏)))
161	158, 160	oveq12d 7410	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(+g‘𝑅)𝑚)(.r‘𝑅)(𝑦(+g‘𝑅)𝑛)) = ((𝑥(+g‘𝑅)(𝑜(.r‘𝑅)𝑎))(.r‘𝑅)(𝑦(+g‘𝑅)(𝑞(.r‘𝑅)𝑏))))
162		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (+g‘𝑅) = (+g‘𝑅)
163	149	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑅 ∈ Ring)
164	17	ad7antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑖 ⊆ 𝐵)
165	164	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑖 ⊆ 𝐵)
166	165	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ⊆ 𝐵)
167		simp-8r 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑥 ∈ 𝑖)
168	166, 167	sseldd 3937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑥 ∈ 𝐵)
169		simp-6r 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑜 ∈ 𝐵)
170	144	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑎 ∈ 𝐵)
171	9, 146, 163, 169, 170	ringcld 20289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑜(.r‘𝑅)𝑎) ∈ 𝐵)
172		simp-4r 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑦 ∈ 𝑖)
173	166, 172	sseldd 3937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑦 ∈ 𝐵)
174		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑞 ∈ 𝐵)
175	151	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑏 ∈ 𝐵)
176	9, 146, 163, 174, 175	ringcld 20289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑞(.r‘𝑅)𝑏) ∈ 𝐵)
177	9, 162, 146, 163, 168, 171, 173, 176	ringdi22 33371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(+g‘𝑅)(𝑜(.r‘𝑅)𝑎))(.r‘𝑅)(𝑦(+g‘𝑅)(𝑞(.r‘𝑅)𝑏))) = (((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦))(+g‘𝑅)((𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)))))
178	156, 161, 177	3eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) = (((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦))(+g‘𝑅)((𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)))))
179	68	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑖 ∈ (LIdeal‘𝑅))
180	179	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ∈ (LIdeal‘𝑅))
181	163, 180, 47	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑖 ∈ (SubGrp‘𝑅))
182	14, 9, 146, 163, 180, 168, 172	lidlmcld 33566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑖)
183	14, 9, 146, 163, 180, 171, 172	lidlmcld 33566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦) ∈ 𝑖)
184	162, 181, 182, 183	subgcld 33182	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦)) ∈ 𝑖)
185	2	ad7antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑅 ∈ CRing)
186	185	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑅 ∈ CRing)
187	186	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → 𝑅 ∈ CRing)
188	9, 146, 187, 168, 176	crngcomd 20284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑞(.r‘𝑅)𝑏)(.r‘𝑅)𝑥))
189	14, 9, 146, 163, 180, 176, 167	lidlmcld 33566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑞(.r‘𝑅)𝑏)(.r‘𝑅)𝑥) ∈ 𝑖)
190	188, 189	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) ∈ 𝑖)
191	9, 146	cringm4 33593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ CRing ∧ (𝑜 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑞 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)))
192	187, 169, 170, 174, 175, 191	syl122anc 1397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) = ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)))
193	9, 146, 163, 169, 174	ringcld 20289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑜(.r‘𝑅)𝑞) ∈ 𝐵)
194		simp-5r 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑎(.r‘𝑅)𝑏) ∈ 𝑖)
195	194	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑎(.r‘𝑅)𝑏) ∈ 𝑖)
196	14, 9, 146, 163, 180, 193, 195	lidlmcld 33566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑞)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)) ∈ 𝑖)
197	192, 196	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)) ∈ 𝑖)
198	162, 181, 190, 197	subgcld 33182	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → ((𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))) ∈ 𝑖)
199	162, 181, 184, 198	subgcld 33182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)𝑦))(+g‘𝑅)((𝑥(.r‘𝑅)(𝑞(.r‘𝑅)𝑏))(+g‘𝑅)((𝑜(.r‘𝑅)𝑎)(.r‘𝑅)(𝑞(.r‘𝑅)𝑏)))) ∈ 𝑖)
200	178, 199	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
201	200	r19.29an 3165	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ ∃𝑞 ∈ 𝐵 𝑛 = (𝑞(.r‘𝑅)𝑏)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
202	153, 201	sylbida 601	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) ∧ 𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
203	202	an32s 662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ 𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})) ∧ 𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
204	203	r19.29an 3165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) ∧ 𝑦 ∈ 𝑖) ∧ ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
205	111	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅))
206	9, 14	lidlss 21262	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((RSpan‘𝑅)‘{𝑏}) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
207	205, 206	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
208	207	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵)
209		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))))
210	209	elin2d 4157	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
211	210	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))
212	9, 162, 58	lsmelvalx 19663	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵) → (𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})) ↔ ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛)))
213	212	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑏}) ⊆ 𝐵) ∧ 𝑓 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏}))) → ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛))
214	186, 165, 208, 211, 213	syl31anc 1391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → ∃𝑦 ∈ 𝑖 ∃𝑛 ∈ ((RSpan‘𝑅)‘{𝑏})𝑓 = (𝑦(+g‘𝑅)𝑛))
215	204, 214	r19.29a 3169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑜 ∈ 𝐵) ∧ 𝑚 = (𝑜(.r‘𝑅)𝑎)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
216	215	r19.29an 3165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ ∃𝑜 ∈ 𝐵 𝑚 = (𝑜(.r‘𝑅)𝑎)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
217	148, 216	sylbida 601	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) ∧ 𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
218	217	an32s 662	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ 𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})) ∧ 𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
219	218	r19.29an 3165	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) ∧ 𝑥 ∈ 𝑖) ∧ ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚)) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
220	55	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅))
221	9, 14	lidlss 21262	. . . . . . . . . . . . . . . . . . 19 ⊢ (((RSpan‘𝑅)‘{𝑎}) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵)
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵)
223		simplr 778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))))
224	223	elin2d 4157	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))
225	9, 162, 58	lsmelvalx 19663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵) → (𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})) ↔ ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚)))
226	225	biimpa 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ((RSpan‘𝑅)‘{𝑎}) ⊆ 𝐵) ∧ 𝑒 ∈ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎}))) → ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚))
227	185, 164, 222, 224, 226	syl31anc 1391	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → ∃𝑥 ∈ 𝑖 ∃𝑚 ∈ ((RSpan‘𝑅)‘{𝑎})𝑒 = (𝑥(+g‘𝑅)𝑚))
228	219, 227	r19.29a 3169	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑖)
229	34, 146	mgpplusg 20173	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘𝑅) = (+g‘𝑀)
230	33	ad9antr 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑆 ∈ (SubMnd‘𝑀))
231	223	elin1d 4156	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑒 ∈ 𝑆)
232	209	elin1d 4156	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → 𝑓 ∈ 𝑆)
233	229, 230, 231, 232	submcld 33174	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ 𝑆)
234	228, 233	elind 4152	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑒(.r‘𝑅)𝑓) ∈ (𝑖 ∩ 𝑆))
235	234	ne0d 4294	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) ∧ 𝑓 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑏})))) → (𝑖 ∩ 𝑆) ≠ ∅)
236	141, 235	exlimddv 1954	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) ∧ 𝑒 ∈ (𝑆 ∩ (𝑖(LSSum‘𝑅)((RSpan‘𝑅)‘{𝑎})))) → (𝑖 ∩ 𝑆) ≠ ∅)
237	107, 236	exlimddv 1954	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ 𝑎 ∈ 𝑖) ∧ ¬ 𝑏 ∈ 𝑖) → (𝑖 ∩ 𝑆) ≠ ∅)
238	237	anasss 470	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ (¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
239	46, 238	sylan2b 603	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → (𝑖 ∩ 𝑆) ≠ ∅)
240	239	neneqd 2961	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) ∧ ¬ (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)) → ¬ (𝑖 ∩ 𝑆) = ∅)
241	45, 240	condan 827	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ (𝑎(.r‘𝑅)𝑏) ∈ 𝑖) → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖))
242	241	ex 416	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
243	242	anasss 470	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
244	243	ralrimivva 3204	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))
245	9, 146	isprmidlc 33594	. . . . . 6 ⊢ (𝑅 ∈ CRing → (𝑖 ∈ (PrmIdeal‘𝑅) ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))))
246	245	biimpar 481	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(.r‘𝑅)𝑏) ∈ 𝑖 → (𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖)))) → 𝑖 ∈ (PrmIdeal‘𝑅))
247	2, 7, 44, 244, 246	syl13anc 1390	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (PrmIdeal‘𝑅))
248	247	anasss 470	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → 𝑖 ∈ (PrmIdeal‘𝑅))
249		simprr 782	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
250	248, 249	jca 519	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) → (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))
251		ssdifidlprm.3	. . 3 ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
252	34, 9	mgpbas 20174	. . . . 5 ⊢ 𝐵 = (Base‘𝑀)
253	252	submss 18826	. . . 4 ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
254	33, 253	syl 17	. . 3 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
255		ssdifidlprm.6	. . 3 ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)
256	9, 8, 251, 254, 255, 3	ssdifidl 33605	. 2 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
257	250, 256	reximddv 3177	1 ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1097  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141   ≠ wne 2956  ∀wral 3075  ∃wrex 3085  {crab 3413   ∖ cdif 3901   ∩ cin 3903   ⊆ wss 3904   ⊊ wpss 3905  ∅c0 4285  {csn 4581  ‘cfv 6517  (class class class)co 7392  Basecbs 17228  +_gcplusg 17269  ._rcmulr 17270  SubMndcsubmnd 18799  SubGrpcsubg 19145  LSSumclsm 19657  mulGrpcmgp 20169  1_rcur 20210  Ringcrg 20262  CRingccrg 20263  LIdealclidl 21256  RSpancrsp 21257  PrmIdealcprmidl 33582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-ac2 10417  ax-cnex 11126  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4905  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-se 5599  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-isom 6526  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-rpss 7702  df-om 7843  df-1st 7966  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-1o 8432  df-oadd 8436  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-fin 8927  df-dju 9856  df-card 9894  df-ac 10069  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-nn 12208  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17229  df-ress 17250  df-plusg 17282  df-mulr 17283  df-sca 17285  df-vsca 17286  df-ip 17287  df-0g 17453  df-mgm 18657  df-sgrp 18736  df-mnd 18752  df-submnd 18801  df-grp 18961  df-minusg 18962  df-sbg 18963  df-subg 19148  df-cntz 19340  df-lsm 19659  df-cmn 19805  df-abl 19806  df-mgp 20170  df-rng 20182  df-ur 20211  df-ring 20264  df-cring 20265  df-subrg 20599  df-lmod 20909  df-lss 20979  df-lsp 21019  df-sra 21220  df-rgmod 21221  df-lidl 21258  df-rsp 21259  df-prmidl 33583

This theorem is referenced by:  1arithufdlem4  33704