assaass - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > assaass		GIF version

Theorem assaass 14987

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

**Hypotheses**
Ref	Expression
isassa.v	⊢ 𝑉 = (Base‘𝑊)
isassa.f	⊢ 𝐹 = (Scalar‘𝑊)
isassa.b	⊢ 𝐵 = (Base‘𝐹)
isassa.s	⊢ · = ( ·_𝑠 ‘𝑊)
isassa.t	⊢ × = (._r‘𝑊)

**Assertion**
Ref	Expression
assaass	⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))

**Proof of Theorem assaass**
Step	Hyp	Ref	Expression
1		isassa.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
2		isassa.f	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
3		isassa.b	. . 3 ⊢ 𝐵 = (Base‘𝐹)
4		isassa.s	. . 3 ⊢ · = ( ·_𝑠 ‘𝑊)
5		isassa.t	. . 3 ⊢ × = (._r‘𝑊)
6	1, 2, 3, 4, 5	assalem 14986	. 2 ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))
7	6	simpld 112	1 ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 ‘cfv 5375 (class class class)co 6079 Basecbs 13335 ._rcmulr 13415 Scalarcsca 13417 ·_𝑠 cvsca 13418 AssAlgcasa 14979

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4247 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-cnex 8264 ax-resscn 8265 ax-1re 8267 ax-addrcl 8270

This theorem depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ral 2533 df-rex 2534 df-rab 2537 df-v 2823 df-sbc 3052 df-un 3224 df-in 3226 df-ss 3233 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-br 4129 df-opab 4191 df-mpt 4192 df-id 4436 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-iota 5335 df-fun 5377 df-fn 5378 df-fv 5383 df-ov 6082 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-5 9349 df-6 9350 df-ndx 13338 df-slot 13339 df-mulr 13428 df-sca 13430 df-vsca 13431 df-assa 14982

This theorem is referenced by: assa2ass 14992 assa2ass2 14993 issubassa3 14995 asclmul1 15012 assamulgscmlem2 15025

W3C validator