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)

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

Metamath Proof Explorer

Theorem rmodislmod

Proof