Theorem rmodislmod

Description: 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 shortened by AV, 18-Oct-2024)

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