Theorem rmodislmodOLD

Description: Obsolete version of rmodislmod as of 18-Oct-2024. The right module R induces a left module L by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod of a left module, see also islmod . (Contributed by AV, 3-Dec-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rmodislmod.v	⊢ 𝑉 = ( Base ‘ 𝑅 )
	rmodislmod.a	⊢ + = ( +g ‘ 𝑅 )
	rmodislmod.s	⊢ · = ( ·𝑠 ‘ 𝑅 )
	rmodislmod.f	⊢ 𝐹 = ( Scalar ‘ 𝑅 )
	rmodislmod.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	rmodislmod.p	⊢ ⨣ = ( +g ‘ 𝐹 )
	rmodislmod.t	⊢ × = ( .r ‘ 𝐹 )
	rmodislmod.u	⊢ 1 = ( 1r ‘ 𝐹 )
	rmodislmod.r	⊢ ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) )
	rmodislmod.m	⊢ ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) )
	rmodislmod.l	⊢ 𝐿 = ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ )
Assertion	rmodislmodOLD	⊢ ( 𝐹 ∈ CRing → 𝐿 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		rmodislmod.v	⊢ 𝑉 = ( Base ‘ 𝑅 )
2		rmodislmod.a	⊢ + = ( +g ‘ 𝑅 )
3		rmodislmod.s	⊢ · = ( ·𝑠 ‘ 𝑅 )
4		rmodislmod.f	⊢ 𝐹 = ( Scalar ‘ 𝑅 )
5		rmodislmod.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		rmodislmod.p	⊢ ⨣ = ( +g ‘ 𝐹 )
7		rmodislmod.t	⊢ × = ( .r ‘ 𝐹 )
8		rmodislmod.u	⊢ 1 = ( 1r ‘ 𝐹 )
9		rmodislmod.r	⊢ ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) )
10		rmodislmod.m	⊢ ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) )
11		rmodislmod.l	⊢ 𝐿 = ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ )
12		baseid	⊢ Base = Slot ( Base ‘ ndx )
13		df-base	⊢ Base = Slot 1
14		1nn	⊢ 1 ∈ ℕ
15	13 14	ndxarg	⊢ ( Base ‘ ndx ) = 1
16		1re	⊢ 1 ∈ ℝ
17		1lt6	⊢ 1 < 6
18	16 17	ltneii	⊢ 1 ≠ 6
19		vscandx	⊢ ( ·𝑠 ‘ ndx ) = 6
20	18 19	neeqtrri	⊢ 1 ≠ ( ·𝑠 ‘ ndx )
21	15 20	eqnetri	⊢ ( Base ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
22	12 21	setsnid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
23	1 22	eqtri	⊢ 𝑉 = ( Base ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
24	11	eqcomi	⊢ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) = 𝐿
25	24	fveq2i	⊢ ( Base ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) ) = ( Base ‘ 𝐿 )
26	23 25	eqtri	⊢ 𝑉 = ( Base ‘ 𝐿 )
27	26	a1i	⊢ ( 𝐹 ∈ CRing → 𝑉 = ( Base ‘ 𝐿 ) )
28		plusgid	⊢ +g = Slot ( +g ‘ ndx )
29		plusgndx	⊢ ( +g ‘ ndx ) = 2
30		2re	⊢ 2 ∈ ℝ
31		2lt6	⊢ 2 < 6
32	30 31	ltneii	⊢ 2 ≠ 6
33	32 19	neeqtrri	⊢ 2 ≠ ( ·𝑠 ‘ ndx )
34	29 33	eqnetri	⊢ ( +g ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
35	28 34	setsnid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
36	11	fveq2i	⊢ ( +g ‘ 𝐿 ) = ( +g ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
37	35 2 36	3eqtr4i	⊢ + = ( +g ‘ 𝐿 )
38	37	a1i	⊢ ( 𝐹 ∈ CRing → + = ( +g ‘ 𝐿 ) )
39		scaid	⊢ Scalar = Slot ( Scalar ‘ ndx )
40		scandx	⊢ ( Scalar ‘ ndx ) = 5
41		5re	⊢ 5 ∈ ℝ
42		5lt6	⊢ 5 < 6
43	41 42	ltneii	⊢ 5 ≠ 6
44	43 19	neeqtrri	⊢ 5 ≠ ( ·𝑠 ‘ ndx )
45	40 44	eqnetri	⊢ ( Scalar ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
46	39 45	setsnid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
47	11	fveq2i	⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
48	46 4 47	3eqtr4i	⊢ 𝐹 = ( Scalar ‘ 𝐿 )
49	48	a1i	⊢ ( 𝐹 ∈ CRing → 𝐹 = ( Scalar ‘ 𝐿 ) )
50	9	simp1i	⊢ 𝑅 ∈ Grp
51	5	fvexi	⊢ 𝐾 ∈ V
52	1	fvexi	⊢ 𝑉 ∈ V
53	10	mpoexg	⊢ ( ( 𝐾 ∈ V ∧ 𝑉 ∈ V ) → ∗ ∈ V )
54	51 52 53	mp2an	⊢ ∗ ∈ V
55		vscaid	⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )
56	55	setsid	⊢ ( ( 𝑅 ∈ Grp ∧ ∗ ∈ V ) → ∗ = ( ·𝑠 ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) ) )
57	50 54 56	mp2an	⊢ ∗ = ( ·𝑠 ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
58	24	fveq2i	⊢ ( ·𝑠 ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) ) = ( ·𝑠 ‘ 𝐿 )
59	57 58	eqtri	⊢ ∗ = ( ·𝑠 ‘ 𝐿 )
60	59	a1i	⊢ ( 𝐹 ∈ CRing → ∗ = ( ·𝑠 ‘ 𝐿 ) )
61	5	a1i	⊢ ( 𝐹 ∈ CRing → 𝐾 = ( Base ‘ 𝐹 ) )
62	6	a1i	⊢ ( 𝐹 ∈ CRing → ⨣ = ( +g ‘ 𝐹 ) )
63	7	a1i	⊢ ( 𝐹 ∈ CRing → × = ( .r ‘ 𝐹 ) )
64	8	a1i	⊢ ( 𝐹 ∈ CRing → 1 = ( 1r ‘ 𝐹 ) )
65		crngring	⊢ ( 𝐹 ∈ CRing → 𝐹 ∈ Ring )
66	1	eqcomi	⊢ ( Base ‘ 𝑅 ) = 𝑉
67	66 26	eqtri	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐿 )
68	35 36	eqtr4i	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝐿 )
69	67 68	grpprop	⊢ ( 𝑅 ∈ Grp ↔ 𝐿 ∈ Grp )
70	50 69	mpbi	⊢ 𝐿 ∈ Grp
71	70	a1i	⊢ ( 𝐹 ∈ CRing → 𝐿 ∈ Grp )
72	10	a1i	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
73		oveq12	⊢ ( ( 𝑣 = 𝑏 ∧ 𝑠 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( 𝑏 · 𝑎 ) )
74	73	ancoms	⊢ ( ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( 𝑣 · 𝑠 ) = ( 𝑏 · 𝑎 ) )
75	74	adantl	⊢ ( ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑏 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑏 · 𝑎 ) )
76		simp2	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → 𝑎 ∈ 𝐾 )
77		simp3	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
78		ovexd	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ V )
79	72 75 76 77 78	ovmpod	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑏 ) = ( 𝑏 · 𝑎 ) )
80		simpl1	⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( 𝑤 · 𝑟 ) ∈ 𝑉 )
81	80	2ralimi	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
82	81	2ralimi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
83		ringgrp	⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
84	5	grpbn0	⊢ ( 𝐹 ∈ Grp → 𝐾 ≠ ∅ )
85	83 84	syl	⊢ ( 𝐹 ∈ Ring → 𝐾 ≠ ∅ )
86	85	3ad2ant2	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → 𝐾 ≠ ∅ )
87	9 86	ax-mp	⊢ 𝐾 ≠ ∅
88		rspn0	⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ) )
89	87 88	ax-mp	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
90		ralcom	⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
91	1	grpbn0	⊢ ( 𝑅 ∈ Grp → 𝑉 ≠ ∅ )
92	91	3ad2ant1	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → 𝑉 ≠ ∅ )
93	9 92	ax-mp	⊢ 𝑉 ≠ ∅
94		rspn0	⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ) )
95	93 94	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
96		oveq2	⊢ ( 𝑟 = 𝑎 → ( 𝑤 · 𝑟 ) = ( 𝑤 · 𝑎 ) )
97	96	eleq1d	⊢ ( 𝑟 = 𝑎 → ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ↔ ( 𝑤 · 𝑎 ) ∈ 𝑉 ) )
98		oveq1	⊢ ( 𝑤 = 𝑏 → ( 𝑤 · 𝑎 ) = ( 𝑏 · 𝑎 ) )
99	98	eleq1d	⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 · 𝑎 ) ∈ 𝑉 ↔ ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
100	97 99	rspc2v	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
101	100	3adant1	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
102	95 101	syl5com	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
103	90 102	sylbi	⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
104	82 89 103	3syl	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
105	104	3ad2ant3	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
106	9 105	ax-mp	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 )
107	79 106	eqeltrd	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑏 ) ∈ 𝑉 )
108	10	a1i	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
109		oveq12	⊢ ( ( 𝑣 = ( 𝑏 + 𝑐 ) ∧ 𝑠 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
110	109	ancoms	⊢ ( ( 𝑠 = 𝑎 ∧ 𝑣 = ( 𝑏 + 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
111	110	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = ( 𝑏 + 𝑐 ) ) ) → ( 𝑣 · 𝑠 ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
112		simp1	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → 𝑎 ∈ 𝐾 )
113	1 2	grpcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 + 𝑐 ) ∈ 𝑉 )
114	50 113	mp3an1	⊢ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 + 𝑐 ) ∈ 𝑉 )
115	114	3adant1	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 + 𝑐 ) ∈ 𝑉 )
116		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) ∈ V )
117	108 111 112 115 116	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ ( 𝑏 + 𝑐 ) ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
118		simpl2	⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) )
119	118	2ralimi	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) )
120	119	2ralimi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) )
121		rspn0	⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ) )
122	87 121	ax-mp	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) )
123		oveq2	⊢ ( 𝑟 = 𝑎 → ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 + 𝑥 ) · 𝑎 ) )
124		oveq2	⊢ ( 𝑟 = 𝑎 → ( 𝑥 · 𝑟 ) = ( 𝑥 · 𝑎 ) )
125	96 124	oveq12d	⊢ ( 𝑟 = 𝑎 → ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑥 · 𝑎 ) ) )
126	123 125	eqeq12d	⊢ ( 𝑟 = 𝑎 → ( ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ↔ ( ( 𝑤 + 𝑥 ) · 𝑎 ) = ( ( 𝑤 · 𝑎 ) + ( 𝑥 · 𝑎 ) ) ) )
127		oveq2	⊢ ( 𝑥 = 𝑐 → ( 𝑤 + 𝑥 ) = ( 𝑤 + 𝑐 ) )
128	127	oveq1d	⊢ ( 𝑥 = 𝑐 → ( ( 𝑤 + 𝑥 ) · 𝑎 ) = ( ( 𝑤 + 𝑐 ) · 𝑎 ) )
129		oveq1	⊢ ( 𝑥 = 𝑐 → ( 𝑥 · 𝑎 ) = ( 𝑐 · 𝑎 ) )
130	129	oveq2d	⊢ ( 𝑥 = 𝑐 → ( ( 𝑤 · 𝑎 ) + ( 𝑥 · 𝑎 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
131	128 130	eqeq12d	⊢ ( 𝑥 = 𝑐 → ( ( ( 𝑤 + 𝑥 ) · 𝑎 ) = ( ( 𝑤 · 𝑎 ) + ( 𝑥 · 𝑎 ) ) ↔ ( ( 𝑤 + 𝑐 ) · 𝑎 ) = ( ( 𝑤 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
132		oveq1	⊢ ( 𝑤 = 𝑏 → ( 𝑤 + 𝑐 ) = ( 𝑏 + 𝑐 ) )
133	132	oveq1d	⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
134	98	oveq1d	⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
135	133 134	eqeq12d	⊢ ( 𝑤 = 𝑏 → ( ( ( 𝑤 + 𝑐 ) · 𝑎 ) = ( ( 𝑤 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ↔ ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
136	126 131 135	rspc3v	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
137	136	3com23	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
138	122 137	syl5com	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
139	120 138	syl	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
140	139	3ad2ant3	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
141	9 140	ax-mp	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
142	117 141	eqtrd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ ( 𝑏 + 𝑐 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
143	142	adantl	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑎 ∗ ( 𝑏 + 𝑐 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
144	74	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑏 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑏 · 𝑎 ) )
145		simp2	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
146		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ V )
147	108 144 112 145 146	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑏 ) = ( 𝑏 · 𝑎 ) )
148		oveq12	⊢ ( ( 𝑣 = 𝑐 ∧ 𝑠 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑎 ) )
149	148	ancoms	⊢ ( ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑐 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑎 ) )
150	149	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑎 ) )
151		simp3	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → 𝑐 ∈ 𝑉 )
152		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑎 ) ∈ V )
153	108 150 112 151 152	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑐 ) = ( 𝑐 · 𝑎 ) )
154	147 153	oveq12d	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ∗ 𝑏 ) + ( 𝑎 ∗ 𝑐 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
155	154	adantl	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 ∗ 𝑏 ) + ( 𝑎 ∗ 𝑐 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
156	143 155	eqtr4d	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑎 ∗ ( 𝑏 + 𝑐 ) ) = ( ( 𝑎 ∗ 𝑏 ) + ( 𝑎 ∗ 𝑐 ) ) )
157		simpl3	⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
158	157	2ralimi	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
159	158	2ralimi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
160		ralrot3	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
161		rspn0	⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) )
162	93 161	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
163		oveq1	⊢ ( 𝑞 = 𝑎 → ( 𝑞 ⨣ 𝑟 ) = ( 𝑎 ⨣ 𝑟 ) )
164	163	oveq2d	⊢ ( 𝑞 = 𝑎 → ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( 𝑤 · ( 𝑎 ⨣ 𝑟 ) ) )
165		oveq2	⊢ ( 𝑞 = 𝑎 → ( 𝑤 · 𝑞 ) = ( 𝑤 · 𝑎 ) )
166	165	oveq1d	⊢ ( 𝑞 = 𝑎 → ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑟 ) ) )
167	164 166	eqeq12d	⊢ ( 𝑞 = 𝑎 → ( ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ↔ ( 𝑤 · ( 𝑎 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑟 ) ) ) )
168		oveq2	⊢ ( 𝑟 = 𝑏 → ( 𝑎 ⨣ 𝑟 ) = ( 𝑎 ⨣ 𝑏 ) )
169	168	oveq2d	⊢ ( 𝑟 = 𝑏 → ( 𝑤 · ( 𝑎 ⨣ 𝑟 ) ) = ( 𝑤 · ( 𝑎 ⨣ 𝑏 ) ) )
170		oveq2	⊢ ( 𝑟 = 𝑏 → ( 𝑤 · 𝑟 ) = ( 𝑤 · 𝑏 ) )
171	170	oveq2d	⊢ ( 𝑟 = 𝑏 → ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑏 ) ) )
172	169 171	eqeq12d	⊢ ( 𝑟 = 𝑏 → ( ( 𝑤 · ( 𝑎 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑟 ) ) ↔ ( 𝑤 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑏 ) ) ) )
173		oveq1	⊢ ( 𝑤 = 𝑐 → ( 𝑤 · ( 𝑎 ⨣ 𝑏 ) ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
174		oveq1	⊢ ( 𝑤 = 𝑐 → ( 𝑤 · 𝑎 ) = ( 𝑐 · 𝑎 ) )
175		oveq1	⊢ ( 𝑤 = 𝑐 → ( 𝑤 · 𝑏 ) = ( 𝑐 · 𝑏 ) )
176	174 175	oveq12d	⊢ ( 𝑤 = 𝑐 → ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) )
177	173 176	eqeq12d	⊢ ( 𝑤 = 𝑐 → ( ( 𝑤 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑏 ) ) ↔ ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
178	167 172 177	rspc3v	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
179	162 178	syl5com	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
180	160 179	sylbi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
181	159 180	syl	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
182	181	3ad2ant3	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
183	9 182	ax-mp	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) )
184	10	a1i	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
185		oveq12	⊢ ( ( 𝑣 = 𝑐 ∧ 𝑠 = ( 𝑎 ⨣ 𝑏 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
186	185	ancoms	⊢ ( ( 𝑠 = ( 𝑎 ⨣ 𝑏 ) ∧ 𝑣 = 𝑐 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
187	186	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = ( 𝑎 ⨣ 𝑏 ) ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
188	5 6	grpcl	⊢ ( ( 𝐹 ∈ Grp ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 )
189	188	3expib	⊢ ( 𝐹 ∈ Grp → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 ) )
190	83 189	syl	⊢ ( 𝐹 ∈ Ring → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 ) )
191	190	3ad2ant2	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 ) )
192	9 191	ax-mp	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 )
193	192	3adant3	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 )
194		simp3	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑐 ∈ 𝑉 )
195		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) ∈ V )
196	184 187 193 194 195	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ⨣ 𝑏 ) ∗ 𝑐 ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
197	149	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑎 ) )
198		simp1	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑎 ∈ 𝐾 )
199		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑎 ) ∈ V )
200	184 197 198 194 199	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑐 ) = ( 𝑐 · 𝑎 ) )
201		oveq12	⊢ ( ( 𝑣 = 𝑐 ∧ 𝑠 = 𝑏 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
202	201	ancoms	⊢ ( ( 𝑠 = 𝑏 ∧ 𝑣 = 𝑐 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
203	202	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑏 ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
204		simp2	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑏 ∈ 𝐾 )
205		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ V )
206	184 203 204 194 205	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 ∗ 𝑐 ) = ( 𝑐 · 𝑏 ) )
207	200 206	oveq12d	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ∗ 𝑐 ) + ( 𝑏 ∗ 𝑐 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) )
208	183 196 207	3eqtr4d	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ⨣ 𝑏 ) ∗ 𝑐 ) = ( ( 𝑎 ∗ 𝑐 ) + ( 𝑏 ∗ 𝑐 ) ) )
209	208	adantl	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 ⨣ 𝑏 ) ∗ 𝑐 ) = ( ( 𝑎 ∗ 𝑐 ) + ( 𝑏 ∗ 𝑐 ) ) )
210	1 2 3 4 5 6 7 8 9 10 11	rmodislmodlem	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 × 𝑏 ) ∗ 𝑐 ) = ( 𝑎 ∗ ( 𝑏 ∗ 𝑐 ) ) )
211	10	a1i	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
212		oveq12	⊢ ( ( 𝑣 = 𝑎 ∧ 𝑠 = 1 ) → ( 𝑣 · 𝑠 ) = ( 𝑎 · 1 ) )
213	212	ancoms	⊢ ( ( 𝑠 = 1 ∧ 𝑣 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( 𝑎 · 1 ) )
214	213	adantl	⊢ ( ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑠 = 1 ∧ 𝑣 = 𝑎 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑎 · 1 ) )
215	5 8	ringidcl	⊢ ( 𝐹 ∈ Ring → 1 ∈ 𝐾 )
216	65 215	syl	⊢ ( 𝐹 ∈ CRing → 1 ∈ 𝐾 )
217	216	adantr	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → 1 ∈ 𝐾 )
218		simpr	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
219		ovexd	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) ∈ V )
220	211 214 217 218 219	ovmpod	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 1 ∗ 𝑎 ) = ( 𝑎 · 1 ) )
221		simprr	⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( 𝑤 · 1 ) = 𝑤 )
222	221	2ralimi	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
223	222	2ralimi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
224		rspn0	⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 ) )
225	87 224	ax-mp	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
226		rspn0	⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 ) )
227	87 226	ax-mp	⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
228		rspn0	⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 ) )
229	93 228	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
230		oveq1	⊢ ( 𝑤 = 𝑎 → ( 𝑤 · 1 ) = ( 𝑎 · 1 ) )
231		id	⊢ ( 𝑤 = 𝑎 → 𝑤 = 𝑎 )
232	230 231	eqeq12d	⊢ ( 𝑤 = 𝑎 → ( ( 𝑤 · 1 ) = 𝑤 ↔ ( 𝑎 · 1 ) = 𝑎 ) )
233	232	rspcv	⊢ ( 𝑎 ∈ 𝑉 → ( ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ( 𝑎 · 1 ) = 𝑎 ) )
234	233	adantl	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ( 𝑎 · 1 ) = 𝑎 ) )
235	229 234	syl5com	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 ) )
236	227 235	syl	⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 ) )
237	223 225 236	3syl	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 ) )
238	237	3ad2ant3	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 ) )
239	9 238	ax-mp	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 )
240	220 239	eqtrd	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 1 ∗ 𝑎 ) = 𝑎 )
241	27 38 49 60 61 62 63 64 65 71 107 156 209 210 240	islmodd	⊢ ( 𝐹 ∈ CRing → 𝐿 ∈ LMod )