Metamath Proof Explorer

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 )