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	$⊢ V = {Base}_{R}$
	rmodislmod.a	$⊢ \underset{˙}{+} = +_{R}$
	rmodislmod.s	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rmodislmod.f	$⊢ F = Scalar (R)$
	rmodislmod.k	$⊢ K = {Base}_{F}$
	rmodislmod.p	$⊢ \underset{˙}{⨣} = +_{F}$
	rmodislmod.t	$⊢ \underset{˙}{\times} = \cdot_{F}$
	rmodislmod.u	$⊢ \underset{˙}{1} = 1_{F}$
	rmodislmod.r	$⊢ (R \in Grp \land F \in Ring \land \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((w \underset{˙}{\cdot} r \in V \land (w \underset{˙}{+} x) \underset{˙}{\cdot} r = (w \underset{˙}{\cdot} r) \underset{˙}{+} (x \underset{˙}{\cdot} r) \land w \underset{˙}{\cdot} (q \underset{˙}{⨣} r) = (w \underset{˙}{\cdot} q) \underset{˙}{+} (w \underset{˙}{\cdot} r)) \land (w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \land w \underset{˙}{\cdot} \underset{˙}{1} = w)))$
	rmodislmod.m	$⊢ \underset{˙}{*} = (s \in K, v \in V ⟼ v \underset{˙}{\cdot} s)$
	rmodislmod.l	$⊢ L = R sSet ⟨\cdot_{ndx}, \underset{˙}{*}⟩$
Assertion	rmodislmod	$⊢ F \in CRing \to L \in LMod$

Proof

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

Metamath Proof Explorer

Theorem rmodislmod

Proof