Metamath Proof Explorer

Theorem isassa

Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses isassa.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
isassa.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
isassa.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
isassa.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
isassa.t ⊢ × = ( .r ‘ 𝑊 )
Assertion isassa ( 𝑊 ∈ AssAlg ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing ) ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isassa.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 isassa.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 isassa.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 isassa.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 isassa.t ⊢ × = ( .r ‘ 𝑊 )
6 fvexd ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) ∈ V )
7 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
8 7 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐹 )
9 simpr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
10 9 eleq1d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = 𝐹 ) → ( 𝑓 ∈ CRing ↔ 𝐹 ∈ CRing ) )
11 9 fveq2d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
12 11 3 eqtr4di ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = 𝐵 )
13 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
14 13 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
15 fvexd ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) ∈ V )
16 fvexd ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) → ( .r ‘ 𝑤 ) ∈ V )
17 simpr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → 𝑡 = ( .r ‘ 𝑤 ) )
18 fveq2 ⊢ ( 𝑤 = 𝑊 → ( .r ‘ 𝑤 ) = ( .r ‘ 𝑊 ) )
19 18 ad2antrr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( .r ‘ 𝑤 ) = ( .r ‘ 𝑊 ) )
20 19 5 eqtr4di ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( .r ‘ 𝑤 ) = × )
21 17 20 eqtrd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → 𝑡 = × )
22 simplr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → 𝑠 = ( ·𝑠 ‘ 𝑤 ) )
23 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
24 23 ad2antrr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
25 24 4 eqtr4di ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( ·𝑠 ‘ 𝑤 ) = · )
26 22 25 eqtrd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → 𝑠 = · )
27 26 oveqd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( 𝑟 𝑠 𝑥 ) = ( 𝑟 · 𝑥 ) )
28 eqidd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → 𝑦 = 𝑦 )
29 21 27 28 oveq123d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( ( 𝑟 · 𝑥 ) × 𝑦 ) )
30 eqidd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → 𝑟 = 𝑟 )
31 21 oveqd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( 𝑥 𝑡 𝑦 ) = ( 𝑥 × 𝑦 ) )
32 26 30 31 oveq123d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) )
33 29 32 eqeq12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ↔ ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) )
34 eqidd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → 𝑥 = 𝑥 )
35 26 oveqd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( 𝑟 𝑠 𝑦 ) = ( 𝑟 · 𝑦 ) )
36 21 34 35 oveq123d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑥 × ( 𝑟 · 𝑦 ) ) )
37 36 32 eqeq12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ↔ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) )
38 33 37 anbi12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) ∧ 𝑡 = ( .r ‘ 𝑤 ) ) → ( ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
39 16 38 sbcied ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑠 = ( ·𝑠 ‘ 𝑤 ) ) → ( [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
40 15 39 sbcied ⊢ ( 𝑤 = 𝑊 → ( [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
41 14 40 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
42 14 41 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
43 42 adantr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
44 12 43 raleqbidv ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
45 10 44 anbi12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = 𝐹 ) → ( ( 𝑓 ∈ CRing ∧ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ) ↔ ( 𝐹 ∈ CRing ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) ) )
46 6 8 45 sbcied2 ⊢ ( 𝑤 = 𝑊 → ( [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ CRing ∧ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ) ↔ ( 𝐹 ∈ CRing ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) ) )
47 df-assa ⊢ AssAlg = { 𝑤 ∈ ( LMod ∩ Ring ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ CRing ∧ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ) }
48 46 47 elrab2 ⊢ ( 𝑊 ∈ AssAlg ↔ ( 𝑊 ∈ ( LMod ∩ Ring ) ∧ ( 𝐹 ∈ CRing ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) ) )
49 anass ⊢ ( ( ( 𝑊 ∈ ( LMod ∩ Ring ) ∧ 𝐹 ∈ CRing ) ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) ↔ ( 𝑊 ∈ ( LMod ∩ Ring ) ∧ ( 𝐹 ∈ CRing ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) ) )
50 elin ⊢ ( 𝑊 ∈ ( LMod ∩ Ring ) ↔ ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) )
51 50 anbi1i ⊢ ( ( 𝑊 ∈ ( LMod ∩ Ring ) ∧ 𝐹 ∈ CRing ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) ∧ 𝐹 ∈ CRing ) )
52 df-3an ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) ∧ 𝐹 ∈ CRing ) )
53 51 52 bitr4i ⊢ ( ( 𝑊 ∈ ( LMod ∩ Ring ) ∧ 𝐹 ∈ CRing ) ↔ ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing ) )
54 53 anbi1i ⊢ ( ( ( 𝑊 ∈ ( LMod ∩ Ring ) ∧ 𝐹 ∈ CRing ) ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing ) ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
55 48 49 54 3bitr2i ⊢ ( 𝑊 ∈ AssAlg ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing ) ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )