Metamath Proof Explorer


Theorem isassa

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

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

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 fveq2 ( 𝑓 = 𝐹 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
10 9 3 eqtr4di ( 𝑓 = 𝐹 → ( Base ‘ 𝑓 ) = 𝐵 )
11 10 adantl ( ( 𝑤 = 𝑊𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = 𝐵 )
12 fveq2 ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
13 12 1 eqtr4di ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
14 simpr ( ( 𝑠 = ·𝑡 = × ) → 𝑡 = × )
15 simpl ( ( 𝑠 = ·𝑡 = × ) → 𝑠 = · )
16 15 oveqd ( ( 𝑠 = ·𝑡 = × ) → ( 𝑟 𝑠 𝑥 ) = ( 𝑟 · 𝑥 ) )
17 eqidd ( ( 𝑠 = ·𝑡 = × ) → 𝑦 = 𝑦 )
18 14 16 17 oveq123d ( ( 𝑠 = ·𝑡 = × ) → ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( ( 𝑟 · 𝑥 ) × 𝑦 ) )
19 eqidd ( ( 𝑠 = ·𝑡 = × ) → 𝑟 = 𝑟 )
20 14 oveqd ( ( 𝑠 = ·𝑡 = × ) → ( 𝑥 𝑡 𝑦 ) = ( 𝑥 × 𝑦 ) )
21 15 19 20 oveq123d ( ( 𝑠 = ·𝑡 = × ) → ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) )
22 18 21 eqeq12d ( ( 𝑠 = ·𝑡 = × ) → ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ↔ ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) )
23 eqidd ( ( 𝑠 = ·𝑡 = × ) → 𝑥 = 𝑥 )
24 15 oveqd ( ( 𝑠 = ·𝑡 = × ) → ( 𝑟 𝑠 𝑦 ) = ( 𝑟 · 𝑦 ) )
25 14 23 24 oveq123d ( ( 𝑠 = ·𝑡 = × ) → ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑥 × ( 𝑟 · 𝑦 ) ) )
26 25 21 eqeq12d ( ( 𝑠 = ·𝑡 = × ) → ( ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ↔ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) )
27 22 26 anbi12d ( ( 𝑠 = ·𝑡 = × ) → ( ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
28 4 5 27 sbcie2s ( 𝑤 = 𝑊 → ( [ ( ·𝑠𝑤 ) / 𝑠 ] [ ( .r𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
29 13 28 raleqbidv ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠𝑤 ) / 𝑠 ] [ ( .r𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
30 13 29 raleqbidv ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠𝑤 ) / 𝑠 ] [ ( .r𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑥𝑉𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
31 30 adantr ( ( 𝑤 = 𝑊𝑓 = 𝐹 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠𝑤 ) / 𝑠 ] [ ( .r𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑥𝑉𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
32 11 31 raleqbidv ( ( 𝑤 = 𝑊𝑓 = 𝐹 ) → ( ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠𝑤 ) / 𝑠 ] [ ( .r𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑟𝐵𝑥𝑉𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
33 6 8 32 sbcied2 ( 𝑤 = 𝑊 → ( [ ( Scalar ‘ 𝑤 ) / 𝑓 ]𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠𝑤 ) / 𝑠 ] [ ( .r𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ↔ ∀ 𝑟𝐵𝑥𝑉𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
34 df-assa AssAlg = { 𝑤 ∈ ( LMod ∩ Ring ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ]𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠𝑤 ) / 𝑠 ] [ ( .r𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) }
35 33 34 elrab2 ( 𝑊 ∈ AssAlg ↔ ( 𝑊 ∈ ( LMod ∩ Ring ) ∧ ∀ 𝑟𝐵𝑥𝑉𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
36 elin ( 𝑊 ∈ ( LMod ∩ Ring ) ↔ ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) )
37 36 anbi1i ( ( 𝑊 ∈ ( LMod ∩ Ring ) ∧ ∀ 𝑟𝐵𝑥𝑉𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) ∧ ∀ 𝑟𝐵𝑥𝑉𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
38 35 37 bitri ( 𝑊 ∈ AssAlg ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) ∧ ∀ 𝑟𝐵𝑥𝑉𝑦𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )