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 21103

Description: Properties that determine a left module. See note in isgrpd2 19129 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 2861	. 2 ⊢ (𝜑 → (Scalar‘𝑊) ∈ Ring)
5		islmodd.w	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉) → (𝑥 · 𝑦) ∈ 𝑉)
6	5	3expb 1138	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉)) → (𝑥 · 𝑦) ∈ 𝑉)
7	6	ralrimivva 3205	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉)
8		oveq1 7415	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑟 → (𝑥 · 𝑦) = (𝑟 · 𝑦))
9	8	eleq1d 2845	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑟 → ((𝑥 · 𝑦) ∈ 𝑉 ↔ (𝑟 · 𝑦) ∈ 𝑉))
10		oveq2 7416	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (𝑟 · 𝑦) = (𝑟 · 𝑤))
11	10	eleq1d 2845	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ((𝑟 · 𝑦) ∈ 𝑉 ↔ (𝑟 · 𝑤) ∈ 𝑉))
12	9, 11	rspc2v 3586	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉 → (𝑟 · 𝑤) ∈ 𝑉))
13	12	ad2ant2l 759	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉 → (𝑟 · 𝑤) ∈ 𝑉))
14	7, 13	mpan9 516	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (𝑟 · 𝑤) ∈ 𝑉)
15		islmodd.c	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
16	15	ralrimivvva 3208	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
17		oveq1 7415	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (𝑥 · (𝑦 + 𝑧)) = (𝑟 · (𝑦 + 𝑧)))
18		oveq1 7415	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑥 · 𝑧) = (𝑟 · 𝑧))
19	8, 18	oveq12d 7426	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → ((𝑥 · 𝑦) + (𝑥 · 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧)))
20	17, 19	eqeq12d 2776	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ↔ (𝑟 · (𝑦 + 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧))))
21		oveq1 7415	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → (𝑦 + 𝑧) = (𝑤 + 𝑧))
22	21	oveq2d 7424	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝑟 · (𝑦 + 𝑧)) = (𝑟 · (𝑤 + 𝑧)))
23	10	oveq1d 7423	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → ((𝑟 · 𝑦) + (𝑟 · 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧)))
24	22, 23	eqeq12d 2776	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝑟 · (𝑦 + 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧)) ↔ (𝑟 · (𝑤 + 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧))))
25		oveq2 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝑤 + 𝑧) = (𝑤 + 𝑢))
26	25	oveq2d 7424	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝑟 · (𝑤 + 𝑧)) = (𝑟 · (𝑤 + 𝑢)))
27		oveq2 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝑟 · 𝑧) = (𝑟 · 𝑢))
28	27	oveq2d 7424	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → ((𝑟 · 𝑤) + (𝑟 · 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)))
29	26, 28	eqeq12d 2776	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → ((𝑟 · (𝑤 + 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧)) ↔ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
30	20, 24, 29	rspc3v 3591	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉 ∧ 𝑢 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
31	30	3com23 1144	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
32	31	3expb 1138	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
33	32	adantll 727	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
34	16, 33	mpan9 516	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)))
35		simpll 779	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → 𝑥 ∈ 𝐵)
36		islmodd.d	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
37	36	3exp2 1373	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝑉 → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
38	37	imp43 433	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
39	38	ralrimivva 3205	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
40	35, 39	sylan2 605	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
41		simprlr 792	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → 𝑟 ∈ 𝐵)
42		simprrr 794	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → 𝑤 ∈ 𝑉)
43		oveq2 7416	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑟 → (𝑥 ⨣ 𝑦) = (𝑥 ⨣ 𝑟))
44	43	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 ⨣ 𝑟) · 𝑧))
45		oveq1 7415	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑟 → (𝑦 · 𝑧) = (𝑟 · 𝑧))
46	45	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = ((𝑥 · 𝑧) + (𝑟 · 𝑧)))
47	44, 46	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) ↔ ((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 · 𝑧) + (𝑟 · 𝑧))))
48		oveq2 7416	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 ⨣ 𝑟) · 𝑤))
49		oveq2 7416	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑥 · 𝑧) = (𝑥 · 𝑤))
50		oveq2 7416	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑟 · 𝑧) = (𝑟 · 𝑤))
51	49, 50	oveq12d 7426	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑥 · 𝑧) + (𝑟 · 𝑧)) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)))
52	48, 51	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 · 𝑧) + (𝑟 · 𝑧)) ↔ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
53	47, 52	rspc2v 3586	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
54	41, 42, 53	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
55	40, 54	mpd 16	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)))
56	14, 34, 55	3jca 1146	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
57		islmodd.e	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
58	57	3exp2 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝑉 → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))))))
59	58	imp43 433	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
60	59	ralrimivva 3205	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
61	35, 60	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
62		oveq2 7416	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → (𝑥 × 𝑦) = (𝑥 × 𝑟))
63	62	oveq1d 7423	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → ((𝑥 × 𝑦) · 𝑧) = ((𝑥 × 𝑟) · 𝑧))
64	45	oveq2d 7424	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑥 · (𝑦 · 𝑧)) = (𝑥 · (𝑟 · 𝑧)))
65	63, 64	eqeq12d 2776	. . . . . . . . . 10 ⊢ (𝑦 = 𝑟 → (((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) ↔ ((𝑥 × 𝑟) · 𝑧) = (𝑥 · (𝑟 · 𝑧))))
66		oveq2 7416	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → ((𝑥 × 𝑟) · 𝑧) = ((𝑥 × 𝑟) · 𝑤))
67	50	oveq2d 7424	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (𝑥 · (𝑟 · 𝑧)) = (𝑥 · (𝑟 · 𝑤)))
68	66, 67	eqeq12d 2776	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (((𝑥 × 𝑟) · 𝑧) = (𝑥 · (𝑟 · 𝑧)) ↔ ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
69	65, 68	rspc2v 3586	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
70	41, 42, 69	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
71	61, 70	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)))
72		islmodd.g	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 1 · 𝑥) = 𝑥)
73	72	ralrimiva 3154	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥)
74		oveq2 7416	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ( 1 · 𝑥) = ( 1 · 𝑤))
75		id 23	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤)
76	74, 75	eqeq12d 2776	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (( 1 · 𝑥) = 𝑥 ↔ ( 1 · 𝑤) = 𝑤))
77	76	rspcv 3572	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥 → ( 1 · 𝑤) = 𝑤))
78	77	ad2antll 742	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥 → ( 1 · 𝑤) = 𝑤))
79	73, 78	mpan9 516	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ( 1 · 𝑤) = 𝑤)
80	56, 71, 79	jca32 525	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
81	80	anassrs 473	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
82	81	ralrimivva 3205	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
83	82	ralrimivva 3205	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
84		islmodd.b	. . . . 5 ⊢ (𝜑 → 𝐵 = (Base‘𝐹))
85	2	fveq2d 6877	. . . . 5 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝑊)))
86	84, 85	eqtrd 2795	. . . 4 ⊢ (𝜑 → 𝐵 = (Base‘(Scalar‘𝑊)))
87		islmodd.v	. . . . . 6 ⊢ (𝜑 → 𝑉 = (Base‘𝑊))
88		islmodd.s	. . . . . . . . . . 11 ⊢ (𝜑 → · = ( ·_𝑠 ‘𝑊))
89	88	oveqd 7425	. . . . . . . . . 10 ⊢ (𝜑 → (𝑟 · 𝑤) = (𝑟( ·_𝑠 ‘𝑊)𝑤))
90	89, 87	eleq12d 2854	. . . . . . . . 9 ⊢ (𝜑 → ((𝑟 · 𝑤) ∈ 𝑉 ↔ (𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊)))
91		eqidd 2761	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑟 = 𝑟)
92		islmodd.a	. . . . . . . . . . . 12 ⊢ (𝜑 → + = (+_g‘𝑊))
93	92	oveqd 7425	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 + 𝑢) = (𝑤(+_g‘𝑊)𝑢))
94	88, 91, 93	oveq123d 7429	. . . . . . . . . 10 ⊢ (𝜑 → (𝑟 · (𝑤 + 𝑢)) = (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)))
95	88	oveqd 7425	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑟 · 𝑢) = (𝑟( ·_𝑠 ‘𝑊)𝑢))
96	92, 89, 95	oveq123d 7429	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑟 · 𝑤) + (𝑟 · 𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)))
97	94, 96	eqeq12d 2776	. . . . . . . . 9 ⊢ (𝜑 → ((𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ↔ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢))))
98		islmodd.p	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⨣ = (+_g‘𝐹))
99	2	fveq2d 6877	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+_g‘𝐹) = (+_g‘(Scalar‘𝑊)))
100	98, 99	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → ⨣ = (+_g‘(Scalar‘𝑊)))
101	100	oveqd 7425	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ⨣ 𝑟) = (𝑥(+_g‘(Scalar‘𝑊))𝑟))
102		eqidd 2761	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑤 = 𝑤)
103	88, 101, 102	oveq123d 7429	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤))
104	88	oveqd 7425	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 · 𝑤) = (𝑥( ·_𝑠 ‘𝑊)𝑤))
105	92, 104, 89	oveq123d 7429	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 · 𝑤) + (𝑟 · 𝑤)) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))
106	103, 105	eqeq12d 2776	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))))
107	90, 97, 106	3anbi123d 1464	. . . . . . . 8 ⊢ (𝜑 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))))
108		islmodd.t	. . . . . . . . . . . . 13 ⊢ (𝜑 → × = (._r‘𝐹))
109	2	fveq2d 6877	. . . . . . . . . . . . 13 ⊢ (𝜑 → (._r‘𝐹) = (._r‘(Scalar‘𝑊)))
110	108, 109	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → × = (._r‘(Scalar‘𝑊)))
111	110	oveqd 7425	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 × 𝑟) = (𝑥(._r‘(Scalar‘𝑊))𝑟))
112	88, 111, 102	oveq123d 7429	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 × 𝑟) · 𝑤) = ((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤))
113		eqidd 2761	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑥 = 𝑥)
114	88, 113, 89	oveq123d 7429	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 · (𝑟 · 𝑤)) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))
115	112, 114	eqeq12d 2776	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ↔ ((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))))
116		islmodd.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (1_r‘𝐹))
117	2	fveq2d 6877	. . . . . . . . . . . 12 ⊢ (𝜑 → (1_r‘𝐹) = (1_r‘(Scalar‘𝑊)))
118	116, 117	eqtrd 2795	. . . . . . . . . . 11 ⊢ (𝜑 → 1 = (1_r‘(Scalar‘𝑊)))
119	88, 118, 102	oveq123d 7429	. . . . . . . . . 10 ⊢ (𝜑 → ( 1 · 𝑤) = ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤))
120	119	eqeq1d 2762	. . . . . . . . 9 ⊢ (𝜑 → (( 1 · 𝑤) = 𝑤 ↔ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))
121	115, 120	anbi12d 644	. . . . . . . 8 ⊢ (𝜑 → ((((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤)))
122	107, 121	anbi12d 644	. . . . . . 7 ⊢ (𝜑 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
123	87, 122	raleqbidv 3334	. . . . . 6 ⊢ (𝜑 → (∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
124	87, 123	raleqbidv 3334	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
125	86, 124	raleqbidv 3334	. . . 4 ⊢ (𝜑 → (∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
126	86, 125	raleqbidv 3334	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
127	83, 126	mpbid 235	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤)))
128		eqid 2760	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
129		eqid 2760	. . 3 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
130		eqid 2760	. . 3 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
131		eqid 2760	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
132		eqid 2760	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
133		eqid 2760	. . 3 ⊢ (+_g‘(Scalar‘𝑊)) = (+_g‘(Scalar‘𝑊))
134		eqid 2760	. . 3 ⊢ (._r‘(Scalar‘𝑊)) = (._r‘(Scalar‘𝑊))
135		eqid 2760	. . 3 ⊢ (1_r‘(Scalar‘𝑊)) = (1_r‘(Scalar‘𝑊))
136	128, 129, 130, 131, 132, 133, 134, 135	islmod 21101	. 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 1362	1 ⊢ (𝜑 → 𝑊 ∈ LMod)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3076 ‘cfv 6527 (class class class)co 7408 Basecbs 17349 +_gcplusg 17390 ._rcmulr 17391 Scalarcsca 17393 ·_𝑠 cvsca 17394 Grpcgrp 19106 1_rcur 20369 Ringcrg 20421 LModclmod 21097

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2732 ax-nul 5259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rab 3413 df-v 3452 df-sbc 3739 df-dif 3901 df-un 3903 df-ss 3915 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-iota 6483 df-fv 6535 df-ov 7411 df-lmod 21099

This theorem is used by: rmodislmod 21167 islss3 21196 prdslmodd 21206 sralmod 21424 zlmlmod 21790 psrlmod 22229 cnlmod 25423 imaslmod 33848 lduallmodlem 40129 dvalveclem 42002 dvhlveclem 42085 mendlmod 44134

W3C validator