Theorem islmodd

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

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

Proof

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