islmodd - Intuitionistic Logic Explorer

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

Theorem islmodd 13570

Description: Properties that determine a left module. See note in isgrpd2 12932 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 2267	. 2 ⊢ (𝜑 → (Scalar‘𝑊) ∈ Ring)
5		islmodd.w	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉) → (𝑥 · 𝑦) ∈ 𝑉)
6	5	3expb 1206	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉)) → (𝑥 · 𝑦) ∈ 𝑉)
7	6	ralrimivva 2572	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉)
8		oveq1 5898	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑟 → (𝑥 · 𝑦) = (𝑟 · 𝑦))
9	8	eleq1d 2258	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑟 → ((𝑥 · 𝑦) ∈ 𝑉 ↔ (𝑟 · 𝑦) ∈ 𝑉))
10		oveq2 5899	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (𝑟 · 𝑦) = (𝑟 · 𝑤))
11	10	eleq1d 2258	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ((𝑟 · 𝑦) ∈ 𝑉 ↔ (𝑟 · 𝑤) ∈ 𝑉))
12	9, 11	rspc2v 2869	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉 → (𝑟 · 𝑤) ∈ 𝑉))
13	12	ad2ant2l 508	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 (𝑥 · 𝑦) ∈ 𝑉 → (𝑟 · 𝑤) ∈ 𝑉))
14	7, 13	mpan9 281	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (𝑟 · 𝑤) ∈ 𝑉)
15		islmodd.c	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
16	15	ralrimivvva 2573	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
17		oveq1 5898	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (𝑥 · (𝑦 + 𝑧)) = (𝑟 · (𝑦 + 𝑧)))
18		oveq1 5898	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑥 · 𝑧) = (𝑟 · 𝑧))
19	8, 18	oveq12d 5909	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → ((𝑥 · 𝑦) + (𝑥 · 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧)))
20	17, 19	eqeq12d 2204	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ↔ (𝑟 · (𝑦 + 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧))))
21		oveq1 5898	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → (𝑦 + 𝑧) = (𝑤 + 𝑧))
22	21	oveq2d 5907	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝑟 · (𝑦 + 𝑧)) = (𝑟 · (𝑤 + 𝑧)))
23	10	oveq1d 5906	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → ((𝑟 · 𝑦) + (𝑟 · 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧)))
24	22, 23	eqeq12d 2204	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝑟 · (𝑦 + 𝑧)) = ((𝑟 · 𝑦) + (𝑟 · 𝑧)) ↔ (𝑟 · (𝑤 + 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧))))
25		oveq2 5899	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝑤 + 𝑧) = (𝑤 + 𝑢))
26	25	oveq2d 5907	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝑟 · (𝑤 + 𝑧)) = (𝑟 · (𝑤 + 𝑢)))
27		oveq2 5899	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝑟 · 𝑧) = (𝑟 · 𝑢))
28	27	oveq2d 5907	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → ((𝑟 · 𝑤) + (𝑟 · 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)))
29	26, 28	eqeq12d 2204	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → ((𝑟 · (𝑤 + 𝑧)) = ((𝑟 · 𝑤) + (𝑟 · 𝑧)) ↔ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
30	20, 24, 29	rspc3v 2872	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉 ∧ 𝑢 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
31	30	3com23 1211	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
32	31	3expb 1206	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
33	32	adantll 476	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢))))
34	16, 33	mpan9 281	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)))
35		simpll 527	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → 𝑥 ∈ 𝐵)
36		islmodd.d	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
37	36	3exp2 1227	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝑉 → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
38	37	imp43 355	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
39	38	ralrimivva 2572	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
40	35, 39	sylan2 286	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
41		simprlr 538	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → 𝑟 ∈ 𝐵)
42		simprrr 540	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → 𝑤 ∈ 𝑉)
43		oveq2 5899	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑟 → (𝑥 ⨣ 𝑦) = (𝑥 ⨣ 𝑟))
44	43	oveq1d 5906	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 ⨣ 𝑟) · 𝑧))
45		oveq1 5898	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑟 → (𝑦 · 𝑧) = (𝑟 · 𝑧))
46	45	oveq2d 5907	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = ((𝑥 · 𝑧) + (𝑟 · 𝑧)))
47	44, 46	eqeq12d 2204	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) ↔ ((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 · 𝑧) + (𝑟 · 𝑧))))
48		oveq2 5899	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 ⨣ 𝑟) · 𝑤))
49		oveq2 5899	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑥 · 𝑧) = (𝑥 · 𝑤))
50		oveq2 5899	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑟 · 𝑧) = (𝑟 · 𝑤))
51	49, 50	oveq12d 5909	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑥 · 𝑧) + (𝑟 · 𝑧)) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)))
52	48, 51	eqeq12d 2204	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝑥 ⨣ 𝑟) · 𝑧) = ((𝑥 · 𝑧) + (𝑟 · 𝑧)) ↔ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
53	47, 52	rspc2v 2869	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
54	41, 42, 53	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
55	40, 54	mpd 13	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)))
56	14, 34, 55	3jca 1179	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))))
57		islmodd.e	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
58	57	3exp2 1227	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝑉 → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))))))
59	58	imp43 355	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
60	59	ralrimivva 2572	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
61	35, 60	sylan2 286	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
62		oveq2 5899	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → (𝑥 × 𝑦) = (𝑥 × 𝑟))
63	62	oveq1d 5906	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → ((𝑥 × 𝑦) · 𝑧) = ((𝑥 × 𝑟) · 𝑧))
64	45	oveq2d 5907	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑥 · (𝑦 · 𝑧)) = (𝑥 · (𝑟 · 𝑧)))
65	63, 64	eqeq12d 2204	. . . . . . . . . 10 ⊢ (𝑦 = 𝑟 → (((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) ↔ ((𝑥 × 𝑟) · 𝑧) = (𝑥 · (𝑟 · 𝑧))))
66		oveq2 5899	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → ((𝑥 × 𝑟) · 𝑧) = ((𝑥 × 𝑟) · 𝑤))
67	50	oveq2d 5907	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (𝑥 · (𝑟 · 𝑧)) = (𝑥 · (𝑟 · 𝑤)))
68	66, 67	eqeq12d 2204	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (((𝑥 × 𝑟) · 𝑧) = (𝑥 · (𝑟 · 𝑧)) ↔ ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
69	65, 68	rspc2v 2869	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝑤 ∈ 𝑉) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
70	41, 42, 69	syl2anc 411	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑉 ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤))))
71	61, 70	mpd 13	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)))
72		islmodd.g	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 1 · 𝑥) = 𝑥)
73	72	ralrimiva 2563	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥)
74		oveq2 5899	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ( 1 · 𝑥) = ( 1 · 𝑤))
75		id 19	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤)
76	74, 75	eqeq12d 2204	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (( 1 · 𝑥) = 𝑥 ↔ ( 1 · 𝑤) = 𝑤))
77	76	rspcv 2852	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥 → ( 1 · 𝑤) = 𝑤))
78	77	ad2antll 491	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (∀𝑥 ∈ 𝑉 ( 1 · 𝑥) = 𝑥 → ( 1 · 𝑤) = 𝑤))
79	73, 78	mpan9 281	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → ( 1 · 𝑤) = 𝑤)
80	56, 71, 79	jca32 310	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉))) → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
81	80	anassrs 400	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) ∧ (𝑢 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
82	81	ralrimivva 2572	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
83	82	ralrimivva 2572	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
84		islmodd.b	. . . . 5 ⊢ (𝜑 → 𝐵 = (Base‘𝐹))
85	2	fveq2d 5534	. . . . 5 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝑊)))
86	84, 85	eqtrd 2222	. . . 4 ⊢ (𝜑 → 𝐵 = (Base‘(Scalar‘𝑊)))
87		islmodd.v	. . . . . 6 ⊢ (𝜑 → 𝑉 = (Base‘𝑊))
88		islmodd.s	. . . . . . . . . . 11 ⊢ (𝜑 → · = ( ·_𝑠 ‘𝑊))
89	88	oveqd 5908	. . . . . . . . . 10 ⊢ (𝜑 → (𝑟 · 𝑤) = (𝑟( ·_𝑠 ‘𝑊)𝑤))
90	89, 87	eleq12d 2260	. . . . . . . . 9 ⊢ (𝜑 → ((𝑟 · 𝑤) ∈ 𝑉 ↔ (𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊)))
91		eqidd 2190	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑟 = 𝑟)
92		islmodd.a	. . . . . . . . . . . 12 ⊢ (𝜑 → + = (+_g‘𝑊))
93	92	oveqd 5908	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 + 𝑢) = (𝑤(+_g‘𝑊)𝑢))
94	88, 91, 93	oveq123d 5912	. . . . . . . . . 10 ⊢ (𝜑 → (𝑟 · (𝑤 + 𝑢)) = (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)))
95	88	oveqd 5908	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑟 · 𝑢) = (𝑟( ·_𝑠 ‘𝑊)𝑢))
96	92, 89, 95	oveq123d 5912	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑟 · 𝑤) + (𝑟 · 𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)))
97	94, 96	eqeq12d 2204	. . . . . . . . 9 ⊢ (𝜑 → ((𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ↔ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢))))
98		islmodd.p	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⨣ = (+_g‘𝐹))
99	2	fveq2d 5534	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+_g‘𝐹) = (+_g‘(Scalar‘𝑊)))
100	98, 99	eqtrd 2222	. . . . . . . . . . . 12 ⊢ (𝜑 → ⨣ = (+_g‘(Scalar‘𝑊)))
101	100	oveqd 5908	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ⨣ 𝑟) = (𝑥(+_g‘(Scalar‘𝑊))𝑟))
102		eqidd 2190	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑤 = 𝑤)
103	88, 101, 102	oveq123d 5912	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤))
104	88	oveqd 5908	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 · 𝑤) = (𝑥( ·_𝑠 ‘𝑊)𝑤))
105	92, 104, 89	oveq123d 5912	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 · 𝑤) + (𝑟 · 𝑤)) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))
106	103, 105	eqeq12d 2204	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))))
107	90, 97, 106	3anbi123d 1323	. . . . . . . 8 ⊢ (𝜑 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))))
108		islmodd.t	. . . . . . . . . . . . 13 ⊢ (𝜑 → × = (._r‘𝐹))
109	2	fveq2d 5534	. . . . . . . . . . . . 13 ⊢ (𝜑 → (._r‘𝐹) = (._r‘(Scalar‘𝑊)))
110	108, 109	eqtrd 2222	. . . . . . . . . . . 12 ⊢ (𝜑 → × = (._r‘(Scalar‘𝑊)))
111	110	oveqd 5908	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 × 𝑟) = (𝑥(._r‘(Scalar‘𝑊))𝑟))
112	88, 111, 102	oveq123d 5912	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 × 𝑟) · 𝑤) = ((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤))
113		eqidd 2190	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑥 = 𝑥)
114	88, 113, 89	oveq123d 5912	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 · (𝑟 · 𝑤)) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)))
115	112, 114	eqeq12d 2204	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ↔ ((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))))
116		islmodd.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (1_r‘𝐹))
117	2	fveq2d 5534	. . . . . . . . . . . 12 ⊢ (𝜑 → (1_r‘𝐹) = (1_r‘(Scalar‘𝑊)))
118	116, 117	eqtrd 2222	. . . . . . . . . . 11 ⊢ (𝜑 → 1 = (1_r‘(Scalar‘𝑊)))
119	88, 118, 102	oveq123d 5912	. . . . . . . . . 10 ⊢ (𝜑 → ( 1 · 𝑤) = ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤))
120	119	eqeq1d 2198	. . . . . . . . 9 ⊢ (𝜑 → (( 1 · 𝑤) = 𝑤 ↔ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))
121	115, 120	anbi12d 473	. . . . . . . 8 ⊢ (𝜑 → ((((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤)))
122	107, 121	anbi12d 473	. . . . . . 7 ⊢ (𝜑 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
123	87, 122	raleqbidv 2698	. . . . . 6 ⊢ (𝜑 → (∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
124	87, 123	raleqbidv 2698	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
125	86, 124	raleqbidv 2698	. . . 4 ⊢ (𝜑 → (∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
126	86, 125	raleqbidv 2698	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑟 ∈ 𝐵 ∀𝑢 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑢)) = ((𝑟 · 𝑤) + (𝑟 · 𝑢)) ∧ ((𝑥 ⨣ 𝑟) · 𝑤) = ((𝑥 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑥 × 𝑟) · 𝑤) = (𝑥 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤))))
127	83, 126	mpbid 147	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·_𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·_𝑠 ‘𝑊)(𝑤(+_g‘𝑊)𝑢)) = ((𝑟( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑢)) ∧ ((𝑥(+_g‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = ((𝑥( ·_𝑠 ‘𝑊)𝑤)(+_g‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤))) ∧ (((𝑥(._r‘(Scalar‘𝑊))𝑟)( ·_𝑠 ‘𝑊)𝑤) = (𝑥( ·_𝑠 ‘𝑊)(𝑟( ·_𝑠 ‘𝑊)𝑤)) ∧ ((1_r‘(Scalar‘𝑊))( ·_𝑠 ‘𝑊)𝑤) = 𝑤)))
128		eqid 2189	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
129		eqid 2189	. . 3 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
130		eqid 2189	. . 3 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
131		eqid 2189	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
132		eqid 2189	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
133		eqid 2189	. . 3 ⊢ (+_g‘(Scalar‘𝑊)) = (+_g‘(Scalar‘𝑊))
134		eqid 2189	. . 3 ⊢ (._r‘(Scalar‘𝑊)) = (._r‘(Scalar‘𝑊))
135		eqid 2189	. . 3 ⊢ (1_r‘(Scalar‘𝑊)) = (1_r‘(Scalar‘𝑊))
136	128, 129, 130, 131, 132, 133, 134, 135	islmod 13568	. 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 1183	1 ⊢ (𝜑 → 𝑊 ∈ LMod)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 = wceq 1364 ∈ wcel 2160 ∀wral 2468 ‘cfv 5231 (class class class)co 5891 Basecbs 12480 +_gcplusg 12555 ._rcmulr 12556 Scalarcsca 12558 ·_𝑠 cvsca 12559 Grpcgrp 12911 1_rcur 13274 Ringcrg 13311 LModclmod 13564

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-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 2162 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-cnex 7920 ax-resscn 7921 ax-1re 7923 ax-addrcl 7926

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-rab 2477 df-v 2754 df-sbc 2978 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-br 4019 df-opab 4080 df-mpt 4081 df-id 4308 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-iota 5193 df-fun 5233 df-fn 5234 df-fv 5239 df-ov 5894 df-inn 8938 df-2 8996 df-3 8997 df-4 8998 df-5 8999 df-6 9000 df-ndx 12483 df-slot 12484 df-base 12486 df-plusg 12568 df-mulr 12569 df-sca 12571 df-vsca 12572 df-lmod 13566

This theorem is referenced by: rmodislmod 13628 islss3 13656 sralmod 13727

W3C validator