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

Metamath Proof Explorer

Theorem assalem

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 assalem ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) )

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 1 2 3 4 5 isassa ⊢ ( 𝑊 ∈ AssAlg ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) ∧ ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ) )
7 6 simprbi ⊢ ( 𝑊 ∈ AssAlg → ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) )
8 oveq1 ⊢ ( 𝑟 = 𝐴 → ( 𝑟 · 𝑥 ) = ( 𝐴 · 𝑥 ) )
9 8 oveq1d ⊢ ( 𝑟 = 𝐴 → ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( ( 𝐴 · 𝑥 ) × 𝑦 ) )
10 oveq1 ⊢ ( 𝑟 = 𝐴 → ( 𝑟 · ( 𝑥 × 𝑦 ) ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) )
11 9 10 eqeq12d ⊢ ( 𝑟 = 𝐴 → ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ↔ ( ( 𝐴 · 𝑥 ) × 𝑦 ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) ) )
12 oveq1 ⊢ ( 𝑟 = 𝐴 → ( 𝑟 · 𝑦 ) = ( 𝐴 · 𝑦 ) )
13 12 oveq2d ⊢ ( 𝑟 = 𝐴 → ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑥 × ( 𝐴 · 𝑦 ) ) )
14 13 10 eqeq12d ⊢ ( 𝑟 = 𝐴 → ( ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ↔ ( 𝑥 × ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) ) )
15 11 14 anbi12d ⊢ ( 𝑟 = 𝐴 → ( ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) ↔ ( ( ( 𝐴 · 𝑥 ) × 𝑦 ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) ) ) )
16 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑋 ) )
17 16 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 · 𝑥 ) × 𝑦 ) = ( ( 𝐴 · 𝑋 ) × 𝑦 ) )
18 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 × 𝑦 ) = ( 𝑋 × 𝑦 ) )
19 18 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐴 · ( 𝑥 × 𝑦 ) ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) )
20 17 19 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐴 · 𝑥 ) × 𝑦 ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) ↔ ( ( 𝐴 · 𝑋 ) × 𝑦 ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) ) )
21 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 × ( 𝐴 · 𝑦 ) ) = ( 𝑋 × ( 𝐴 · 𝑦 ) ) )
22 21 19 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 × ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) ↔ ( 𝑋 × ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) ) )
23 20 22 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( ( 𝐴 · 𝑥 ) × 𝑦 ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝑥 × 𝑦 ) ) ) ↔ ( ( ( 𝐴 · 𝑋 ) × 𝑦 ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) ) ) )
24 oveq2 ⊢ ( 𝑦 = 𝑌 → ( ( 𝐴 · 𝑋 ) × 𝑦 ) = ( ( 𝐴 · 𝑋 ) × 𝑌 ) )
25 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 × 𝑦 ) = ( 𝑋 × 𝑌 ) )
26 25 oveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝐴 · ( 𝑋 × 𝑦 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )
27 24 26 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐴 · 𝑋 ) × 𝑦 ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) ↔ ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) )
28 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝑌 ) )
29 28 oveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑋 × ( 𝐴 · 𝑦 ) ) = ( 𝑋 × ( 𝐴 · 𝑌 ) ) )
30 29 26 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 × ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) ↔ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) )
31 27 30 anbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( ( 𝐴 · 𝑋 ) × 𝑦 ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝑋 × 𝑦 ) ) ) ↔ ( ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) ) )
32 15 23 31 rspc3v ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝑟 · 𝑥 ) × 𝑦 ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ∧ ( 𝑥 × ( 𝑟 · 𝑦 ) ) = ( 𝑟 · ( 𝑥 × 𝑦 ) ) ) → ( ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) ) )
33 7 32 mpan9 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) )