rmodislmod - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > rmodislmod		GIF version

Theorem rmodislmod 14336

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 Definition df-lmod 14274 of a left module, see also islmod 14276. (Contributed by AV, 3-Dec-2021.) (Proof shortened by AV, 18-Oct-2024.)

**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		rmodislmod.r	. . . . . . 7 ⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))
3	2	simp1i 1030	. . . . . 6 ⊢ 𝑅 ∈ Grp
4		rmodislmod.k	. . . . . . . 8 ⊢ 𝐾 = (Base‘𝐹)
5		basfn 13112	. . . . . . . . 9 ⊢ Base Fn V
6	2	simp2i 1031	. . . . . . . . . 10 ⊢ 𝐹 ∈ Ring
7	6	elexi 2812	. . . . . . . . 9 ⊢ 𝐹 ∈ V
8		funfvex 5649	. . . . . . . . . 10 ⊢ ((Fun Base ∧ 𝐹 ∈ dom Base) → (Base‘𝐹) ∈ V)
9	8	funfni 5426	. . . . . . . . 9 ⊢ ((Base Fn V ∧ 𝐹 ∈ V) → (Base‘𝐹) ∈ V)
10	5, 7, 9	mp2an 426	. . . . . . . 8 ⊢ (Base‘𝐹) ∈ V
11	4, 10	eqeltri 2302	. . . . . . 7 ⊢ 𝐾 ∈ V
12	3	elexi 2812	. . . . . . . . 9 ⊢ 𝑅 ∈ V
13		funfvex 5649	. . . . . . . . . 10 ⊢ ((Fun Base ∧ 𝑅 ∈ dom Base) → (Base‘𝑅) ∈ V)
14	13	funfni 5426	. . . . . . . . 9 ⊢ ((Base Fn V ∧ 𝑅 ∈ V) → (Base‘𝑅) ∈ V)
15	5, 12, 14	mp2an 426	. . . . . . . 8 ⊢ (Base‘𝑅) ∈ V
16	1, 15	eqeltri 2302	. . . . . . 7 ⊢ 𝑉 ∈ V
17		rmodislmod.m	. . . . . . . 8 ⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠))
18	17	mpoexg 6368	. . . . . . 7 ⊢ ((𝐾 ∈ V ∧ 𝑉 ∈ V) → ∗ ∈ V)
19	11, 16, 18	mp2an 426	. . . . . 6 ⊢ ∗ ∈ V
20		baseslid 13111	. . . . . . 7 ⊢ (Base = Slot (Base‘ndx) ∧ (Base‘ndx) ∈ ℕ)
21		vscandxnbasendx 13213	. . . . . . . 8 ⊢ ( ·_𝑠 ‘ndx) ≠ (Base‘ndx)
22	21	necomi 2485	. . . . . . 7 ⊢ (Base‘ndx) ≠ ( ·_𝑠 ‘ndx)
23		vscaslid 13217	. . . . . . . 8 ⊢ ( ·_𝑠 = Slot ( ·_𝑠 ‘ndx) ∧ ( ·_𝑠 ‘ndx) ∈ ℕ)
24	23	simpri 113	. . . . . . 7 ⊢ ( ·_𝑠 ‘ndx) ∈ ℕ
25	20, 22, 24	setsslnid 13105	. . . . . 6 ⊢ ((𝑅 ∈ Grp ∧ ∗ ∈ V) → (Base‘𝑅) = (Base‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩)))
26	3, 19, 25	mp2an 426	. . . . 5 ⊢ (Base‘𝑅) = (Base‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩))
27	1, 26	eqtri 2250	. . . 4 ⊢ 𝑉 = (Base‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩))
28		rmodislmod.l	. . . . . 6 ⊢ 𝐿 = (𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩)
29	28	eqcomi 2233	. . . . 5 ⊢ (𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩) = 𝐿
30	29	fveq2i 5635	. . . 4 ⊢ (Base‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩)) = (Base‘𝐿)
31	27, 30	eqtri 2250	. . 3 ⊢ 𝑉 = (Base‘𝐿)
32	31	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → 𝑉 = (Base‘𝐿))
33		plusgslid 13166	. . . . . 6 ⊢ (+_g = Slot (+_g‘ndx) ∧ (+_g‘ndx) ∈ ℕ)
34		vscandxnplusgndx 13214	. . . . . . 7 ⊢ ( ·_𝑠 ‘ndx) ≠ (+_g‘ndx)
35	34	necomi 2485	. . . . . 6 ⊢ (+_g‘ndx) ≠ ( ·_𝑠 ‘ndx)
36	33, 35, 24	setsslnid 13105	. . . . 5 ⊢ ((𝑅 ∈ Grp ∧ ∗ ∈ V) → (+_g‘𝑅) = (+_g‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩)))
37	3, 19, 36	mp2an 426	. . . 4 ⊢ (+_g‘𝑅) = (+_g‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩))
38		rmodislmod.a	. . . 4 ⊢ + = (+_g‘𝑅)
39	28	fveq2i 5635	. . . 4 ⊢ (+_g‘𝐿) = (+_g‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩))
40	37, 38, 39	3eqtr4i 2260	. . 3 ⊢ + = (+_g‘𝐿)
41	40	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → + = (+_g‘𝐿))
42		scaslid 13207	. . . . . 6 ⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ)
43		vscandxnscandx 13216	. . . . . . 7 ⊢ ( ·_𝑠 ‘ndx) ≠ (Scalar‘ndx)
44	43	necomi 2485	. . . . . 6 ⊢ (Scalar‘ndx) ≠ ( ·_𝑠 ‘ndx)
45	42, 44, 24	setsslnid 13105	. . . . 5 ⊢ ((𝑅 ∈ Grp ∧ ∗ ∈ V) → (Scalar‘𝑅) = (Scalar‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩)))
46	3, 19, 45	mp2an 426	. . . 4 ⊢ (Scalar‘𝑅) = (Scalar‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩))
47		rmodislmod.f	. . . 4 ⊢ 𝐹 = (Scalar‘𝑅)
48	28	fveq2i 5635	. . . 4 ⊢ (Scalar‘𝐿) = (Scalar‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩))
49	46, 47, 48	3eqtr4i 2260	. . 3 ⊢ 𝐹 = (Scalar‘𝐿)
50	49	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → 𝐹 = (Scalar‘𝐿))
51	23	setsslid 13104	. . . . 5 ⊢ ((𝑅 ∈ Grp ∧ ∗ ∈ V) → ∗ = ( ·_𝑠 ‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩)))
52	3, 19, 51	mp2an 426	. . . 4 ⊢ ∗ = ( ·_𝑠 ‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩))
53	29	fveq2i 5635	. . . 4 ⊢ ( ·_𝑠 ‘(𝑅 sSet ⟨( ·_𝑠 ‘ndx), ∗ ⟩)) = ( ·_𝑠 ‘𝐿)
54	52, 53	eqtri 2250	. . 3 ⊢ ∗ = ( ·_𝑠 ‘𝐿)
55	54	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → ∗ = ( ·_𝑠 ‘𝐿))
56	4	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → 𝐾 = (Base‘𝐹))
57		rmodislmod.p	. . 3 ⊢ ⨣ = (+_g‘𝐹)
58	57	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → ⨣ = (+_g‘𝐹))
59		rmodislmod.t	. . 3 ⊢ × = (._r‘𝐹)
60	59	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → × = (._r‘𝐹))
61		rmodislmod.u	. . 3 ⊢ 1 = (1_r‘𝐹)
62	61	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → 1 = (1_r‘𝐹))
63		crngring 13992	. 2 ⊢ (𝐹 ∈ CRing → 𝐹 ∈ Ring)
64	1	eqcomi 2233	. . . . . 6 ⊢ (Base‘𝑅) = 𝑉
65	64, 31	eqtri 2250	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝐿)
66	37, 39	eqtr4i 2253	. . . . 5 ⊢ (+_g‘𝑅) = (+_g‘𝐿)
67	65, 66	grpprop 13572	. . . 4 ⊢ (𝑅 ∈ Grp ↔ 𝐿 ∈ Grp)
68	3, 67	mpbi 145	. . 3 ⊢ 𝐿 ∈ Grp
69	68	a1i 9	. 2 ⊢ (𝐹 ∈ CRing → 𝐿 ∈ Grp)
70	17	a1i 9	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)))
71		oveq12 6019	. . . . . 6 ⊢ ((𝑣 = 𝑏 ∧ 𝑠 = 𝑎) → (𝑣 · 𝑠) = (𝑏 · 𝑎))
72	71	ancoms 268	. . . . 5 ⊢ ((𝑠 = 𝑎 ∧ 𝑣 = 𝑏) → (𝑣 · 𝑠) = (𝑏 · 𝑎))
73	72	adantl 277	. . . 4 ⊢ (((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) ∧ (𝑠 = 𝑎 ∧ 𝑣 = 𝑏)) → (𝑣 · 𝑠) = (𝑏 · 𝑎))
74		simp2 1022	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → 𝑎 ∈ 𝐾)
75		simp3 1023	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉)
76		vex 2802	. . . . . 6 ⊢ 𝑏 ∈ V
77		rmodislmod.s	. . . . . . 7 ⊢ · = ( ·_𝑠 ‘𝑅)
78	23	slotex 13080	. . . . . . . 8 ⊢ (𝑅 ∈ Grp → ( ·_𝑠 ‘𝑅) ∈ V)
79	3, 78	ax-mp 5	. . . . . . 7 ⊢ ( ·_𝑠 ‘𝑅) ∈ V
80	77, 79	eqeltri 2302	. . . . . 6 ⊢ · ∈ V
81		vex 2802	. . . . . 6 ⊢ 𝑎 ∈ V
82		ovexg 6044	. . . . . 6 ⊢ ((𝑏 ∈ V ∧ · ∈ V ∧ 𝑎 ∈ V) → (𝑏 · 𝑎) ∈ V)
83	76, 80, 81, 82	mp3an 1371	. . . . 5 ⊢ (𝑏 · 𝑎) ∈ V
84	83	a1i 9	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (𝑏 · 𝑎) ∈ V)
85	70, 73, 74, 75, 84	ovmpod 6141	. . 3 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (𝑎 ∗ 𝑏) = (𝑏 · 𝑎))
86		simpl1 1024	. . . . . . . 8 ⊢ ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · 𝑟) ∈ 𝑉)
87	86	2ralimi 2594	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
88	87	2ralimi 2594	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
89	4, 61	ringidcl 14004	. . . . . . . . . 10 ⊢ (𝐹 ∈ Ring → 1 ∈ 𝐾)
90		elex2 2816	. . . . . . . . . 10 ⊢ ( 1 ∈ 𝐾 → ∃𝑗 𝑗 ∈ 𝐾)
91	89, 90	syl 14	. . . . . . . . 9 ⊢ (𝐹 ∈ Ring → ∃𝑗 𝑗 ∈ 𝐾)
92	6, 91	ax-mp 5	. . . . . . . 8 ⊢ ∃𝑗 𝑗 ∈ 𝐾
93		r19.3rmv 3582	. . . . . . . 8 ⊢ (∃𝑗 𝑗 ∈ 𝐾 → (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉))
94	92, 93	ax-mp 5	. . . . . . 7 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
95	94	biimpri 133	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
96		ralcom 2694	. . . . . . 7 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
97		eqid 2229	. . . . . . . . . . . . 13 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
98	1, 97	grpidcl 13583	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Grp → (0_g‘𝑅) ∈ 𝑉)
99	3, 98	ax-mp 5	. . . . . . . . . . 11 ⊢ (0_g‘𝑅) ∈ 𝑉
100		elex2 2816	. . . . . . . . . . 11 ⊢ ((0_g‘𝑅) ∈ 𝑉 → ∃𝑗 𝑗 ∈ 𝑉)
101	99, 100	ax-mp 5	. . . . . . . . . 10 ⊢ ∃𝑗 𝑗 ∈ 𝑉
102		r19.3rmv 3582	. . . . . . . . . 10 ⊢ (∃𝑗 𝑗 ∈ 𝑉 → (∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉))
103	101, 102	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
104	103	biimpri 133	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
105		oveq2 6018	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑎 → (𝑤 · 𝑟) = (𝑤 · 𝑎))
106	105	eleq1d 2298	. . . . . . . . . 10 ⊢ (𝑟 = 𝑎 → ((𝑤 · 𝑟) ∈ 𝑉 ↔ (𝑤 · 𝑎) ∈ 𝑉))
107		oveq1 6017	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑏 → (𝑤 · 𝑎) = (𝑏 · 𝑎))
108	107	eleq1d 2298	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → ((𝑤 · 𝑎) ∈ 𝑉 ↔ (𝑏 · 𝑎) ∈ 𝑉))
109	106, 108	rspc2v 2920	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → (𝑏 · 𝑎) ∈ 𝑉))
110	109	3adant1 1039	. . . . . . . 8 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → (𝑏 · 𝑎) ∈ 𝑉))
111	104, 110	syl5com 29	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (𝑏 · 𝑎) ∈ 𝑉))
112	96, 111	sylbi 121	. . . . . 6 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (𝑏 · 𝑎) ∈ 𝑉))
113	88, 95, 112	3syl 17	. . . . 5 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (𝑏 · 𝑎) ∈ 𝑉))
114	113	3ad2ant3 1044	. . . 4 ⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (𝑏 · 𝑎) ∈ 𝑉))
115	2, 114	ax-mp 5	. . 3 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (𝑏 · 𝑎) ∈ 𝑉)
116	85, 115	eqeltrd 2306	. 2 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) → (𝑎 ∗ 𝑏) ∈ 𝑉)
117	17	a1i 9	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)))
118		oveq12 6019	. . . . . . . 8 ⊢ ((𝑣 = (𝑏 + 𝑐) ∧ 𝑠 = 𝑎) → (𝑣 · 𝑠) = ((𝑏 + 𝑐) · 𝑎))
119	118	ancoms 268	. . . . . . 7 ⊢ ((𝑠 = 𝑎 ∧ 𝑣 = (𝑏 + 𝑐)) → (𝑣 · 𝑠) = ((𝑏 + 𝑐) · 𝑎))
120	119	adantl 277	. . . . . 6 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑎 ∧ 𝑣 = (𝑏 + 𝑐))) → (𝑣 · 𝑠) = ((𝑏 + 𝑐) · 𝑎))
121		simp1 1021	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 𝑎 ∈ 𝐾)
122	1, 38	grpcl 13562	. . . . . . . 8 ⊢ ((𝑅 ∈ Grp ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑏 + 𝑐) ∈ 𝑉)
123	3, 122	mp3an1 1358	. . . . . . 7 ⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑏 + 𝑐) ∈ 𝑉)
124	123	3adant1 1039	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑏 + 𝑐) ∈ 𝑉)
125	33	slotex 13080	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Grp → (+_g‘𝑅) ∈ V)
126	3, 125	ax-mp 5	. . . . . . . . . 10 ⊢ (+_g‘𝑅) ∈ V
127	38, 126	eqeltri 2302	. . . . . . . . 9 ⊢ + ∈ V
128		vex 2802	. . . . . . . . 9 ⊢ 𝑐 ∈ V
129		ovexg 6044	. . . . . . . . 9 ⊢ ((𝑏 ∈ V ∧ + ∈ V ∧ 𝑐 ∈ V) → (𝑏 + 𝑐) ∈ V)
130	76, 127, 128, 129	mp3an 1371	. . . . . . . 8 ⊢ (𝑏 + 𝑐) ∈ V
131		ovexg 6044	. . . . . . . 8 ⊢ (((𝑏 + 𝑐) ∈ V ∧ · ∈ V ∧ 𝑎 ∈ V) → ((𝑏 + 𝑐) · 𝑎) ∈ V)
132	130, 80, 81, 131	mp3an 1371	. . . . . . 7 ⊢ ((𝑏 + 𝑐) · 𝑎) ∈ V
133	132	a1i 9	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑏 + 𝑐) · 𝑎) ∈ V)
134	117, 120, 121, 124, 133	ovmpod 6141	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ (𝑏 + 𝑐)) = ((𝑏 + 𝑐) · 𝑎))
135		simpl2 1025	. . . . . . . . . 10 ⊢ ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
136	135	2ralimi 2594	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
137	136	2ralimi 2594	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
138		r19.3rmv 3582	. . . . . . . . . . 11 ⊢ (∃𝑗 𝑗 ∈ 𝐾 → (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟))))
139	92, 138	ax-mp 5	. . . . . . . . . 10 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
140	139	biimpri 133	. . . . . . . . 9 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
141		oveq2 6018	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑎 → ((𝑤 + 𝑥) · 𝑟) = ((𝑤 + 𝑥) · 𝑎))
142		oveq2 6018	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑎 → (𝑥 · 𝑟) = (𝑥 · 𝑎))
143	105, 142	oveq12d 6028	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑎 → ((𝑤 · 𝑟) + (𝑥 · 𝑟)) = ((𝑤 · 𝑎) + (𝑥 · 𝑎)))
144	141, 143	eqeq12d 2244	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑎 → (((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ↔ ((𝑤 + 𝑥) · 𝑎) = ((𝑤 · 𝑎) + (𝑥 · 𝑎))))
145		oveq2 6018	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑐 → (𝑤 + 𝑥) = (𝑤 + 𝑐))
146	145	oveq1d 6025	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑐 → ((𝑤 + 𝑥) · 𝑎) = ((𝑤 + 𝑐) · 𝑎))
147		oveq1 6017	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑐 → (𝑥 · 𝑎) = (𝑐 · 𝑎))
148	147	oveq2d 6026	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑐 → ((𝑤 · 𝑎) + (𝑥 · 𝑎)) = ((𝑤 · 𝑎) + (𝑐 · 𝑎)))
149	146, 148	eqeq12d 2244	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑐 → (((𝑤 + 𝑥) · 𝑎) = ((𝑤 · 𝑎) + (𝑥 · 𝑎)) ↔ ((𝑤 + 𝑐) · 𝑎) = ((𝑤 · 𝑎) + (𝑐 · 𝑎))))
150		oveq1 6017	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑏 → (𝑤 + 𝑐) = (𝑏 + 𝑐))
151	150	oveq1d 6025	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑏 → ((𝑤 + 𝑐) · 𝑎) = ((𝑏 + 𝑐) · 𝑎))
152	107	oveq1d 6025	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑏 → ((𝑤 · 𝑎) + (𝑐 · 𝑎)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
153	151, 152	eqeq12d 2244	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑏 → (((𝑤 + 𝑐) · 𝑎) = ((𝑤 · 𝑎) + (𝑐 · 𝑎)) ↔ ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
154	144, 149, 153	rspc3v 2923	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
155	154	3com23 1233	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
156	140, 155	syl5com 29	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
157	137, 156	syl 14	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
158	157	3ad2ant3 1044	. . . . . 6 ⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
159	2, 158	ax-mp 5	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
160	134, 159	eqtrd 2262	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ (𝑏 + 𝑐)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
161	160	adantl 277	. . 3 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∗ (𝑏 + 𝑐)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
162	72	adantl 277	. . . . . 6 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑎 ∧ 𝑣 = 𝑏)) → (𝑣 · 𝑠) = (𝑏 · 𝑎))
163		simp2 1022	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 𝑏 ∈ 𝑉)
164	83	a1i 9	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑏 · 𝑎) ∈ V)
165	117, 162, 121, 163, 164	ovmpod 6141	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ 𝑏) = (𝑏 · 𝑎))
166		oveq12 6019	. . . . . . . 8 ⊢ ((𝑣 = 𝑐 ∧ 𝑠 = 𝑎) → (𝑣 · 𝑠) = (𝑐 · 𝑎))
167	166	ancoms 268	. . . . . . 7 ⊢ ((𝑠 = 𝑎 ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · 𝑎))
168	167	adantl 277	. . . . . 6 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑎 ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑎))
169		simp3 1023	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉)
170		ovexg 6044	. . . . . . . 8 ⊢ ((𝑐 ∈ V ∧ · ∈ V ∧ 𝑎 ∈ V) → (𝑐 · 𝑎) ∈ V)
171	128, 80, 81, 170	mp3an 1371	. . . . . . 7 ⊢ (𝑐 · 𝑎) ∈ V
172	171	a1i 9	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑎) ∈ V)
173	117, 168, 121, 169, 172	ovmpod 6141	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ 𝑐) = (𝑐 · 𝑎))
174	165, 173	oveq12d 6028	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑎 ∗ 𝑏) + (𝑎 ∗ 𝑐)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
175	174	adantl 277	. . 3 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 ∗ 𝑏) + (𝑎 ∗ 𝑐)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
176	161, 175	eqtr4d 2265	. 2 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∗ (𝑏 + 𝑐)) = ((𝑎 ∗ 𝑏) + (𝑎 ∗ 𝑐)))
177		simpl3 1026	. . . . . . . . 9 ⊢ ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
178	177	2ralimi 2594	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
179	178	2ralimi 2594	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
180		ralrot3 2696	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
181		r19.3rmv 3582	. . . . . . . . . . 11 ⊢ (∃𝑗 𝑗 ∈ 𝑉 → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))))
182	101, 181	ax-mp 5	. . . . . . . . . 10 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
183	182	biimpri 133	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
184		oveq1 6017	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑎 → (𝑞 ⨣ 𝑟) = (𝑎 ⨣ 𝑟))
185	184	oveq2d 6026	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑎 → (𝑤 · (𝑞 ⨣ 𝑟)) = (𝑤 · (𝑎 ⨣ 𝑟)))
186		oveq2 6018	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑎 → (𝑤 · 𝑞) = (𝑤 · 𝑎))
187	186	oveq1d 6025	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑎 → ((𝑤 · 𝑞) + (𝑤 · 𝑟)) = ((𝑤 · 𝑎) + (𝑤 · 𝑟)))
188	185, 187	eqeq12d 2244	. . . . . . . . . 10 ⊢ (𝑞 = 𝑎 → ((𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) ↔ (𝑤 · (𝑎 ⨣ 𝑟)) = ((𝑤 · 𝑎) + (𝑤 · 𝑟))))
189		oveq2 6018	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑏 → (𝑎 ⨣ 𝑟) = (𝑎 ⨣ 𝑏))
190	189	oveq2d 6026	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑏 → (𝑤 · (𝑎 ⨣ 𝑟)) = (𝑤 · (𝑎 ⨣ 𝑏)))
191		oveq2 6018	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑏 → (𝑤 · 𝑟) = (𝑤 · 𝑏))
192	191	oveq2d 6026	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑏 → ((𝑤 · 𝑎) + (𝑤 · 𝑟)) = ((𝑤 · 𝑎) + (𝑤 · 𝑏)))
193	190, 192	eqeq12d 2244	. . . . . . . . . 10 ⊢ (𝑟 = 𝑏 → ((𝑤 · (𝑎 ⨣ 𝑟)) = ((𝑤 · 𝑎) + (𝑤 · 𝑟)) ↔ (𝑤 · (𝑎 ⨣ 𝑏)) = ((𝑤 · 𝑎) + (𝑤 · 𝑏))))
194		oveq1 6017	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑐 → (𝑤 · (𝑎 ⨣ 𝑏)) = (𝑐 · (𝑎 ⨣ 𝑏)))
195		oveq1 6017	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑐 → (𝑤 · 𝑎) = (𝑐 · 𝑎))
196		oveq1 6017	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑐 → (𝑤 · 𝑏) = (𝑐 · 𝑏))
197	195, 196	oveq12d 6028	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑐 → ((𝑤 · 𝑎) + (𝑤 · 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏)))
198	194, 197	eqeq12d 2244	. . . . . . . . . 10 ⊢ (𝑤 = 𝑐 → ((𝑤 · (𝑎 ⨣ 𝑏)) = ((𝑤 · 𝑎) + (𝑤 · 𝑏)) ↔ (𝑐 · (𝑎 ⨣ 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
199	188, 193, 198	rspc3v 2923	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → (𝑐 · (𝑎 ⨣ 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
200	183, 199	syl5com 29	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑎 ⨣ 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
201	180, 200	sylbi 121	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑎 ⨣ 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
202	179, 201	syl 14	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑎 ⨣ 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
203	202	3ad2ant3 1044	. . . . 5 ⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑎 ⨣ 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
204	2, 203	ax-mp 5	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑎 ⨣ 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏)))
205	17	a1i 9	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)))
206		oveq12 6019	. . . . . . 7 ⊢ ((𝑣 = 𝑐 ∧ 𝑠 = (𝑎 ⨣ 𝑏)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 ⨣ 𝑏)))
207	206	ancoms 268	. . . . . 6 ⊢ ((𝑠 = (𝑎 ⨣ 𝑏) ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · (𝑎 ⨣ 𝑏)))
208	207	adantl 277	. . . . 5 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = (𝑎 ⨣ 𝑏) ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 ⨣ 𝑏)))
209		ringgrp 13985	. . . . . . . . 9 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp)
210	4, 57	grpcl 13562	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Grp ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 ⨣ 𝑏) ∈ 𝐾)
211	210	3expib 1230	. . . . . . . . 9 ⊢ (𝐹 ∈ Grp → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 ⨣ 𝑏) ∈ 𝐾))
212	209, 211	syl 14	. . . . . . . 8 ⊢ (𝐹 ∈ Ring → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 ⨣ 𝑏) ∈ 𝐾))
213	212	3ad2ant2 1043	. . . . . . 7 ⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 ⨣ 𝑏) ∈ 𝐾))
214	2, 213	ax-mp 5	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 ⨣ 𝑏) ∈ 𝐾)
215	214	3adant3 1041	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 ⨣ 𝑏) ∈ 𝐾)
216		simp3 1023	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉)
217	33	slotex 13080	. . . . . . . . . 10 ⊢ (𝐹 ∈ Ring → (+_g‘𝐹) ∈ V)
218	6, 217	ax-mp 5	. . . . . . . . 9 ⊢ (+_g‘𝐹) ∈ V
219	57, 218	eqeltri 2302	. . . . . . . 8 ⊢ ⨣ ∈ V
220		ovexg 6044	. . . . . . . 8 ⊢ ((𝑎 ∈ V ∧ ⨣ ∈ V ∧ 𝑏 ∈ V) → (𝑎 ⨣ 𝑏) ∈ V)
221	81, 219, 76, 220	mp3an 1371	. . . . . . 7 ⊢ (𝑎 ⨣ 𝑏) ∈ V
222		ovexg 6044	. . . . . . 7 ⊢ ((𝑐 ∈ V ∧ · ∈ V ∧ (𝑎 ⨣ 𝑏) ∈ V) → (𝑐 · (𝑎 ⨣ 𝑏)) ∈ V)
223	128, 80, 221, 222	mp3an 1371	. . . . . 6 ⊢ (𝑐 · (𝑎 ⨣ 𝑏)) ∈ V
224	223	a1i 9	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑎 ⨣ 𝑏)) ∈ V)
225	205, 208, 215, 216, 224	ovmpod 6141	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑎 ⨣ 𝑏) ∗ 𝑐) = (𝑐 · (𝑎 ⨣ 𝑏)))
226	167	adantl 277	. . . . . 6 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑎 ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑎))
227		simp1 1021	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑎 ∈ 𝐾)
228	171	a1i 9	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑎) ∈ V)
229	205, 226, 227, 216, 228	ovmpod 6141	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ 𝑐) = (𝑐 · 𝑎))
230		oveq12 6019	. . . . . . . 8 ⊢ ((𝑣 = 𝑐 ∧ 𝑠 = 𝑏) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
231	230	ancoms 268	. . . . . . 7 ⊢ ((𝑠 = 𝑏 ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
232	231	adantl 277	. . . . . 6 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑏 ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
233		simp2 1022	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑏 ∈ 𝐾)
234		ovexg 6044	. . . . . . . 8 ⊢ ((𝑐 ∈ V ∧ · ∈ V ∧ 𝑏 ∈ V) → (𝑐 · 𝑏) ∈ V)
235	128, 80, 76, 234	mp3an 1371	. . . . . . 7 ⊢ (𝑐 · 𝑏) ∈ V
236	235	a1i 9	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ V)
237	205, 232, 233, 216, 236	ovmpod 6141	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑏 ∗ 𝑐) = (𝑐 · 𝑏))
238	229, 237	oveq12d 6028	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑎 ∗ 𝑐) + (𝑏 ∗ 𝑐)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏)))
239	204, 225, 238	3eqtr4d 2272	. . 3 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑎 ⨣ 𝑏) ∗ 𝑐) = ((𝑎 ∗ 𝑐) + (𝑏 ∗ 𝑐)))
240	239	adantl 277	. 2 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 ⨣ 𝑏) ∗ 𝑐) = ((𝑎 ∗ 𝑐) + (𝑏 ∗ 𝑐)))
241	1, 38, 77, 47, 4, 57, 59, 61, 2, 17, 28	rmodislmodlem 14335	. 2 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑎 ∗ (𝑏 ∗ 𝑐)))
242	17	a1i 9	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)))
243		oveq12 6019	. . . . . 6 ⊢ ((𝑣 = 𝑎 ∧ 𝑠 = 1 ) → (𝑣 · 𝑠) = (𝑎 · 1 ))
244	243	ancoms 268	. . . . 5 ⊢ ((𝑠 = 1 ∧ 𝑣 = 𝑎) → (𝑣 · 𝑠) = (𝑎 · 1 ))
245	244	adantl 277	. . . 4 ⊢ (((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) ∧ (𝑠 = 1 ∧ 𝑣 = 𝑎)) → (𝑣 · 𝑠) = (𝑎 · 1 ))
246	63, 89	syl 14	. . . . 5 ⊢ (𝐹 ∈ CRing → 1 ∈ 𝐾)
247	246	adantr 276	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → 1 ∈ 𝐾)
248		simpr 110	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉)
249	6, 89	ax-mp 5	. . . . . 6 ⊢ 1 ∈ 𝐾
250		ovexg 6044	. . . . . 6 ⊢ ((𝑎 ∈ V ∧ · ∈ V ∧ 1 ∈ 𝐾) → (𝑎 · 1 ) ∈ V)
251	81, 80, 249, 250	mp3an 1371	. . . . 5 ⊢ (𝑎 · 1 ) ∈ V
252	251	a1i 9	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → (𝑎 · 1 ) ∈ V)
253	242, 245, 247, 248, 252	ovmpod 6141	. . 3 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → ( 1 ∗ 𝑎) = (𝑎 · 1 ))
254		simprr 531	. . . . . . . 8 ⊢ ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · 1 ) = 𝑤)
255	254	2ralimi 2594	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤)
256	255	2ralimi 2594	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤)
257		r19.3rmv 3582	. . . . . . . 8 ⊢ (∃𝑗 𝑗 ∈ 𝐾 → (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤))
258	92, 257	ax-mp 5	. . . . . . 7 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤)
259	258	biimpri 133	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 → ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤)
260		r19.3rmv 3582	. . . . . . . 8 ⊢ (∃𝑗 𝑗 ∈ 𝐾 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 ↔ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤))
261	92, 260	ax-mp 5	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 ↔ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤)
262		r19.3rmv 3582	. . . . . . . . . 10 ⊢ (∃𝑗 𝑗 ∈ 𝑉 → (∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤))
263	101, 262	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤)
264	263	biimpri 133	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 → ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤)
265		oveq1 6017	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑎 → (𝑤 · 1 ) = (𝑎 · 1 ))
266		id 19	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑎 → 𝑤 = 𝑎)
267	265, 266	eqeq12d 2244	. . . . . . . . . 10 ⊢ (𝑤 = 𝑎 → ((𝑤 · 1 ) = 𝑤 ↔ (𝑎 · 1 ) = 𝑎))
268	267	rspcv 2903	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝑉 → (∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 → (𝑎 · 1 ) = 𝑎))
269	268	adantl 277	. . . . . . . 8 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → (∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 → (𝑎 · 1 ) = 𝑎))
270	264, 269	syl5com 29	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 → ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → (𝑎 · 1 ) = 𝑎))
271	261, 270	sylbir 135	. . . . . 6 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 1 ) = 𝑤 → ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → (𝑎 · 1 ) = 𝑎))
272	256, 259, 271	3syl 17	. . . . 5 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → (𝑎 · 1 ) = 𝑎))
273	272	3ad2ant3 1044	. . . 4 ⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → (𝑎 · 1 ) = 𝑎))
274	2, 273	ax-mp 5	. . 3 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → (𝑎 · 1 ) = 𝑎)
275	253, 274	eqtrd 2262	. 2 ⊢ ((𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉) → ( 1 ∗ 𝑎) = 𝑎)
276	32, 41, 50, 55, 56, 58, 60, 62, 63, 69, 116, 176, 240, 241, 275	islmodd 14278	1 ⊢ (𝐹 ∈ CRing → 𝐿 ∈ LMod)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1002 = wceq 1395 ∃wex 1538 ∈ wcel 2200 ∀wral 2508 Vcvv 2799 ⟨cop 3669 Fn wfn 5316 ‘cfv 5321 (class class class)co 6010 ∈ cmpo 6012 ℕcn 9126 ndxcnx 13050 sSet csts 13051 Slot cslot 13052 Basecbs 13053 +_gcplusg 13131 ._rcmulr 13132 Scalarcsca 13134 ·_𝑠 cvsca 13135 0_gc0g 13310 Grpcgrp 13554 1_rcur 13943 Ringcrg 13980 CRingccrg 13981 LModclmod 14272

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-pow 4259 ax-pr 4294 ax-un 4525 ax-setind 4630 ax-cnex 8106 ax-resscn 8107 ax-1cn 8108 ax-1re 8109 ax-icn 8110 ax-addcl 8111 ax-addrcl 8112 ax-mulcl 8113 ax-addcom 8115 ax-addass 8117 ax-i2m1 8120 ax-0lt1 8121 ax-0id 8123 ax-rnegex 8124 ax-pre-ltirr 8127 ax-pre-lttrn 8129 ax-pre-ltadd 8131

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-id 4385 df-xp 4726 df-rel 4727 df-cnv 4728 df-co 4729 df-dm 4730 df-rn 4731 df-res 4732 df-ima 4733 df-iota 5281 df-fun 5323 df-fn 5324 df-f 5325 df-f1 5326 df-fo 5327 df-f1o 5328 df-fv 5329 df-riota 5963 df-ov 6013 df-oprab 6014 df-mpo 6015 df-1st 6295 df-2nd 6296 df-pnf 8199 df-mnf 8200 df-ltxr 8202 df-inn 9127 df-2 9185 df-3 9186 df-4 9187 df-5 9188 df-6 9189 df-ndx 13056 df-slot 13057 df-base 13059 df-sets 13060 df-plusg 13144 df-mulr 13145 df-sca 13147 df-vsca 13148 df-0g 13312 df-mgm 13410 df-sgrp 13456 df-mnd 13471 df-grp 13557 df-cmn 13844 df-mgp 13905 df-ur 13944 df-ring 13982 df-cring 13983 df-lmod 14274

This theorem is referenced by: (None)

W3C validator