Theorem rlocisunit

Description: Characterize the units of the localization L of a ring R at S as the elements with a "numerator" P in the saturation T of S . (Contributed by Thierry Arnoux, 6-Jun-2026)

	Ref	Expression
Hypotheses	rlocisunit.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rlocisunit.m	⊢ · = ( .r ‘ 𝑅 )
	rlocisunit.l	⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
	rlocisunit.w	⊢ 𝑊 = ( Unit ‘ 𝐿 )
	rlocisunit.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	rlocisunit.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
	rlocisunit.e	⊢ ∼ = ( 𝑅 ~RL 𝑆 )
	rlocisunit.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	rlocisunit.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
	rlocisunit.t	⊢ 𝑇 = { 𝑟 ∈ 𝐵 ∣ ∃ 𝑠 ∈ 𝐵 ( 𝑟 · 𝑠 ) ∈ 𝑆 }
Assertion	rlocisunit	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , 𝑄 ⟩ ] ∼ ∈ 𝑊 ↔ 𝑃 ∈ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		rlocisunit.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rlocisunit.m	⊢ · = ( .r ‘ 𝑅 )
3		rlocisunit.l	⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
4		rlocisunit.w	⊢ 𝑊 = ( Unit ‘ 𝐿 )
5		rlocisunit.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		rlocisunit.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
7		rlocisunit.e	⊢ ∼ = ( 𝑅 ~RL 𝑆 )
8		rlocisunit.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
9		rlocisunit.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
10		rlocisunit.t	⊢ 𝑇 = { 𝑟 ∈ 𝐵 ∣ ∃ 𝑠 ∈ 𝐵 ( 𝑟 · 𝑠 ) ∈ 𝑆 }
11	10	eleq2i	⊢ ( 𝑃 ∈ 𝑇 ↔ 𝑃 ∈ { 𝑟 ∈ 𝐵 ∣ ∃ 𝑠 ∈ 𝐵 ( 𝑟 · 𝑠 ) ∈ 𝑆 } )
12		oveq1	⊢ ( 𝑟 = 𝑃 → ( 𝑟 · 𝑠 ) = ( 𝑃 · 𝑠 ) )
13	12	eleq1d	⊢ ( 𝑟 = 𝑃 → ( ( 𝑟 · 𝑠 ) ∈ 𝑆 ↔ ( 𝑃 · 𝑠 ) ∈ 𝑆 ) )
14	13	rexbidv	⊢ ( 𝑟 = 𝑃 → ( ∃ 𝑠 ∈ 𝐵 ( 𝑟 · 𝑠 ) ∈ 𝑆 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 ) )
15	14	elrab	⊢ ( 𝑃 ∈ { 𝑟 ∈ 𝐵 ∣ ∃ 𝑠 ∈ 𝐵 ( 𝑟 · 𝑠 ) ∈ 𝑆 } ↔ ( 𝑃 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 ) )
16	11 15	bitri	⊢ ( 𝑃 ∈ 𝑇 ↔ ( 𝑃 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 ) )
17	8	biantrurd	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 ↔ ( 𝑃 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 ) ) )
18	16 17	bitr4id	⊢ ( 𝜑 → ( 𝑃 ∈ 𝑇 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 ) )
19		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
20		eqid	⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
21		eqid	⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 )
22		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
23		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
24	22 23	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
25	24	subm0cl	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
26	6 25	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
27	8 26	opelxpd	⊢ ( 𝜑 → ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ∈ ( 𝐵 × 𝑆 ) )
28	7	ovexi	⊢ ∼ ∈ V
29	28	ecelqsi	⊢ ( ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ∈ ( 𝐵 × 𝑆 ) → [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
30	27 29	syl	⊢ ( 𝜑 → [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
31		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
32		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
33		eqid	⊢ ( 𝐵 × 𝑆 ) = ( 𝐵 × 𝑆 )
34	22 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
35	34	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 𝑆 ⊆ 𝐵 )
36	6 35	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
37	1 31 2 32 33 3 7 5 36	rlocbas	⊢ ( 𝜑 → ( ( 𝐵 × 𝑆 ) / ∼ ) = ( Base ‘ 𝐿 ) )
38	30 37	eleqtrd	⊢ ( 𝜑 → [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) )
39		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
40	1 2 39 3 7 5 6	rloccring	⊢ ( 𝜑 → 𝐿 ∈ CRing )
41	19 4 20 21 38 40	isunitc	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ 𝑊 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) )
42	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
43	42	ad7antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
44	36	ad7antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑆 ⊆ 𝐵 )
45		simplr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑡 ∈ 𝑆 )
46	44 45	sseldd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑡 ∈ 𝐵 )
47		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → 𝑟 ∈ 𝐵 )
48	47	ad2antrr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑟 ∈ 𝐵 )
49	1 2 43 46 48	ringcld	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑡 · 𝑟 ) ∈ 𝐵 )
50		oveq2	⊢ ( 𝑢 = ( 𝑡 · 𝑟 ) → ( 𝑃 · 𝑢 ) = ( 𝑃 · ( 𝑡 · 𝑟 ) ) )
51	50	eleq1d	⊢ ( 𝑢 = ( 𝑡 · 𝑟 ) → ( ( 𝑃 · 𝑢 ) ∈ 𝑆 ↔ ( 𝑃 · ( 𝑡 · 𝑟 ) ) ∈ 𝑆 ) )
52	51	adantl	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) ∧ 𝑢 = ( 𝑡 · 𝑟 ) ) → ( ( 𝑃 · 𝑢 ) ∈ 𝑆 ↔ ( 𝑃 · ( 𝑡 · 𝑟 ) ) ∈ 𝑆 ) )
53	5	ad7antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑅 ∈ CRing )
54	8	ad7antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑃 ∈ 𝐵 )
55	1 2 53 54 46 48	crng12d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑃 · ( 𝑡 · 𝑟 ) ) = ( 𝑡 · ( 𝑃 · 𝑟 ) ) )
56	1 2 43 54 48	ringcld	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑃 · 𝑟 ) ∈ 𝐵 )
57	1 2 23 43 56	ringridmd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) = ( 𝑃 · 𝑟 ) )
58	57	oveq2d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( 𝑃 · 𝑟 ) ) )
59	55 58	eqtr4d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑃 · ( 𝑡 · 𝑟 ) ) = ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) )
60		simpr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) )
61	36 26	sseldd	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
62	61	ad7antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
63		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → 𝑠 ∈ 𝑆 )
64	63	ad2antrr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑠 ∈ 𝑆 )
65	44 64	sseldd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑠 ∈ 𝐵 )
66	1 2 43 62 65	ringcld	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( ( 1r ‘ 𝑅 ) · 𝑠 ) ∈ 𝐵 )
67	1 2 23 43 66	ringlidmd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) = ( ( 1r ‘ 𝑅 ) · 𝑠 ) )
68	1 2 23 43 65	ringlidmd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( ( 1r ‘ 𝑅 ) · 𝑠 ) = 𝑠 )
69	67 68	eqtrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) = 𝑠 )
70	69	oveq2d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) = ( 𝑡 · 𝑠 ) )
71	59 60 70	3eqtrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑃 · ( 𝑡 · 𝑟 ) ) = ( 𝑡 · 𝑠 ) )
72	22 2	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
73	6	ad7antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
74	72 73 45 64	submcld	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑡 · 𝑠 ) ∈ 𝑆 )
75	71 74	eqeltrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ( 𝑃 · ( 𝑡 · 𝑟 ) ) ∈ 𝑆 )
76	49 52 75	rspcedvd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 )
77		simp-5l	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → 𝜑 )
78		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ )
79	78	oveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) )
80		simp-4r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) )
81	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑅 ∈ CRing )
82	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
83	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑃 ∈ 𝐵 )
84		simplr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑟 ∈ 𝐵 )
85	82 25	syl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
86		simpr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝑆 )
87	1 2 39 3 7 81 82 83 84 85 86 20	rlocmulval	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) = [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ )
88	77 47 63 87	syl21anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) = [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ )
89	79 80 88	3eqtr3rd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = ( 1r ‘ 𝐿 ) )
90		eqid	⊢ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼
91	31 23 3 7 5 6 90	rloc1r	⊢ ( 𝜑 → [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ = ( 1r ‘ 𝐿 ) )
92	91	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ = ( 1r ‘ 𝐿 ) )
93	89 92	eqtr4d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ )
94	81	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ) → 𝑅 ∈ CRing )
95	82	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
96	42	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑅 ∈ Ring )
97	1 2 96 83 84	ringcld	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑃 · 𝑟 ) ∈ 𝐵 )
98	97	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ) → ( 𝑃 · 𝑟 ) ∈ 𝐵 )
99	72 82 85 86	submcld	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( ( 1r ‘ 𝑅 ) · 𝑠 ) ∈ 𝑆 )
100	99	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ) → ( ( 1r ‘ 𝑅 ) · 𝑠 ) ∈ 𝑆 )
101	61	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
102	95 25	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
103		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ) → [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ )
104	1 7 2 94 95 98 100 101 102 103	erld2	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ [ ⟨ ( 𝑃 · 𝑟 ) , ( ( 1r ‘ 𝑅 ) · 𝑠 ) ⟩ ] ∼ = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ) → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) )
105	77 47 63 93 104	syl1111anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( 𝑃 · 𝑟 ) · ( 1r ‘ 𝑅 ) ) ) = ( 𝑡 · ( ( 1r ‘ 𝑅 ) · ( ( 1r ‘ 𝑅 ) · 𝑠 ) ) ) )
106	76 105	r19.29a	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 )
107	106	r19.29an	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑆 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ ) → ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 )
108	37	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) ↔ 𝑥 ∈ ( Base ‘ 𝐿 ) ) )
109	108	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) → 𝑥 ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
110	109	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) → 𝑥 ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
111	110	elrlocbasi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) → ∃ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑆 𝑥 = [ ⟨ 𝑟 , 𝑠 ⟩ ] ∼ )
112	107 111	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 )
113	112	r19.29an	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 )
114		simplr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → 𝑢 ∈ 𝐵 )
115		simpr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( 𝑃 · 𝑢 ) ∈ 𝑆 )
116	114 115	opelxpd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ∈ ( 𝐵 × 𝑆 ) )
117	28	ecelqsi	⊢ ( ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ∈ ( 𝐵 × 𝑆 ) → [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
118	116 117	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
119	37	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( ( 𝐵 × 𝑆 ) / ∼ ) = ( Base ‘ 𝐿 ) )
120	118 119	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) )
121		oveq2	⊢ ( 𝑥 = [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ) )
122	121	eqeq1d	⊢ ( 𝑥 = [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ → ( ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ↔ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ) = ( 1r ‘ 𝐿 ) ) )
123	122	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ) → ( ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ↔ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ) = ( 1r ‘ 𝐿 ) ) )
124	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → 𝑅 ∈ CRing )
125	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
126	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → 𝑃 ∈ 𝐵 )
127	125 25	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
128	1 2 39 3 7 124 125 126 114 127 115 20	rlocmulval	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ) = [ ⟨ ( 𝑃 · 𝑢 ) , ( ( 1r ‘ 𝑅 ) · ( 𝑃 · 𝑢 ) ) ⟩ ] ∼ )
129	1 31 23 2 32 33 7 5 6	erler	⊢ ( 𝜑 → ∼ Er ( 𝐵 × 𝑆 ) )
130	129	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ∼ Er ( 𝐵 × 𝑆 ) )
131		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ = ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ )
132		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( 𝑃 · 𝑢 ) = ( 𝑃 · 𝑢 ) )
133	42	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → 𝑅 ∈ Ring )
134	1 2 133 126 114	ringcld	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( 𝑃 · 𝑢 ) ∈ 𝐵 )
135	1 2 23 133 134	ringlidmd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( ( 1r ‘ 𝑅 ) · ( 𝑃 · 𝑢 ) ) = ( 𝑃 · 𝑢 ) )
136	132 135	opeq12d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ⟨ ( 𝑃 · 𝑢 ) , ( ( 1r ‘ 𝑅 ) · ( 𝑃 · 𝑢 ) ) ⟩ = ⟨ ( 𝑃 · 𝑢 ) , ( 𝑃 · 𝑢 ) ⟩ )
137	61	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
138	1 2 23 133 134	ringridmd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( ( 𝑃 · 𝑢 ) · ( 1r ‘ 𝑅 ) ) = ( 𝑃 · 𝑢 ) )
139	138	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( 𝑃 · 𝑢 ) = ( ( 𝑃 · 𝑢 ) · ( 1r ‘ 𝑅 ) ) )
140	1 7 124 125 2 131 136 137 134 127 115 115 139 139	erlbr2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ∼ ⟨ ( 𝑃 · 𝑢 ) , ( ( 1r ‘ 𝑅 ) · ( 𝑃 · 𝑢 ) ) ⟩ )
141	130 140	erthi	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ = [ ⟨ ( 𝑃 · 𝑢 ) , ( ( 1r ‘ 𝑅 ) · ( 𝑃 · 𝑢 ) ) ⟩ ] ∼ )
142	31 23 3 7 124 125 90	rloc1r	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ∼ = ( 1r ‘ 𝐿 ) )
143	128 141 142	3eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑢 , ( 𝑃 · 𝑢 ) ⟩ ] ∼ ) = ( 1r ‘ 𝐿 ) )
144	120 123 143	rspcedvd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) )
145	144	r19.29an	⊢ ( ( 𝜑 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 ) → ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) )
146	113 145	impbida	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = ( 1r ‘ 𝐿 ) ↔ ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 ) )
147		oveq2	⊢ ( 𝑢 = 𝑠 → ( 𝑃 · 𝑢 ) = ( 𝑃 · 𝑠 ) )
148	147	eleq1d	⊢ ( 𝑢 = 𝑠 → ( ( 𝑃 · 𝑢 ) ∈ 𝑆 ↔ ( 𝑃 · 𝑠 ) ∈ 𝑆 ) )
149	148	cbvrexvw	⊢ ( ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 )
150	149	a1i	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝐵 ( 𝑃 · 𝑢 ) ∈ 𝑆 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 ) )
151	41 146 150	3bitrd	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ 𝑊 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑃 · 𝑠 ) ∈ 𝑆 ) )
152	5	adantr	⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝑆 ) → 𝑅 ∈ CRing )
153	6	adantr	⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝑆 ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
154		simpr	⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝑆 ) → 𝑄 ∈ 𝑆 )
155	1 23 7 3 4 152 153 154	rlocinvunit	⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝑆 ) → [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ 𝑊 )
156	9 155	mpdan	⊢ ( 𝜑 → [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ 𝑊 )
157	156	biantrud	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ 𝑊 ↔ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ 𝑊 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ 𝑊 ) ) )
158	1 2 39 3 7 5 6 8 61 26 9 20	rlocmulval	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ) = [ ⟨ ( 𝑃 · ( 1r ‘ 𝑅 ) ) , ( ( 1r ‘ 𝑅 ) · 𝑄 ) ⟩ ] ∼ )
159	1 2 23 42 8	ringridmd	⊢ ( 𝜑 → ( 𝑃 · ( 1r ‘ 𝑅 ) ) = 𝑃 )
160	36 9	sseldd	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
161	1 2 23 42 160	ringlidmd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑄 ) = 𝑄 )
162	159 161	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝑃 · ( 1r ‘ 𝑅 ) ) , ( ( 1r ‘ 𝑅 ) · 𝑄 ) ⟩ = ⟨ 𝑃 , 𝑄 ⟩ )
163	162	eceq1d	⊢ ( 𝜑 → [ ⟨ ( 𝑃 · ( 1r ‘ 𝑅 ) ) , ( ( 1r ‘ 𝑅 ) · 𝑄 ) ⟩ ] ∼ = [ ⟨ 𝑃 , 𝑄 ⟩ ] ∼ )
164	158 163	eqtrd	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ) = [ ⟨ 𝑃 , 𝑄 ⟩ ] ∼ )
165	164	eleq1d	⊢ ( 𝜑 → ( ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ) ∈ 𝑊 ↔ [ ⟨ 𝑃 , 𝑄 ⟩ ] ∼ ∈ 𝑊 ) )
166	61 9	opelxpd	⊢ ( 𝜑 → ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ∈ ( 𝐵 × 𝑆 ) )
167	28	ecelqsi	⊢ ( ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ∈ ( 𝐵 × 𝑆 ) → [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
168	166 167	syl	⊢ ( 𝜑 → [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
169	168 37	eleqtrd	⊢ ( 𝜑 → [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) )
170	4 20 19	unitmulclb	⊢ ( ( 𝐿 ∈ CRing ∧ [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) ∧ [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) ) → ( ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ) ∈ 𝑊 ↔ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ 𝑊 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ 𝑊 ) ) )
171	40 38 169 170	syl3anc	⊢ ( 𝜑 → ( ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ) ∈ 𝑊 ↔ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ 𝑊 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ 𝑊 ) ) )
172	165 171	bitr3d	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , 𝑄 ⟩ ] ∼ ∈ 𝑊 ↔ ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ 𝑊 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , 𝑄 ⟩ ] ∼ ∈ 𝑊 ) ) )
173	157 172	bitr4d	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , ( 1r ‘ 𝑅 ) ⟩ ] ∼ ∈ 𝑊 ↔ [ ⟨ 𝑃 , 𝑄 ⟩ ] ∼ ∈ 𝑊 ) )
174	18 151 173	3bitr2rd	⊢ ( 𝜑 → ( [ ⟨ 𝑃 , 𝑄 ⟩ ] ∼ ∈ 𝑊 ↔ 𝑃 ∈ 𝑇 ) )