Theorem lmodprop2d

Description: If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015)

	Ref	Expression
Hypotheses	lmodprop2d.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	lmodprop2d.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	lmodprop2d.f	⊢ 𝐹 = ( Scalar ‘ 𝐾 )
	lmodprop2d.g	⊢ 𝐺 = ( Scalar ‘ 𝐿 )
	lmodprop2d.p1	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
	lmodprop2d.p2	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
	lmodprop2d.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
	lmodprop2d.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
	lmodprop2d.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) )
	lmodprop2d.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
Assertion	lmodprop2d	⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )

Proof

Step	Hyp	Ref	Expression
1		lmodprop2d.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		lmodprop2d.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		lmodprop2d.f	⊢ 𝐹 = ( Scalar ‘ 𝐾 )
4		lmodprop2d.g	⊢ 𝐺 = ( Scalar ‘ 𝐿 )
5		lmodprop2d.p1	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
6		lmodprop2d.p2	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
7		lmodprop2d.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
8		lmodprop2d.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
9		lmodprop2d.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) )
10		lmodprop2d.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
11		lmodgrp	⊢ ( 𝐾 ∈ LMod → 𝐾 ∈ Grp )
12	11	a1i	⊢ ( 𝜑 → ( 𝐾 ∈ LMod → 𝐾 ∈ Grp ) )
13		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14		eqid	⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
15		eqid	⊢ ( ·𝑠 ‘ 𝐾 ) = ( ·𝑠 ‘ 𝐾 )
16		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
17		eqid	⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
18		eqid	⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
19		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
20	13 14 15 3 16 17 18 19	islmod	⊢ ( 𝐾 ∈ LMod ↔ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ 𝐹 ) ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
21	20	simp2bi	⊢ ( 𝐾 ∈ LMod → 𝐹 ∈ Ring )
22	21	a1i	⊢ ( 𝜑 → ( 𝐾 ∈ LMod → 𝐹 ∈ Ring ) )
23		simplr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐾 ∈ LMod )
24		simprl	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝑃 )
25	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 = ( Base ‘ 𝐹 ) )
26	24 25	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
27		simprr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
28	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
29	27 28	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
30	13 3 15 16	lmodvscl	⊢ ( ( 𝐾 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
31	23 26 29 30	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
32	31 28	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
33	32	ralrimivva	⊢ ( ( 𝜑 ∧ 𝐾 ∈ LMod ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
34	33	ex	⊢ ( 𝜑 → ( 𝐾 ∈ LMod → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) )
35	12 22 34	3jcad	⊢ ( 𝜑 → ( 𝐾 ∈ LMod → ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) )
36		lmodgrp	⊢ ( 𝐿 ∈ LMod → 𝐿 ∈ Grp )
37	1 2 7	grppropd	⊢ ( 𝜑 → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )
38	36 37	imbitrrid	⊢ ( 𝜑 → ( 𝐿 ∈ LMod → 𝐾 ∈ Grp ) )
39		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
40		eqid	⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
41		eqid	⊢ ( ·𝑠 ‘ 𝐿 ) = ( ·𝑠 ‘ 𝐿 )
42		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
43		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
44		eqid	⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝐺 )
45		eqid	⊢ ( 1r ‘ 𝐺 ) = ( 1r ‘ 𝐺 )
46	39 40 41 4 42 43 44 45	islmod	⊢ ( 𝐿 ∈ LMod ↔ ( 𝐿 ∈ Grp ∧ 𝐺 ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ 𝐺 ) ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
47	46	simp2bi	⊢ ( 𝐿 ∈ LMod → 𝐺 ∈ Ring )
48	5 6 8 9	ringpropd	⊢ ( 𝜑 → ( 𝐹 ∈ Ring ↔ 𝐺 ∈ Ring ) )
49	47 48	imbitrrid	⊢ ( 𝜑 → ( 𝐿 ∈ LMod → 𝐹 ∈ Ring ) )
50		simplr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐿 ∈ LMod )
51		simprl	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝑃 )
52	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 = ( Base ‘ 𝐺 ) )
53	51 52	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
54		simprr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
55	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
56	54 55	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐿 ) )
57	39 4 41 42	lmodvscl	⊢ ( ( 𝐿 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) )
58	50 53 56 57	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) )
59	10	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
60	58 59 55	3eltr4d	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
61	60	ralrimivva	⊢ ( ( 𝜑 ∧ 𝐿 ∈ LMod ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
62	61	ex	⊢ ( 𝜑 → ( 𝐿 ∈ LMod → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) )
63	38 49 62	3jcad	⊢ ( 𝜑 → ( 𝐿 ∈ LMod → ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) )
64	37	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )
65	48	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( 𝐹 ∈ Ring ↔ 𝐺 ∈ Ring ) )
66		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝜑 )
67		simprlr	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑟 ∈ 𝑃 )
68		simprrr	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑤 ∈ 𝐵 )
69	10	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
70	66 67 68 69	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
71	70	eleq1d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ) )
72		simplr1	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐾 ∈ Grp )
73	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
74	68 73	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐾 ) )
75		simprrl	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑧 ∈ 𝐵 )
76	75 73	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
77	13 14	grpcl	⊢ ( ( 𝐾 ∈ Grp ∧ 𝑤 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
78	72 74 76 77	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
79	78 73	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 )
80	10	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) )
81	66 67 79 80	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) )
82	7	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) = ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) )
83	66 68 75 82	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) = ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) )
84	83	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) )
85	81 84	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) )
86		simplr3	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
87		ovrspc2v	⊢ ( ( ( 𝑟 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
88	67 68 86 87	syl21anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
89		ovrspc2v	⊢ ( ( ( 𝑟 ∈ 𝑃 ∧ 𝑧 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 )
90	67 75 86 89	syl21anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 )
91	7	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) )
92	66 88 90 91	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) )
93	10	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) )
94	66 67 75 93	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) )
95	70 94	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) )
96	92 95	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) )
97	85 96	eqeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ↔ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ) )
98		simplr2	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐹 ∈ Ring )
99		simprll	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑞 ∈ 𝑃 )
100	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑃 = ( Base ‘ 𝐹 ) )
101	99 100	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑞 ∈ ( Base ‘ 𝐹 ) )
102	67 100	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑟 ∈ ( Base ‘ 𝐹 ) )
103	16 17	ringacl	⊢ ( ( 𝐹 ∈ Ring ∧ 𝑞 ∈ ( Base ‘ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ∈ ( Base ‘ 𝐹 ) )
104	98 101 102 103	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ∈ ( Base ‘ 𝐹 ) )
105	104 100	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ∈ 𝑃 )
106	10	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
107	66 105 68 106	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
108	8	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) = ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) )
109	108	ad2ant2r	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) = ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) )
110	109	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
111	107 110	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
112		ovrspc2v	⊢ ( ( ( 𝑞 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
113	99 68 86 112	syl21anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
114	7	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
115	66 113 88 114	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
116	10	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
117	66 99 68 116	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
118	117 70	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
119	115 118	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
120	111 119	eqeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) )
121	71 97 120	3anbi123d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ) )
122	16 18	ringcl	⊢ ( ( 𝐹 ∈ Ring ∧ 𝑞 ∈ ( Base ‘ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ∈ ( Base ‘ 𝐹 ) )
123	98 101 102 122	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ∈ ( Base ‘ 𝐹 ) )
124	123 100	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ∈ 𝑃 )
125	10	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
126	66 124 68 125	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
127	9	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) = ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) )
128	127	ad2ant2r	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) = ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) )
129	128	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
130	126 129	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
131	10	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑃 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
132	66 99 88 131	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
133	70	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
134	132 133	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
135	130 134	eqeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ↔ ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) )
136	16 19	ringidcl	⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
137	98 136	syl	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
138	137 100	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 1r ‘ 𝐹 ) ∈ 𝑃 )
139	10	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( ( 1r ‘ 𝐹 ) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
140	66 138 68 139	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
141	5 6 9	rngidpropd	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐺 ) )
142	141	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐺 ) )
143	142	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
144	140 143	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
145	144	eqeq1d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ↔ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) )
146	135 145	anbi12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ↔ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) )
147	121 146	anbi12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
148	147	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
149	148	2ralbidva	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
150	149	2ralbidva	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑞 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
151	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → 𝑃 = ( Base ‘ 𝐹 ) )
152	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
153	152	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ) )
154	153	3anbi1d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ) )
155	154	anbi1d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
156	152 155	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
157	152 156	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
158	151 157	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
159	151 158	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑞 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ 𝐹 ) ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
160	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → 𝑃 = ( Base ‘ 𝐺 ) )
161	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
162	161	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ) )
163	162	3anbi1d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ) )
164	163	anbi1d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
165	161 164	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
166	161 165	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
167	160 166	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
168	160 167	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑞 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ 𝐺 ) ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
169	150 159 168	3bitr3d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑞 ∈ ( Base ‘ 𝐹 ) ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ 𝐺 ) ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
170	64 65 169	3anbi123d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ 𝐹 ) ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐿 ∈ Grp ∧ 𝐺 ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ 𝐺 ) ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) ) )
171	170 20 46	3bitr4g	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )
172	171	ex	⊢ ( 𝜑 → ( ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) ) )
173	35 63 172	pm5.21ndd	⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )