Theorem isassad 19323

Description: Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.)

Hypotheses

Ref	Expression
isassad.v	⊢ (𝜑 → 𝑉 = (Base‘𝑊))
isassad.f	⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))
isassad.b	⊢ (𝜑 → 𝐵 = (Base‘𝐹))
isassad.s	⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))
isassad.t	⊢ (𝜑 → × = (.r‘𝑊))
isassad.1	⊢ (𝜑 → 𝑊 ∈ LMod)
isassad.2	⊢ (𝜑 → 𝑊 ∈ Ring)
isassad.3	⊢ (𝜑 → 𝐹 ∈ CRing)
isassad.4	⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)))
isassad.5	⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))

Assertion

Ref	Expression
isassad	⊢ (𝜑 → 𝑊 ∈ AssAlg)

Distinct variable groups:   𝑥,𝑟,𝑦,𝐵   𝜑,𝑟,𝑥,𝑦   𝑥,𝑉,𝑦   𝑊,𝑟,𝑥,𝑦

Allowed substitution hints:   · (𝑥,𝑦,𝑟)   × (𝑥,𝑦,𝑟)   𝐹(𝑥,𝑦,𝑟)   𝑉(𝑟)

Proof of Theorem isassad

Step	Hyp	Ref	Expression
1		isassad.1	. . 3 ⊢ (𝜑 → 𝑊 ∈ LMod)
2		isassad.2	. . 3 ⊢ (𝜑 → 𝑊 ∈ Ring)
3		isassad.f	. . . 4 ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))
4		isassad.3	. . . 4 ⊢ (𝜑 → 𝐹 ∈ CRing)
5	3, 4	eqeltrrd 2702	. . 3 ⊢ (𝜑 → (Scalar‘𝑊) ∈ CRing)
6	1, 2, 5	3jca 1242	. 2 ⊢ (𝜑 → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ (Scalar‘𝑊) ∈ CRing))
7		isassad.4	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)))
8		isassad.5	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))
9	7, 8	jca 554	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
10	9	ralrimivvva 2972	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
11		isassad.b	. . . . 5 ⊢ (𝜑 → 𝐵 = (Base‘𝐹))
12	3	fveq2d 6195	. . . . 5 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝑊)))
13	11, 12	eqtrd 2656	. . . 4 ⊢ (𝜑 → 𝐵 = (Base‘(Scalar‘𝑊)))
14		isassad.v	. . . . 5 ⊢ (𝜑 → 𝑉 = (Base‘𝑊))
15		isassad.t	. . . . . . . . 9 ⊢ (𝜑 → × = (.r‘𝑊))
16		isassad.s	. . . . . . . . . 10 ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))
17	16	oveqd 6667	. . . . . . . . 9 ⊢ (𝜑 → (𝑟 · 𝑥) = (𝑟( ·𝑠 ‘𝑊)𝑥))
18		eqidd 2623	. . . . . . . . 9 ⊢ (𝜑 → 𝑦 = 𝑦)
19	15, 17, 18	oveq123d 6671	. . . . . . . 8 ⊢ (𝜑 → ((𝑟 · 𝑥) × 𝑦) = ((𝑟( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦))
20		eqidd 2623	. . . . . . . . 9 ⊢ (𝜑 → 𝑟 = 𝑟)
21	15	oveqd 6667	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 × 𝑦) = (𝑥(.r‘𝑊)𝑦))
22	16, 20, 21	oveq123d 6671	. . . . . . . 8 ⊢ (𝜑 → (𝑟 · (𝑥 × 𝑦)) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))
23	19, 22	eqeq12d 2637	. . . . . . 7 ⊢ (𝜑 → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ↔ ((𝑟( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦))))
24		eqidd 2623	. . . . . . . . 9 ⊢ (𝜑 → 𝑥 = 𝑥)
25	16	oveqd 6667	. . . . . . . . 9 ⊢ (𝜑 → (𝑟 · 𝑦) = (𝑟( ·𝑠 ‘𝑊)𝑦))
26	15, 24, 25	oveq123d 6671	. . . . . . . 8 ⊢ (𝜑 → (𝑥 × (𝑟 · 𝑦)) = (𝑥(.r‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑦)))
27	26, 22	eqeq12d 2637	. . . . . . 7 ⊢ (𝜑 → ((𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)) ↔ (𝑥(.r‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑦)) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦))))
28	23, 27	anbi12d 747	. . . . . 6 ⊢ (𝜑 → ((((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ (((𝑟( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑦)) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
29	14, 28	raleqbidv 3152	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑦)) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
30	14, 29	raleqbidv 3152	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑦)) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
31	13, 30	raleqbidv 3152	. . 3 ⊢ (𝜑 → (∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑦)) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
32	10, 31	mpbid 222	. 2 ⊢ (𝜑 → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑦)) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦))))
33		eqid 2622	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
34		eqid 2622	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
35		eqid 2622	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
36		eqid 2622	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
37		eqid 2622	. . 3 ⊢ (.r‘𝑊) = (.r‘𝑊)
38	33, 34, 35, 36, 37	isassa 19315	. 2 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ (Scalar‘𝑊) ∈ CRing) ∧ ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑦)) = (𝑟( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
39	6, 32, 38	sylanbrc 698	1 ⊢ (𝜑 → 𝑊 ∈ AssAlg)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  ._rcmulr 15942  Scalarcsca 15944   ·_𝑠 cvsca 15945  Ringcrg 18547  CRingccrg 18548  LModclmod 18863  AssAlgcasa 19309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-assa 19312

This theorem is referenced by:  issubassa  19324  sraassa  19325  psrassa  19414  zlmassa  19872  matassa  20250  mendassa  37764