islmodd - Metamath Proof Explorer

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

Theorem islmodd 20044

Description: Properties that determine a left module. See note in isgrpd2 18514 regarding the 𝜑 on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.)

**Hypotheses**
Ref	Expression
islmodd.v	⊢ (𝜑 → 𝑉 = (Base‘𝑊))
islmodd.a	⊢ (𝜑 → + = (+_g‘𝑊))
islmodd.f	⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))
islmodd.s	⊢ (𝜑 → · = ( ·_𝑠 ‘𝑊))
islmodd.b	⊢ (𝜑 → 𝐵 = (Base‘𝐹))
islmodd.p	⊢ (𝜑 → ⨣ = (+_g‘𝐹))
islmodd.t	⊢ (𝜑 → × = (._r‘𝐹))
islmodd.u	⊢ (𝜑 → 1 = (1_r‘𝐹))
islmodd.r	⊢ (𝜑 → 𝐹 ∈ Ring)
islmodd.l	⊢ (𝜑 → 𝑊 ∈ Grp)
islmodd.w	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉) → (𝑥 · 𝑦) ∈ 𝑉)
islmodd.c	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
islmodd.d	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
islmodd.e	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
islmodd.g	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 1 · 𝑥) = 𝑥)

**Assertion**
Ref	Expression
islmodd	⊢ (𝜑 → 𝑊 ∈ LMod)

Distinct variable groups: 𝑦,𝑧, ⨣ 𝑥,𝑦,𝑧,𝐵 𝜑,𝑥,𝑦,𝑧 𝑥,𝑉,𝑦,𝑧 𝑥, + ,𝑦,𝑧 𝑥,𝑊 𝑥, · ,𝑦,𝑧 𝑦, × ,𝑧 𝑥, 1 Allowed substitution hints: ⨣ (𝑥) × (𝑥) 1 (𝑦,𝑧) 𝐹(𝑥,𝑦,𝑧) 𝑊(𝑦,𝑧)

Proof of Theorem islmodd Dummy variables 𝑢 𝑟 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		islmodd.l	. 2 ⊢ (𝜑 → 𝑊 ∈ Grp)
2		islmodd.f	. . 3 ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))
3		islmodd.r	. . 3 ⊢ (𝜑 → 𝐹 ∈ Ring)
4	2, 3	eqeltrrd 2840	. 2 ⊢ (𝜑 → (Scalar‘𝑊) ∈ Ring)
5		islmodd.w	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉) → (𝑥 · 𝑦) ∈ 𝑉)
6	5	3expb 1118	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉)) → (𝑥 · 𝑦) ∈ 𝑉)
7	6	ralrimivva 3114	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉)
8		oveq1 7262	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑟 → (𝑥 · 𝑦) = (𝑟 · 𝑦))
9	8	eleq1d 2823	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑟 → ((𝑥 · 𝑦) ∈ 𝑉 ↔ (𝑟 · 𝑦) ∈ 𝑉))
10		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (𝑟 · 𝑦) = (𝑟 · 𝑤))
11	10	eleq1d 2823	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ((𝑟 · 𝑦) ∈ 𝑉 ↔ (𝑟 · 𝑤) ∈ 𝑉))
12	9, 11	rspc2v 3562	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉 → (𝑟 · 𝑤) ∈ 𝑉))
13	12	ad2ant2l 742	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉 → (𝑟 · 𝑤) ∈ 𝑉))
14	7, 13	mpan9 506	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (𝑟 · 𝑤) ∈ 𝑉)
15		islmodd.c	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
16	15	ralrimivvva 3115	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
17		oveq1 7262	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (𝑥 · (𝑦 + 𝑧)) = (𝑟 · (𝑦 + 𝑧)))
18		oveq1 7262	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑥 · 𝑧) = (𝑟 · 𝑧))
19	8, 18	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → ((𝑥 · 𝑦) + (𝑥 · 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧)))
20	17, 19	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ↔ (𝑟 · (𝑦 + 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧))))
21		oveq1 7262	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → (𝑦 + 𝑧) = (𝑤 + 𝑧))
22	21	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝑟 · (𝑦 + 𝑧)) = (𝑟 · (𝑤 + 𝑧)))
23	10	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → ((𝑟 · 𝑦) + (𝑟 · 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧)))
24	22, 23	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝑟 · (𝑦 + 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧)) ↔ (𝑟 · (𝑤 + 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧))))
25		oveq2 7263	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝑤 + 𝑧) = (𝑤 + 𝑢))
26	25	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝑟 · (𝑤 + 𝑧)) = (𝑟 · (𝑤 + 𝑢)))
27		oveq2 7263	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝑟 · 𝑧) = (𝑟 · 𝑢))
28	27	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → ((𝑟 · 𝑤) + (𝑟 · 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)))
29	26, 28	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → ((𝑟 · (𝑤 + 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧)) ↔ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
30	20, 24, 29	rspc3v 3565	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉 ∧ 𝑢 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
31	30	3com23 1124	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
32	31	3expb 1118	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
33	32	adantll 710	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
34	16, 33	mpan9 506	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)))
35		simpll 763	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → 𝑥 ∈ 𝐵)
36		islmodd.d	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
37	36	3exp2 1352	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝑉 → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
38	37	imp43 427	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
39	38	ralrimivva 3114	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
40	35, 39	sylan2 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
41		simprlr 776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → 𝑟 ∈ 𝐵)
42		simprrr 778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → 𝑤 ∈ 𝑉)
43		oveq2 7263	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑟 → (𝑥 ⨣ 𝑦) = (𝑥 ⨣ 𝑟))
44	43	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 ⨣ 𝑟) · 𝑧))
45		oveq1 7262	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑟 → (𝑦 · 𝑧) = (𝑟 · 𝑧))
46	45	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = ((𝑥 · 𝑧) + (𝑟 · 𝑧)))
47	44, 46	eqeq12d 2754	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) ↔ ((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 · 𝑧) + (𝑟 · 𝑧))))
48		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 ⨣ 𝑟) · 𝑤))
49		oveq2 7263	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑥 · 𝑧) = (𝑥 · 𝑤))
50		oveq2 7263	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑟 · 𝑧) = (𝑟 · 𝑤))
51	49, 50	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑥 · 𝑧) + (𝑟 · 𝑧)) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)))
52	48, 51	eqeq12d 2754	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 · 𝑧) + (𝑟 · 𝑧)) ↔ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
53	47, 52	rspc2v 3562	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
54	41, 42, 53	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
55	40, 54	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)))
56	14, 34, 55	3jca 1126	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
57		islmodd.e	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
58	57	3exp2 1352	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝑉 → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))))))
59	58	imp43 427	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
60	59	ralrimivva 3114	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
61	35, 60	sylan2 592	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
62		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → (𝑥 × 𝑦) = (𝑥 × 𝑟))
63	62	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → ((𝑥 × 𝑦) · 𝑧) = ((𝑥 × 𝑟) · 𝑧))
64	45	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑥 · (𝑦 · 𝑧)) = (𝑥 · (𝑟 · 𝑧)))
65	63, 64	eqeq12d 2754	. . . . . . . . . 10 ⊢ (𝑦 = 𝑟 → (((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) ↔ ((𝑥 × 𝑟) · 𝑧) = (𝑥 · (𝑟 · 𝑧))))
66		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → ((𝑥 × 𝑟) · 𝑧) = ((𝑥 × 𝑟) · 𝑤))
67	50	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (𝑥 · (𝑟 · 𝑧)) = (𝑥 · (𝑟 · 𝑤)))
68	66, 67	eqeq12d 2754	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (((𝑥 × 𝑟) · 𝑧) = (𝑥 · (𝑟 · 𝑧)) ↔ ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
69	65, 68	rspc2v 3562	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
70	41, 42, 69	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
71	61, 70	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)))
72		islmodd.g	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 1 · 𝑥) = 𝑥)
73	72	ralrimiva 3107	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥)
74		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ( 1 · 𝑥) = ( 1 · 𝑤))
75		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤)
76	74, 75	eqeq12d 2754	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (( 1 · 𝑥) = 𝑥 ↔ ( 1 · 𝑤) = 𝑤))
77	76	rspcv 3547	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥 → ( 1 · 𝑤) = 𝑤))
78	77	ad2antll 725	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥 → ( 1 · 𝑤) = 𝑤))
79	73, 78	mpan9 506	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ( 1 · 𝑤) = 𝑤)
80	56, 71, 79	jca32 515	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
81	80	anassrs 467	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
82	81	ralrimivva 3114	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
83	82	ralrimivva 3114	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
84		islmodd.b	. . . . 5 ⊢ (𝜑 → 𝐵 = (Base‘𝐹))
85	2	fveq2d 6760	. . . . 5 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝑊)))
86	84, 85	eqtrd 2778	. . . 4 ⊢ (𝜑 → 𝐵 = (Base‘(Scalar‘𝑊)))
87		islmodd.v	. . . . . 6 ⊢ (𝜑 → 𝑉 = (Base‘𝑊))
88		islmodd.s	. . . . . . . . . . 11 ⊢ (𝜑 → · = ( ·_𝑠 ‘𝑊))
89	88	oveqd 7272	. . . . . . . . . 10 ⊢ (𝜑 → (𝑟 · 𝑤) = (𝑟( ·_𝑠 ‘𝑊)𝑤))
90	89, 87	eleq12d 2833	. . . . . . . . 9 ⊢ (𝜑 → ((𝑟 · 𝑤) ∈ 𝑉 ↔ (𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊)))
91		eqidd 2739	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑟 = 𝑟)
92		islmodd.a	. . . . . . . . . . . 12 ⊢ (𝜑 → + = (+_g‘𝑊))
93	92	oveqd 7272	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 + 𝑢) = (𝑤(+_g‘𝑊)𝑢))
94	88, 91, 93	oveq123d 7276	. . . . . . . . . 10 ⊢ (𝜑 → (𝑟 · (𝑤 + 𝑢)) = (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)))
95	88	oveqd 7272	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑟 · 𝑢) = (𝑟( ·_𝑠 ‘𝑊)𝑢))
96	92, 89, 95	oveq123d 7276	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑟 · 𝑤) + (𝑟 · 𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)))
97	94, 96	eqeq12d 2754	. . . . . . . . 9 ⊢ (𝜑 → ((𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ↔ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢))))
98		islmodd.p	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⨣ = (+_g‘𝐹))
99	2	fveq2d 6760	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+_g‘𝐹) = (+_g‘(Scalar‘𝑊)))
100	98, 99	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → ⨣ = (+_g‘(Scalar‘𝑊)))
101	100	oveqd 7272	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ⨣ 𝑟) = (𝑥(+_g‘(Scalar‘𝑊))𝑟))
102		eqidd 2739	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑤 = 𝑤)
103	88, 101, 102	oveq123d 7276	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤))
104	88	oveqd 7272	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 · 𝑤) = (𝑥( ·_𝑠 ‘𝑊)𝑤))
105	92, 104, 89	oveq123d 7276	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 · 𝑤) + (𝑟 · 𝑤)) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))
106	103, 105	eqeq12d 2754	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))))
107	90, 97, 106	3anbi123d 1434	. . . . . . . 8 ⊢ (𝜑 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))))
108		islmodd.t	. . . . . . . . . . . . 13 ⊢ (𝜑 → × = (._r‘𝐹))
109	2	fveq2d 6760	. . . . . . . . . . . . 13 ⊢ (𝜑 → (._r‘𝐹) = (._r‘(Scalar‘𝑊)))
110	108, 109	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → × = (._r‘(Scalar‘𝑊)))
111	110	oveqd 7272	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 × 𝑟) = (𝑥(._r‘(Scalar‘𝑊))𝑟))
112	88, 111, 102	oveq123d 7276	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 × 𝑟) · 𝑤) = ((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤))
113		eqidd 2739	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑥 = 𝑥)
114	88, 113, 89	oveq123d 7276	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 · (𝑟 · 𝑤)) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))
115	112, 114	eqeq12d 2754	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ↔ ((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))))
116		islmodd.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (1_r‘𝐹))
117	2	fveq2d 6760	. . . . . . . . . . . 12 ⊢ (𝜑 → (1_r‘𝐹) = (1_r‘(Scalar‘𝑊)))
118	116, 117	eqtrd 2778	. . . . . . . . . . 11 ⊢ (𝜑 → 1 = (1_r‘(Scalar‘𝑊)))
119	88, 118, 102	oveq123d 7276	. . . . . . . . . 10 ⊢ (𝜑 → ( 1 · 𝑤) = ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤))
120	119	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝜑 → (( 1 · 𝑤) = 𝑤 ↔ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))
121	115, 120	anbi12d 630	. . . . . . . 8 ⊢ (𝜑 → ((((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤)))
122	107, 121	anbi12d 630	. . . . . . 7 ⊢ (𝜑 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
123	87, 122	raleqbidv 3327	. . . . . 6 ⊢ (𝜑 → (∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
124	87, 123	raleqbidv 3327	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
125	86, 124	raleqbidv 3327	. . . 4 ⊢ (𝜑 → (∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
126	86, 125	raleqbidv 3327	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
127	83, 126	mpbid 231	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤)))
128		eqid 2738	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
129		eqid 2738	. . 3 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
130		eqid 2738	. . 3 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
131		eqid 2738	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
132		eqid 2738	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
133		eqid 2738	. . 3 ⊢ (+_g‘(Scalar‘𝑊)) = (+_g‘(Scalar‘𝑊))
134		eqid 2738	. . 3 ⊢ (._r‘(Scalar‘𝑊)) = (._r‘(Scalar‘𝑊))
135		eqid 2738	. . 3 ⊢ (1_r‘(Scalar‘𝑊)) = (1_r‘(Scalar‘𝑊))
136	128, 129, 130, 131, 132, 133, 134, 135	islmod 20042	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (Scalar‘𝑊) ∈ Ring ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
137	1, 4, 127, 136	syl3anbrc 1341	1 ⊢ (𝜑 → 𝑊 ∈ LMod)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ‘cfv 6418 (class class class)co 7255 Basecbs 16840 +_gcplusg 16888 ._rcmulr 16889 Scalarcsca 16891 ·_𝑠 cvsca 16892 Grpcgrp 18492 1_rcur 19652 Ringcrg 19698 LModclmod 20038

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-nul 5225

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-iota 6376 df-fv 6426 df-ov 7258 df-lmod 20040

This theorem is referenced by: rmodislmod 20106 rmodislmodOLD 20107 islss3 20136 prdslmodd 20146 sralmod 20370 zlmlmod 20640 psrlmod 21080 cnlmod 24209 imaslmod 31455 lduallmodlem 37093 dvalveclem 38966 dvhlveclem 39049 mendlmod 40934

W3C validator