rmodislmodlem

Description: Lemma for rmodislmod . This is the part of the proof of rmodislmod which requires the scalar ring to be commutative. (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	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)$

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		simprl	$⊢ ((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{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r$
13	12	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{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r$
14	13	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{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r$
15		ralrot3	$⊢ \forall q \in K \forall r \in K \forall x \in V \forall w \in V w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \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{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r$
16	1	grpbn0	$⊢ R \in Grp \to V \neq \emptyset$
17	16	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$
18	9 17	ax-mp	$⊢ V \neq \emptyset$
19		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{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \to \forall q \in K \forall r \in K \forall w \in V w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r)$
20	18 19	ax-mp	$⊢ \forall x \in V \forall q \in K \forall r \in K \forall w \in V w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \to \forall q \in K \forall r \in K \forall w \in V w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r$
21		oveq1	$⊢ q = b \to q \underset{˙}{\times} r = b \underset{˙}{\times} r$
22	21	oveq2d	$⊢ q = b \to w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = w \underset{˙}{\cdot} (b \underset{˙}{\times} r)$
23		oveq2	$⊢ q = b \to w \underset{˙}{\cdot} q = w \underset{˙}{\cdot} b$
24	23	oveq1d	$⊢ q = b \to (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r = (w \underset{˙}{\cdot} b) \underset{˙}{\cdot} r$
25	22 24	eqeq12d	$⊢ q = b \to (w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \leftrightarrow w \underset{˙}{\cdot} (b \underset{˙}{\times} r) = (w \underset{˙}{\cdot} b) \underset{˙}{\cdot} r)$
26		oveq2	$⊢ r = a \to b \underset{˙}{\times} r = b \underset{˙}{\times} a$
27	26	oveq2d	$⊢ r = a \to w \underset{˙}{\cdot} (b \underset{˙}{\times} r) = w \underset{˙}{\cdot} (b \underset{˙}{\times} a)$
28		oveq2	$⊢ r = a \to (w \underset{˙}{\cdot} b) \underset{˙}{\cdot} r = (w \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
29	27 28	eqeq12d	$⊢ r = a \to (w \underset{˙}{\cdot} (b \underset{˙}{\times} r) = (w \underset{˙}{\cdot} b) \underset{˙}{\cdot} r \leftrightarrow w \underset{˙}{\cdot} (b \underset{˙}{\times} a) = (w \underset{˙}{\cdot} b) \underset{˙}{\cdot} a)$
30		oveq1	$⊢ w = c \to w \underset{˙}{\cdot} (b \underset{˙}{\times} a) = c \underset{˙}{\cdot} (b \underset{˙}{\times} a)$
31		oveq1	$⊢ w = c \to w \underset{˙}{\cdot} b = c \underset{˙}{\cdot} b$
32	31	oveq1d	$⊢ w = c \to (w \underset{˙}{\cdot} b) \underset{˙}{\cdot} a = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
33	30 32	eqeq12d	$⊢ w = c \to (w \underset{˙}{\cdot} (b \underset{˙}{\times} a) = (w \underset{˙}{\cdot} b) \underset{˙}{\cdot} a \leftrightarrow c \underset{˙}{\cdot} (b \underset{˙}{\times} a) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a)$
34	25 29 33	rspc3v	$⊢ (b \in K \land a \in K \land c \in V) \to (\forall q \in K \forall r \in K \forall w \in V w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \to c \underset{˙}{\cdot} (b \underset{˙}{\times} a) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a)$
35	34	3com12	$⊢ (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{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \to c \underset{˙}{\cdot} (b \underset{˙}{\times} a) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a)$
36	20 35	syl5com	$⊢ \forall x \in V \forall q \in K \forall r \in K \forall w \in V w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \to ((a \in K \land b \in K \land c \in V) \to c \underset{˙}{\cdot} (b \underset{˙}{\times} a) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a)$
37	15 36	sylbi	$⊢ \forall q \in K \forall r \in K \forall x \in V \forall w \in V w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \to ((a \in K \land b \in K \land c \in V) \to c \underset{˙}{\cdot} (b \underset{˙}{\times} a) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a)$
38		eqcom	$⊢ (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a = c \underset{˙}{\cdot} (b \underset{˙}{\times} a) \leftrightarrow c \underset{˙}{\cdot} (b \underset{˙}{\times} a) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
39	37 38	syl6ibr	$⊢ \forall q \in K \forall r \in K \forall x \in V \forall w \in V w \underset{˙}{\cdot} (q \underset{˙}{\times} r) = (w \underset{˙}{\cdot} q) \underset{˙}{\cdot} r \to ((a \in K \land b \in K \land c \in V) \to (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a = c \underset{˙}{\cdot} (b \underset{˙}{\times} a))$
40	14 39	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} b) \underset{˙}{\cdot} a = c \underset{˙}{\cdot} (b \underset{˙}{\times} a))$
41	40	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} b) \underset{˙}{\cdot} a = c \underset{˙}{\cdot} (b \underset{˙}{\times} a))$
42	9 41	ax-mp	$⊢ (a \in K \land b \in K \land c \in V) \to (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a = c \underset{˙}{\cdot} (b \underset{˙}{\times} a)$
43	42	adantl	$⊢ (F \in CRing \land (a \in K \land b \in K \land c \in V)) \to (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a = c \underset{˙}{\cdot} (b \underset{˙}{\times} a)$
44	5 7	crngcom	$⊢ (F \in CRing \land b \in K \land a \in K) \to b \underset{˙}{\times} a = a \underset{˙}{\times} b$
45	44	3expb	$⊢ (F \in CRing \land (b \in K \land a \in K)) \to b \underset{˙}{\times} a = a \underset{˙}{\times} b$
46	45	expcom	$⊢ (b \in K \land a \in K) \to (F \in CRing \to b \underset{˙}{\times} a = a \underset{˙}{\times} b)$
47	46	ancoms	$⊢ (a \in K \land b \in K) \to (F \in CRing \to b \underset{˙}{\times} a = a \underset{˙}{\times} b)$
48	47	3adant3	$⊢ (a \in K \land b \in K \land c \in V) \to (F \in CRing \to b \underset{˙}{\times} a = a \underset{˙}{\times} b)$
49	48	impcom	$⊢ (F \in CRing \land (a \in K \land b \in K \land c \in V)) \to b \underset{˙}{\times} a = a \underset{˙}{\times} b$
50	49	oveq2d	$⊢ (F \in CRing \land (a \in K \land b \in K \land c \in V)) \to c \underset{˙}{\cdot} (b \underset{˙}{\times} a) = c \underset{˙}{\cdot} (a \underset{˙}{\times} b)$
51	43 50	eqtrd	$⊢ (F \in CRing \land (a \in K \land b \in K \land c \in V)) \to (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a = c \underset{˙}{\cdot} (a \underset{˙}{\times} b)$
52	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)$
53		oveq12	$⊢ (v = c \land s = b) \to v \underset{˙}{\cdot} s = c \underset{˙}{\cdot} b$
54	53	ancoms	$⊢ (s = b \land v = c) \to v \underset{˙}{\cdot} s = c \underset{˙}{\cdot} b$
55	54	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$
56		simp2	$⊢ (a \in K \land b \in K \land c \in V) \to b \in K$
57		simp3	$⊢ (a \in K \land b \in K \land c \in V) \to c \in V$
58		ovexd	$⊢ (a \in K \land b \in K \land c \in V) \to c \underset{˙}{\cdot} b \in V$
59	52 55 56 57 58	ovmpod	$⊢ (a \in K \land b \in K \land c \in V) \to b \underset{˙}{*} c = c \underset{˙}{\cdot} b$
60	59	oveq2d	$⊢ (a \in K \land b \in K \land c \in V) \to a \underset{˙}{} (b \underset{˙}{} c) = a \underset{˙}{*} (c \underset{˙}{\cdot} b)$
61		oveq12	$⊢ (v = c \underset{˙}{\cdot} b \land s = a) \to v \underset{˙}{\cdot} s = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
62	61	ancoms	$⊢ (s = a \land v = c \underset{˙}{\cdot} b) \to v \underset{˙}{\cdot} s = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
63	62	adantl	$⊢ ((a \in K \land b \in K \land c \in V) \land (s = a \land v = c \underset{˙}{\cdot} b)) \to v \underset{˙}{\cdot} s = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
64		simp1	$⊢ (a \in K \land b \in K \land c \in V) \to a \in K$
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		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)$
77	18 76	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$
78		oveq2	$⊢ r = b \to w \underset{˙}{\cdot} r = w \underset{˙}{\cdot} b$
79	78	eleq1d	$⊢ r = b \to (w \underset{˙}{\cdot} r \in V \leftrightarrow w \underset{˙}{\cdot} b \in V)$
80	31	eleq1d	$⊢ w = c \to (w \underset{˙}{\cdot} b \in V \leftrightarrow c \underset{˙}{\cdot} b \in V)$
81	79 80	rspc2v	$⊢ (b \in K \land c \in V) \to (\forall r \in K \forall w \in V w \underset{˙}{\cdot} r \in V \to c \underset{˙}{\cdot} b \in V)$
82	77 81	syl5com	$⊢ \forall x \in V \forall r \in K \forall w \in V w \underset{˙}{\cdot} r \in V \to ((b \in K \land c \in V) \to c \underset{˙}{\cdot} b \in V)$
83	75 82	sylbi	$⊢ \forall r \in K \forall x \in V \forall w \in V w \underset{˙}{\cdot} r \in V \to ((b \in K \land c \in V) \to c \underset{˙}{\cdot} b \in V)$
84	67 74 83	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 ((b \in K \land c \in V) \to c \underset{˙}{\cdot} b \in V)$
85	84	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 ((b \in K \land c \in V) \to c \underset{˙}{\cdot} b \in V)$
86	9 85	ax-mp	$⊢ (b \in K \land c \in V) \to c \underset{˙}{\cdot} b \in V$
87	86	3adant1	$⊢ (a \in K \land b \in K \land c \in V) \to c \underset{˙}{\cdot} b \in V$
88		ovexd	$⊢ (a \in K \land b \in K \land c \in V) \to (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a \in V$
89	52 63 64 87 88	ovmpod	$⊢ (a \in K \land b \in K \land c \in V) \to a \underset{˙}{*} (c \underset{˙}{\cdot} b) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
90	60 89	eqtrd	$⊢ (a \in K \land b \in K \land c \in V) \to a \underset{˙}{} (b \underset{˙}{} c) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
91	90	adantl	$⊢ (F \in CRing \land (a \in K \land b \in K \land c \in V)) \to a \underset{˙}{} (b \underset{˙}{} c) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} a$
92		oveq12	$⊢ (v = c \land s = a \underset{˙}{\times} b) \to v \underset{˙}{\cdot} s = c \underset{˙}{\cdot} (a \underset{˙}{\times} b)$
93	92	ancoms	$⊢ (s = a \underset{˙}{\times} b \land v = c) \to v \underset{˙}{\cdot} s = c \underset{˙}{\cdot} (a \underset{˙}{\times} b)$
94	93	adantl	$⊢ ((a \in K \land b \in K \land c \in V) \land (s = a \underset{˙}{\times} b \land v = c)) \to v \underset{˙}{\cdot} s = c \underset{˙}{\cdot} (a \underset{˙}{\times} b)$
95	5 7	ringcl	$⊢ (F \in Ring \land a \in K \land b \in K) \to a \underset{˙}{\times} b \in K$
96	95	3expib	$⊢ F \in Ring \to ((a \in K \land b \in K) \to a \underset{˙}{\times} b \in K)$
97	96	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{˙}{\times} b \in K)$
98	9 97	ax-mp	$⊢ (a \in K \land b \in K) \to a \underset{˙}{\times} b \in K$
99	98	3adant3	$⊢ (a \in K \land b \in K \land c \in V) \to a \underset{˙}{\times} b \in K$
100		ovexd	$⊢ (a \in K \land b \in K \land c \in V) \to c \underset{˙}{\cdot} (a \underset{˙}{\times} b) \in V$
101	52 94 99 57 100	ovmpod	$⊢ (a \in K \land b \in K \land c \in V) \to (a \underset{˙}{\times} b) \underset{˙}{*} c = c \underset{˙}{\cdot} (a \underset{˙}{\times} b)$
102	101	adantl	$⊢ (F \in CRing \land (a \in K \land b \in K \land c \in V)) \to (a \underset{˙}{\times} b) \underset{˙}{*} c = c \underset{˙}{\cdot} (a \underset{˙}{\times} b)$
103	51 91 102	3eqtr4rd	$⊢ (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)$

Metamath Proof Explorer

Theorem rmodislmodlem

Proof