Theorem rmodislmodlem 13846

Description: Lemma for rmodislmod 13847. This is the part of the proof of rmodislmod 13847 which requires the scalar ring to be commutative. (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 = (1r‘𝐹)
rmodislmod.r	⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))
rmodislmod.m	⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠))
rmodislmod.l	⊢ 𝐿 = (𝑅 sSet ⟨( ·𝑠 ‘ndx), ∗ ⟩)

Assertion

Ref	Expression
rmodislmodlem	⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑎 ∗ (𝑏 ∗ 𝑐)))

Distinct variable groups:   × ,𝑞,𝑟,𝑤,𝑥   × ,𝑠,𝑣   · ,𝑞,𝑟,𝑤,𝑥   · ,𝑠,𝑣   𝐾,𝑞,𝑟,𝑥   𝐾,𝑠,𝑣   𝑉,𝑞,𝑟,𝑤,𝑥   𝑉,𝑠,𝑣   𝑟,𝑎,𝑤   𝑠,𝑎,𝑣   𝑞,𝑏,𝑟,𝑤   𝑠,𝑏,𝑣   𝑠,𝑐,𝑣   𝑤,𝑐

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

Proof of Theorem rmodislmodlem

Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rmodislmod.r	. . . . 5 ⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))
2		simprl 529	. . . . . . . . 9 ⊢ ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
3	2	2ralimi 2558	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
4	3	2ralimi 2558	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
5		ralrot3 2659	. . . . . . . . 9 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
6	1	simp1i 1008	. . . . . . . . . . . 12 ⊢ 𝑅 ∈ Grp
7		rmodislmod.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (Base‘𝑅)
8		eqid 2193	. . . . . . . . . . . . . 14 ⊢ (0g‘𝑅) = (0g‘𝑅)
9	7, 8	grpidcl 13101	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Grp → (0g‘𝑅) ∈ 𝑉)
10		elex2 2776	. . . . . . . . . . . . 13 ⊢ ((0g‘𝑅) ∈ 𝑉 → ∃𝑗 𝑗 ∈ 𝑉)
11	9, 10	syl 14	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Grp → ∃𝑗 𝑗 ∈ 𝑉)
12		r19.3rmv 3537	. . . . . . . . . . . 12 ⊢ (∃𝑗 𝑗 ∈ 𝑉 → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟)))
13	6, 11, 12	mp2b 8	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
14	13	biimpri 133	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟))
15		oveq1 5925	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑏 → (𝑞 × 𝑟) = (𝑏 × 𝑟))
16	15	oveq2d 5934	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑏 → (𝑤 · (𝑞 × 𝑟)) = (𝑤 · (𝑏 × 𝑟)))
17		oveq2 5926	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑏 → (𝑤 · 𝑞) = (𝑤 · 𝑏))
18	17	oveq1d 5933	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑏 → ((𝑤 · 𝑞) · 𝑟) = ((𝑤 · 𝑏) · 𝑟))
19	16, 18	eqeq12d 2208	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑏 → ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ↔ (𝑤 · (𝑏 × 𝑟)) = ((𝑤 · 𝑏) · 𝑟)))
20		oveq2 5926	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑎 → (𝑏 × 𝑟) = (𝑏 × 𝑎))
21	20	oveq2d 5934	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑎 → (𝑤 · (𝑏 × 𝑟)) = (𝑤 · (𝑏 × 𝑎)))
22		oveq2 5926	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑎 → ((𝑤 · 𝑏) · 𝑟) = ((𝑤 · 𝑏) · 𝑎))
23	21, 22	eqeq12d 2208	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑎 → ((𝑤 · (𝑏 × 𝑟)) = ((𝑤 · 𝑏) · 𝑟) ↔ (𝑤 · (𝑏 × 𝑎)) = ((𝑤 · 𝑏) · 𝑎)))
24		oveq1 5925	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑐 → (𝑤 · (𝑏 × 𝑎)) = (𝑐 · (𝑏 × 𝑎)))
25		oveq1 5925	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑐 → (𝑤 · 𝑏) = (𝑐 · 𝑏))
26	25	oveq1d 5933	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑐 → ((𝑤 · 𝑏) · 𝑎) = ((𝑐 · 𝑏) · 𝑎))
27	24, 26	eqeq12d 2208	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑐 → ((𝑤 · (𝑏 × 𝑎)) = ((𝑤 · 𝑏) · 𝑎) ↔ (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
28	19, 23, 27	rspc3v 2880	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
29	28	3com12 1209	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
30	14, 29	syl5com 29	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
31	5, 30	sylbi 121	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎)))
32		eqcom 2195	. . . . . . . 8 ⊢ (((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)) ↔ (𝑐 · (𝑏 × 𝑎)) = ((𝑐 · 𝑏) · 𝑎))
33	31, 32	imbitrrdi 162	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎))))
34	4, 33	syl 14	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎))))
35	34	3ad2ant3 1022	. . . . 5 ⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎))))
36	1, 35	ax-mp 5	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)))
37	36	adantl 277	. . 3 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑏 × 𝑎)))
38		rmodislmod.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝐹)
39		rmodislmod.t	. . . . . . . . . 10 ⊢ × = (.r‘𝐹)
40	38, 39	crngcom 13510	. . . . . . . . 9 ⊢ ((𝐹 ∈ CRing ∧ 𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾) → (𝑏 × 𝑎) = (𝑎 × 𝑏))
41	40	3expb 1206	. . . . . . . 8 ⊢ ((𝐹 ∈ CRing ∧ (𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾)) → (𝑏 × 𝑎) = (𝑎 × 𝑏))
42	41	expcom 116	. . . . . . 7 ⊢ ((𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏)))
43	42	ancoms 268	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏)))
44	43	3adant3 1019	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝐹 ∈ CRing → (𝑏 × 𝑎) = (𝑎 × 𝑏)))
45	44	impcom 125	. . . 4 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → (𝑏 × 𝑎) = (𝑎 × 𝑏))
46	45	oveq2d 5934	. . 3 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → (𝑐 · (𝑏 × 𝑎)) = (𝑐 · (𝑎 × 𝑏)))
47	37, 46	eqtrd 2226	. 2 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑐 · 𝑏) · 𝑎) = (𝑐 · (𝑎 × 𝑏)))
48		rmodislmod.m	. . . . . . 7 ⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠))
49	48	a1i 9	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)))
50		oveq12 5927	. . . . . . . 8 ⊢ ((𝑣 = 𝑐 ∧ 𝑠 = 𝑏) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
51	50	ancoms 268	. . . . . . 7 ⊢ ((𝑠 = 𝑏 ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
52	51	adantl 277	. . . . . 6 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑏 ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
53		simp2 1000	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑏 ∈ 𝐾)
54		simp3 1001	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉)
55		vex 2763	. . . . . . . 8 ⊢ 𝑐 ∈ V
56		rmodislmod.s	. . . . . . . . 9 ⊢ · = ( ·𝑠 ‘𝑅)
57		vscaslid 12780	. . . . . . . . . . 11 ⊢ ( ·𝑠 = Slot ( ·𝑠 ‘ndx) ∧ ( ·𝑠 ‘ndx) ∈ ℕ)
58	57	slotex 12645	. . . . . . . . . 10 ⊢ (𝑅 ∈ Grp → ( ·𝑠 ‘𝑅) ∈ V)
59	6, 58	ax-mp 5	. . . . . . . . 9 ⊢ ( ·𝑠 ‘𝑅) ∈ V
60	56, 59	eqeltri 2266	. . . . . . . 8 ⊢ · ∈ V
61		vex 2763	. . . . . . . 8 ⊢ 𝑏 ∈ V
62		ovexg 5952	. . . . . . . 8 ⊢ ((𝑐 ∈ V ∧ · ∈ V ∧ 𝑏 ∈ V) → (𝑐 · 𝑏) ∈ V)
63	55, 60, 61, 62	mp3an 1348	. . . . . . 7 ⊢ (𝑐 · 𝑏) ∈ V
64	63	a1i 9	. . . . . 6 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ V)
65	49, 52, 53, 54, 64	ovmpod 6046	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑏 ∗ 𝑐) = (𝑐 · 𝑏))
66	65	oveq2d 5934	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ (𝑏 ∗ 𝑐)) = (𝑎 ∗ (𝑐 · 𝑏)))
67		oveq12 5927	. . . . . . 7 ⊢ ((𝑣 = (𝑐 · 𝑏) ∧ 𝑠 = 𝑎) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎))
68	67	ancoms 268	. . . . . 6 ⊢ ((𝑠 = 𝑎 ∧ 𝑣 = (𝑐 · 𝑏)) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎))
69	68	adantl 277	. . . . 5 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑎 ∧ 𝑣 = (𝑐 · 𝑏))) → (𝑣 · 𝑠) = ((𝑐 · 𝑏) · 𝑎))
70		simp1 999	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → 𝑎 ∈ 𝐾)
71		simpl1 1002	. . . . . . . . . . 11 ⊢ ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · 𝑟) ∈ 𝑉)
72	71	2ralimi 2558	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
73	72	2ralimi 2558	. . . . . . . . 9 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
74	1	simp2i 1009	. . . . . . . . . . . 12 ⊢ 𝐹 ∈ Ring
75		ringgrp 13497	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp)
76		eqid 2193	. . . . . . . . . . . . 13 ⊢ (0g‘𝐹) = (0g‘𝐹)
77	38, 76	grpidcl 13101	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ Grp → (0g‘𝐹) ∈ 𝐾)
78	74, 75, 77	mp2b 8	. . . . . . . . . . 11 ⊢ (0g‘𝐹) ∈ 𝐾
79		elex2 2776	. . . . . . . . . . 11 ⊢ ((0g‘𝐹) ∈ 𝐾 → ∃𝑗 𝑗 ∈ 𝐾)
80		r19.3rmv 3537	. . . . . . . . . . 11 ⊢ (∃𝑗 𝑗 ∈ 𝐾 → (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉))
81	78, 79, 80	mp2b 8	. . . . . . . . . 10 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
82	81	biimpri 133	. . . . . . . . 9 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
83		ralcom 2657	. . . . . . . . . 10 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
84		r19.3rmv 3537	. . . . . . . . . . . . 13 ⊢ (∃𝑗 𝑗 ∈ 𝑉 → (∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉))
85	6, 11, 84	mp2b 8	. . . . . . . . . . . 12 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
86	85	biimpri 133	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉)
87		oveq2 5926	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑏 → (𝑤 · 𝑟) = (𝑤 · 𝑏))
88	87	eleq1d 2262	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑏 → ((𝑤 · 𝑟) ∈ 𝑉 ↔ (𝑤 · 𝑏) ∈ 𝑉))
89	25	eleq1d 2262	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑐 → ((𝑤 · 𝑏) ∈ 𝑉 ↔ (𝑐 · 𝑏) ∈ 𝑉))
90	88, 89	rspc2v 2877	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → (𝑐 · 𝑏) ∈ 𝑉))
91	86, 90	syl5com 29	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑉 ∀𝑟 ∈ 𝐾 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉))
92	83, 91	sylbi 121	. . . . . . . . 9 ⊢ (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉))
93	73, 82, 92	3syl 17	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉))
94	93	3ad2ant3 1022	. . . . . . 7 ⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉))
95	1, 94	ax-mp 5	. . . . . 6 ⊢ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉)
96	95	3adant1 1017	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · 𝑏) ∈ 𝑉)
97		vex 2763	. . . . . . 7 ⊢ 𝑎 ∈ V
98		ovexg 5952	. . . . . . 7 ⊢ (((𝑐 · 𝑏) ∈ V ∧ · ∈ V ∧ 𝑎 ∈ V) → ((𝑐 · 𝑏) · 𝑎) ∈ V)
99	63, 60, 97, 98	mp3an 1348	. . . . . 6 ⊢ ((𝑐 · 𝑏) · 𝑎) ∈ V
100	99	a1i 9	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑐 · 𝑏) · 𝑎) ∈ V)
101	49, 69, 70, 96, 100	ovmpod 6046	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ (𝑐 · 𝑏)) = ((𝑐 · 𝑏) · 𝑎))
102	66, 101	eqtrd 2226	. . 3 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 ∗ (𝑏 ∗ 𝑐)) = ((𝑐 · 𝑏) · 𝑎))
103	102	adantl 277	. 2 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∗ (𝑏 ∗ 𝑐)) = ((𝑐 · 𝑏) · 𝑎))
104		oveq12 5927	. . . . . 6 ⊢ ((𝑣 = 𝑐 ∧ 𝑠 = (𝑎 × 𝑏)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏)))
105	104	ancoms 268	. . . . 5 ⊢ ((𝑠 = (𝑎 × 𝑏) ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏)))
106	105	adantl 277	. . . 4 ⊢ (((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = (𝑎 × 𝑏) ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 × 𝑏)))
107	38, 39	ringcl 13509	. . . . . . . 8 ⊢ ((𝐹 ∈ Ring ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 × 𝑏) ∈ 𝐾)
108	107	3expib 1208	. . . . . . 7 ⊢ (𝐹 ∈ Ring → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 × 𝑏) ∈ 𝐾))
109	108	3ad2ant2 1021	. . . . . 6 ⊢ ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 × 𝑏) ∈ 𝐾))
110	1, 109	ax-mp 5	. . . . 5 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎 × 𝑏) ∈ 𝐾)
111	110	3adant3 1019	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑎 × 𝑏) ∈ 𝐾)
112		mulrslid 12749	. . . . . . . . . 10 ⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
113	112	slotex 12645	. . . . . . . . 9 ⊢ (𝐹 ∈ Ring → (.r‘𝐹) ∈ V)
114	74, 113	ax-mp 5	. . . . . . . 8 ⊢ (.r‘𝐹) ∈ V
115	39, 114	eqeltri 2266	. . . . . . 7 ⊢ × ∈ V
116		ovexg 5952	. . . . . . 7 ⊢ ((𝑎 ∈ V ∧ × ∈ V ∧ 𝑏 ∈ V) → (𝑎 × 𝑏) ∈ V)
117	97, 115, 61, 116	mp3an 1348	. . . . . 6 ⊢ (𝑎 × 𝑏) ∈ V
118		ovexg 5952	. . . . . 6 ⊢ ((𝑐 ∈ V ∧ · ∈ V ∧ (𝑎 × 𝑏) ∈ V) → (𝑐 · (𝑎 × 𝑏)) ∈ V)
119	55, 60, 117, 118	mp3an 1348	. . . . 5 ⊢ (𝑐 · (𝑎 × 𝑏)) ∈ V
120	119	a1i 9	. . . 4 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → (𝑐 · (𝑎 × 𝑏)) ∈ V)
121	49, 106, 111, 54, 120	ovmpod 6046	. . 3 ⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑐 · (𝑎 × 𝑏)))
122	121	adantl 277	. 2 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑐 · (𝑎 × 𝑏)))
123	47, 103, 122	3eqtr4rd 2237	1 ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑎 ∗ (𝑏 ∗ 𝑐)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 980   = wceq 1364  ∃wex 1503   ∈ wcel 2164  ∀wral 2472  Vcvv 2760  ⟨cop 3621  ‘cfv 5254  (class class class)co 5918   ∈ cmpo 5920  ndxcnx 12615   sSet csts 12616  Basecbs 12618  +_gcplusg 12695  ._rcmulr 12696  Scalarcsca 12698   ·_𝑠 cvsca 12699  0_gc0g 12867  Grpcgrp 13072  1_rcur 13455  Ringcrg 13492  CRingccrg 13493

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-addcom 7972  ax-addass 7974  ax-i2m1 7977  ax-0lt1 7978  ax-0id 7980  ax-rnegex 7981  ax-pre-ltirr 7984  ax-pre-ltadd 7988

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-iota 5215  df-fun 5256  df-fn 5257  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-pnf 8056  df-mnf 8057  df-ltxr 8059  df-inn 8983  df-2 9041  df-3 9042  df-4 9043  df-5 9044  df-6 9045  df-ndx 12621  df-slot 12622  df-base 12624  df-sets 12625  df-plusg 12708  df-mulr 12709  df-vsca 12712  df-0g 12869  df-mgm 12939  df-sgrp 12985  df-mnd 12998  df-grp 13075  df-cmn 13356  df-mgp 13417  df-ring 13494  df-cring 13495

This theorem is referenced by:  rmodislmod  13847