rmodislmod - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rmodislmod		Structured version Visualization version GIF version

Theorem rmodislmod 19702

Description: The right module 𝑅 induces a left module 𝐿 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 the definition df-lmod 19636 of a left module, see also islmod 19638. (Contributed by AV, 3-Dec-2021.)

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

**Assertion**
Ref	Expression
rmodislmod	⊢ (𝐹 ∈ CRing → 𝐿 ∈ LMod)

Distinct variable groups: × ,𝑞,𝑟,𝑤,𝑥 × ,𝑠,𝑣 · ,𝑞,𝑟,𝑤,𝑥 · ,𝑠,𝑣 𝐾,𝑞,𝑟,𝑥 𝐾,𝑠,𝑣 𝑉,𝑞,𝑟,𝑤,𝑥 𝑉,𝑠,𝑣 𝐹,𝑠,𝑣 1 ,𝑠,𝑣 1 ,𝑞,𝑟,𝑤,𝑥 + ,𝑞,𝑟,𝑤,𝑥 + ,𝑠,𝑣 ⨣ ,𝑞,𝑟,𝑤,𝑥 ⨣ ,𝑠,𝑣 Allowed substitution hints: 𝑅(𝑥,𝑤,𝑣,𝑠,𝑟,𝑞) 𝐹(𝑥,𝑤,𝑟,𝑞) ∗ (𝑥,𝑤,𝑣,𝑠,𝑟,𝑞) 𝐾(𝑤) 𝐿(𝑥,𝑤,𝑣,𝑠,𝑟,𝑞)

Proof of Theorem rmodislmod Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ≠ wne 3016 ∀wral 3138 Vcvv 3494 ∅c0 4291 ⟨cop 4573 ‘cfv 6355 (class class class)co 7156 ∈ cmpo 7158 1c1 10538 2c2 11693 5c5 11696 6c6 11697 ndxcnx 16480 sSet csts 16481 Basecbs 16483 +_gcplusg 16565 ._rcmulr 16566 Scalarcsca 16568 ·_𝑠 cvsca 16569 Grpcgrp 18103 1_rcur 19251 Ringcrg 19297 CRingccrg 19298 LModclmod 19634

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-er 8289 df-en 8510 df-dom 8511 df-sdom 8512 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-plusg 16578 df-sca 16581 df-vsca 16582 df-0g 16715 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-grp 18106 df-cmn 18908 df-mgp 19240 df-ur 19252 df-ring 19299 df-cring 19300 df-lmod 19636

This theorem is referenced by: (None)

W3C validator