This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )