Theorem List for Intuitionistic Logic Explorer - 11601-11700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | strslssd 11601 |
Deduction version of strslss 11602. (Contributed by Mario Carneiro,
15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by
Jim Kingdon, 31-Jan-2023.)
|
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝜑 → 𝑇 ∈ 𝑉)
& ⊢ (𝜑 → Fun 𝑇)
& ⊢ (𝜑 → 𝑆 ⊆ 𝑇)
& ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆)) |
|
Theorem | strslss 11602 |
Propagate component extraction to a structure 𝑇 from a subset
structure 𝑆. (Contributed by Mario Carneiro,
11-Oct-2013.)
(Revised by Jim Kingdon, 31-Jan-2023.)
|
⊢ 𝑇 ∈ V & ⊢ Fun 𝑇 & ⊢ 𝑆 ⊆ 𝑇
& ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆 ⇒ ⊢ (𝐸‘𝑇) = (𝐸‘𝑆) |
|
Theorem | strsl0 11603 |
All components of the empty set are empty sets. (Contributed by Stefan
O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.)
|
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈
ℕ) ⇒ ⊢ ∅ = (𝐸‘∅) |
|
Theorem | base0 11604 |
The base set of the empty structure. (Contributed by David A. Wheeler,
7-Jul-2016.)
|
⊢ ∅ =
(Base‘∅) |
|
Theorem | setsslid 11605 |
Value of the structure replacement function at a replaced index.
(Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon,
24-Jan-2023.)
|
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈
ℕ) ⇒ ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉))) |
|
Theorem | setsslnid 11606 |
Value of the structure replacement function at an untouched index.
(Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon,
24-Jan-2023.)
|
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝐸‘ndx) ≠ 𝐷 & ⊢ 𝐷 ∈
ℕ ⇒ ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
|
Theorem | baseval 11607 |
Value of the base set extractor. (Normally it is preferred to work with
(Base‘ndx) rather than the hard-coded
1 in order to make
structure theorems portable. This is an example of how to obtain it
when needed.) (New usage is discouraged.) (Contributed by NM,
4-Sep-2011.)
|
⊢ 𝐾 ∈ V ⇒ ⊢ (Base‘𝐾) = (𝐾‘1) |
|
Theorem | baseid 11608 |
Utility theorem: index-independent form of df-base 11561. (Contributed by
NM, 20-Oct-2012.)
|
⊢ Base = Slot
(Base‘ndx) |
|
Theorem | basendx 11609 |
Index value of the base set extractor. (Normally it is preferred to work
with (Base‘ndx) rather than the hard-coded
1 in order to make
structure theorems portable. This is an example of how to obtain it when
needed.) (New usage is discouraged.) (Contributed by Mario Carneiro,
2-Aug-2013.)
|
⊢ (Base‘ndx) = 1 |
|
Theorem | basendxnn 11610 |
The index value of the base set extractor is a positive integer. This
property should be ensured for every concrete coding because otherwise it
could not be used in an extensible structure (slots must be positive
integers). (Contributed by AV, 23-Sep-2020.)
|
⊢ (Base‘ndx) ∈
ℕ |
|
Theorem | baseslid 11611 |
The base set extractor is a slot. (Contributed by Jim Kingdon,
31-Jan-2023.)
|
⊢ (Base = Slot (Base‘ndx) ∧
(Base‘ndx) ∈ ℕ) |
|
Theorem | basfn 11612 |
The base set extractor is a function on V.
(Contributed by Stefan
O'Rear, 8-Jul-2015.)
|
⊢ Base Fn V |
|
Theorem | reldmress 11613 |
The structure restriction is a proper operator, so it can be used with
ovprc1 5699. (Contributed by Stefan O'Rear,
29-Nov-2014.)
|
⊢ Rel dom ↾s |
|
Theorem | ressid2 11614 |
General behavior of trivial restriction. (Contributed by Stefan O'Rear,
29-Nov-2014.) (Revised by Jim Kingdon, 26-Jan-2023.)
|
⊢ 𝑅 = (𝑊 ↾s 𝐴)
& ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) |
|
Theorem | ressval2 11615 |
Value of nontrivial structure restriction. (Contributed by Stefan
O'Rear, 29-Nov-2014.)
|
⊢ 𝑅 = (𝑊 ↾s 𝐴)
& ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
|
Theorem | ressid 11616 |
Behavior of trivial restriction. (Contributed by Stefan O'Rear,
29-Nov-2014.)
|
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊) |
|
5.1.2 Slot definitions
|
|
Syntax | cplusg 11617 |
Extend class notation with group (addition) operation.
|
class +g |
|
Syntax | cmulr 11618 |
Extend class notation with ring multiplication.
|
class .r |
|
Syntax | cstv 11619 |
Extend class notation with involution.
|
class *𝑟 |
|
Syntax | csca 11620 |
Extend class notation with scalar field.
|
class Scalar |
|
Syntax | cvsca 11621 |
Extend class notation with scalar product.
|
class
·𝑠 |
|
Syntax | cip 11622 |
Extend class notation with Hermitian form (inner product).
|
class
·𝑖 |
|
Syntax | cts 11623 |
Extend class notation with the topology component of a topological
space.
|
class TopSet |
|
Syntax | cple 11624 |
Extend class notation with "less than or equal to" for posets.
|
class le |
|
Syntax | coc 11625 |
Extend class notation with the class of orthocomplementation
extractors.
|
class oc |
|
Syntax | cds 11626 |
Extend class notation with the metric space distance function.
|
class dist |
|
Syntax | cunif 11627 |
Extend class notation with the uniform structure.
|
class UnifSet |
|
Syntax | chom 11628 |
Extend class notation with the hom-set structure.
|
class Hom |
|
Syntax | cco 11629 |
Extend class notation with the composition operation.
|
class comp |
|
Definition | df-plusg 11630 |
Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
⊢ +g = Slot 2 |
|
Definition | df-mulr 11631 |
Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
⊢ .r = Slot 3 |
|
Definition | df-starv 11632 |
Define the involution function of a *-ring. (Contributed by NM,
4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ *𝑟 = Slot
4 |
|
Definition | df-sca 11633 |
Define scalar field component of a vector space 𝑣. (Contributed by
NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ Scalar = Slot 5 |
|
Definition | df-vsca 11634 |
Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
⊢ ·𝑠 = Slot
6 |
|
Definition | df-ip 11635 |
Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ ·𝑖 = Slot
8 |
|
Definition | df-tset 11636 |
Define the topology component of a topological space (structure).
(Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro,
14-Aug-2015.)
|
⊢ TopSet = Slot 9 |
|
Definition | df-ple 11637 |
Define "less than or equal to" ordering extractor for posets and
related
structures. We use ;10 for the index to avoid conflict with 1
through 9 used for other purposes. (Contributed
by NM, 4-Sep-2011.)
(Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|
⊢ le = Slot ;10 |
|
Definition | df-ocomp 11638 |
Define the orthocomplementation extractor for posets and related
structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro,
14-Aug-2015.)
|
⊢ oc = Slot ;11 |
|
Definition | df-ds 11639 |
Define the distance function component of a metric space (structure).
(Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro,
14-Aug-2015.)
|
⊢ dist = Slot ;12 |
|
Definition | df-unif 11640 |
Define the uniform structure component of a uniform space. (Contributed
by Mario Carneiro, 14-Aug-2015.)
|
⊢ UnifSet = Slot ;13 |
|
Definition | df-hom 11641 |
Define the hom-set component of a category. (Contributed by Mario
Carneiro, 2-Jan-2017.)
|
⊢ Hom = Slot ;14 |
|
Definition | df-cco 11642 |
Define the composition operation of a category. (Contributed by Mario
Carneiro, 2-Jan-2017.)
|
⊢ comp = Slot ;15 |
|
Theorem | strleund 11643 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
⊢ (𝜑 → 𝐹 Struct 〈𝐴, 𝐵〉) & ⊢ (𝜑 → 𝐺 Struct 〈𝐶, 𝐷〉) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉) |
|
Theorem | strleun 11644 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.)
|
⊢ 𝐹 Struct 〈𝐴, 𝐵〉 & ⊢ 𝐺 Struct 〈𝐶, 𝐷〉 & ⊢ 𝐵 < 𝐶 ⇒ ⊢ (𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉 |
|
Theorem | strle1g 11645 |
Make a structure from a singleton. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 ⇒ ⊢ (𝑋 ∈ 𝑉 → {〈𝐴, 𝑋〉} Struct 〈𝐼, 𝐼〉) |
|
Theorem | strle2g 11646 |
Make a structure from a pair. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼
& ⊢ 𝐼 < 𝐽
& ⊢ 𝐽 ∈ ℕ & ⊢ 𝐵 = 𝐽 ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉} Struct 〈𝐼, 𝐽〉) |
|
Theorem | strle3g 11647 |
Make a structure from a triple. (Contributed by Mario Carneiro,
29-Aug-2015.)
|
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼
& ⊢ 𝐼 < 𝐽
& ⊢ 𝐽 ∈ ℕ & ⊢ 𝐵 = 𝐽
& ⊢ 𝐽 < 𝐾
& ⊢ 𝐾 ∈ ℕ & ⊢ 𝐶 = 𝐾 ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑃) → {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉, 〈𝐶, 𝑍〉} Struct 〈𝐼, 𝐾〉) |
|
Theorem | plusgndx 11648 |
Index value of the df-plusg 11630 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
⊢ (+g‘ndx) =
2 |
|
Theorem | plusgid 11649 |
Utility theorem: index-independent form of df-plusg 11630. (Contributed by
NM, 20-Oct-2012.)
|
⊢ +g = Slot
(+g‘ndx) |
|
Theorem | plusgslid 11650 |
Slot property of +g. (Contributed by Jim
Kingdon, 3-Feb-2023.)
|
⊢ (+g = Slot
(+g‘ndx) ∧ (+g‘ndx) ∈
ℕ) |
|
Theorem | opelstrsl 11651 |
The slot of a structure which contains an ordered pair for that slot.
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝜑 → 𝑆 Struct 𝑋)
& ⊢ (𝜑 → 𝑉 ∈ 𝑌)
& ⊢ (𝜑 → 〈(𝐸‘ndx), 𝑉〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑉 = (𝐸‘𝑆)) |
|
Theorem | opelstrbas 11652 |
The base set of a structure with a base set. (Contributed by AV,
10-Nov-2021.)
|
⊢ (𝜑 → 𝑆 Struct 𝑋)
& ⊢ (𝜑 → 𝑉 ∈ 𝑌)
& ⊢ (𝜑 → 〈(Base‘ndx), 𝑉〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑉 = (Base‘𝑆)) |
|
Theorem | 1strstrg 11653 |
A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
(Revised by Jim Kingdon, 28-Jan-2023.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐺 Struct 〈1, 1〉) |
|
Theorem | 1strbas 11654 |
The base set of a constructed one-slot structure. (Contributed by AV,
27-Mar-2020.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) |
|
Theorem | 2strstrg 11655 |
A constructed two-slot structure. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁
& ⊢ 1 < 𝑁
& ⊢ 𝑁 ∈ ℕ
⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct 〈1, 𝑁〉) |
|
Theorem | 2strbasg 11656 |
The base set of a constructed two-slot structure. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁
& ⊢ 1 < 𝑁
& ⊢ 𝑁 ∈ ℕ
⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺)) |
|
Theorem | 2stropg 11657 |
The other slot of a constructed two-slot structure. (Contributed by
Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁
& ⊢ 1 < 𝑁
& ⊢ 𝑁 ∈ ℕ
⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (𝐸‘𝐺)) |
|
Theorem | 2strstr1g 11658 |
A constructed two-slot structure. Version of 2strstrg 11655 not depending
on the hard-coded index value of the base set. (Contributed by AV,
22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢
(Base‘ndx) < 𝑁
& ⊢ 𝑁 ∈ ℕ
⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct 〈(Base‘ndx), 𝑁〉) |
|
Theorem | 2strbas1g 11659 |
The base set of a constructed two-slot structure. Version of 2strbasg 11656
not depending on the hard-coded index value of the base set.
(Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon,
2-Feb-2023.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢
(Base‘ndx) < 𝑁
& ⊢ 𝑁 ∈ ℕ
⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺)) |
|
Theorem | 2strop1g 11660 |
The other slot of a constructed two-slot structure. Version of
2stropg 11657 not depending on the hard-coded index value
of the base set.
(Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon,
2-Feb-2023.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢
(Base‘ndx) < 𝑁
& ⊢ 𝑁 ∈ ℕ & ⊢ 𝐸 = Slot 𝑁 ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (𝐸‘𝐺)) |
|
Theorem | basendxnplusgndx 11661 |
The slot for the base set is not the slot for the group operation in an
extensible structure. (Contributed by AV, 14-Nov-2021.)
|
⊢ (Base‘ndx) ≠
(+g‘ndx) |
|
Theorem | grpstrg 11662 |
A constructed group is a structure on 1...2.
(Contributed by
Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), +
〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct 〈1, 2〉) |
|
Theorem | grpbaseg 11663 |
The base set of a constructed group. (Contributed by Mario Carneiro,
2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), +
〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺)) |
|
Theorem | grpplusgg 11664 |
The operation of a constructed group. (Contributed by Mario Carneiro,
2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), +
〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + =
(+g‘𝐺)) |
|
Theorem | mulrndx 11665 |
Index value of the df-mulr 11631 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
⊢ (.r‘ndx) =
3 |
|
Theorem | mulrid 11666 |
Utility theorem: index-independent form of df-mulr 11631. (Contributed by
Mario Carneiro, 8-Jun-2013.)
|
⊢ .r = Slot
(.r‘ndx) |
|
Theorem | mulrslid 11667 |
Slot property of .r. (Contributed by Jim
Kingdon, 3-Feb-2023.)
|
⊢ (.r = Slot
(.r‘ndx) ∧ (.r‘ndx) ∈
ℕ) |
|
Theorem | plusgndxnmulrndx 11668 |
The slot for the group (addition) operation is not the slot for the ring
(multiplication) operation in an extensible structure. (Contributed by
AV, 16-Feb-2020.)
|
⊢ (+g‘ndx) ≠
(.r‘ndx) |
|
Theorem | basendxnmulrndx 11669 |
The slot for the base set is not the slot for the ring (multiplication)
operation in an extensible structure. (Contributed by AV,
16-Feb-2020.)
|
⊢ (Base‘ndx) ≠
(.r‘ndx) |
|
Theorem | rngstrg 11670 |
A constructed ring is a structure. (Contributed by Mario Carneiro,
28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
⊢ 𝑅 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), ·
〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → 𝑅 Struct 〈1, 3〉) |
|
Theorem | rngbaseg 11671 |
The base set of a constructed ring. (Contributed by Mario Carneiro,
2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
⊢ 𝑅 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), ·
〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → 𝐵 = (Base‘𝑅)) |
|
Theorem | rngplusgg 11672 |
The additive operation of a constructed ring. (Contributed by Mario
Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
⊢ 𝑅 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), ·
〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → + =
(+g‘𝑅)) |
|
Theorem | rngmulrg 11673 |
The multiplicative operation of a constructed ring. (Contributed by
Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
⊢ 𝑅 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), ·
〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → · =
(.r‘𝑅)) |
|
Theorem | starvndx 11674 |
Index value of the df-starv 11632 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
⊢ (*𝑟‘ndx) =
4 |
|
Theorem | starvid 11675 |
Utility theorem: index-independent form of df-starv 11632. (Contributed by
Mario Carneiro, 6-Oct-2013.)
|
⊢ *𝑟 = Slot
(*𝑟‘ndx) |
|
Theorem | starvslid 11676 |
Slot property of *𝑟. (Contributed
by Jim Kingdon, 4-Feb-2023.)
|
⊢ (*𝑟 = Slot
(*𝑟‘ndx) ∧ (*𝑟‘ndx)
∈ ℕ) |
|
Theorem | srngstrd 11677 |
A constructed star ring is a structure. (Contributed by Mario Carneiro,
18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), · 〉} ∪
{〈(*𝑟‘ndx), ∗
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → · ∈ 𝑋) & ⊢ (𝜑 → ∗ ∈ 𝑌)
⇒ ⊢ (𝜑 → 𝑅 Struct 〈1, 4〉) |
|
Theorem | srngbased 11678 |
The base set of a constructed star ring. (Contributed by Mario
Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), · 〉} ∪
{〈(*𝑟‘ndx), ∗
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → · ∈ 𝑋) & ⊢ (𝜑 → ∗ ∈ 𝑌)
⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
|
Theorem | srngplusgd 11679 |
The addition operation of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), · 〉} ∪
{〈(*𝑟‘ndx), ∗
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → · ∈ 𝑋) & ⊢ (𝜑 → ∗ ∈ 𝑌)
⇒ ⊢ (𝜑 → + =
(+g‘𝑅)) |
|
Theorem | srngmulrd 11680 |
The multiplication operation of a constructed star ring. (Contributed
by Mario Carneiro, 20-Jun-2015.)
|
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), · 〉} ∪
{〈(*𝑟‘ndx), ∗
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → · ∈ 𝑋) & ⊢ (𝜑 → ∗ ∈ 𝑌)
⇒ ⊢ (𝜑 → · =
(.r‘𝑅)) |
|
Theorem | srnginvld 11681 |
The involution function of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.)
|
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), · 〉} ∪
{〈(*𝑟‘ndx), ∗
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → · ∈ 𝑋) & ⊢ (𝜑 → ∗ ∈ 𝑌)
⇒ ⊢ (𝜑 → ∗ =
(*𝑟‘𝑅)) |
|
Theorem | scandx 11682 |
Index value of the df-sca 11633 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
⊢ (Scalar‘ndx) = 5 |
|
Theorem | scaid 11683 |
Utility theorem: index-independent form of scalar df-sca 11633. (Contributed
by Mario Carneiro, 19-Jun-2014.)
|
⊢ Scalar = Slot
(Scalar‘ndx) |
|
Theorem | scaslid 11684 |
Slot property of Scalar. (Contributed by Jim Kingdon,
5-Feb-2023.)
|
⊢ (Scalar = Slot (Scalar‘ndx) ∧
(Scalar‘ndx) ∈ ℕ) |
|
Theorem | vscandx 11685 |
Index value of the df-vsca 11634 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
⊢ ( ·𝑠
‘ndx) = 6 |
|
Theorem | vscaid 11686 |
Utility theorem: index-independent form of scalar product df-vsca 11634.
(Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
⊢ ·𝑠 = Slot
( ·𝑠 ‘ndx) |
|
Theorem | vscaslid 11687 |
Slot property of ·𝑠.
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
⊢ ( ·𝑠 = Slot
( ·𝑠 ‘ndx) ∧ (
·𝑠 ‘ndx) ∈
ℕ) |
|
Theorem | lmodstrd 11688 |
A constructed left module or left vector space is a structure.
(Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Jim Kingdon,
5-Feb-2023.)
|
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝐹〉} ∪ {〈(
·𝑠 ‘ndx), ·
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑍)
⇒ ⊢ (𝜑 → 𝑊 Struct 〈1, 6〉) |
|
Theorem | lmodbased 11689 |
The base set of a constructed left vector space. (Contributed by Mario
Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝐹〉} ∪ {〈(
·𝑠 ‘ndx), ·
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑍)
⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑊)) |
|
Theorem | lmodplusgd 11690 |
The additive operation of a constructed left vector space. (Contributed
by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon,
6-Feb-2023.)
|
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝐹〉} ∪ {〈(
·𝑠 ‘ndx), ·
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑍)
⇒ ⊢ (𝜑 → + =
(+g‘𝑊)) |
|
Theorem | lmodscad 11691 |
The set of scalars of a constructed left vector space. (Contributed by
Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝐹〉} ∪ {〈(
·𝑠 ‘ndx), ·
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑍)
⇒ ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) |
|
Theorem | lmodvscad 11692 |
The scalar product operation of a constructed left vector space.
(Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝐹〉} ∪ {〈(
·𝑠 ‘ndx), ·
〉})
& ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑍)
⇒ ⊢ (𝜑 → · = (
·𝑠 ‘𝑊)) |
|
Theorem | ipndx 11693 |
Index value of the df-ip 11635 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
⊢
(·𝑖‘ndx) = 8 |
|
Theorem | ipid 11694 |
Utility theorem: index-independent form of df-ip 11635. (Contributed by
Mario Carneiro, 6-Oct-2013.)
|
⊢ ·𝑖 = Slot
(·𝑖‘ndx) |
|
Theorem | ipslid 11695 |
Slot property of ·𝑖.
(Contributed by Jim Kingdon, 7-Feb-2023.)
|
⊢ (·𝑖 = Slot
(·𝑖‘ndx) ∧
(·𝑖‘ndx) ∈
ℕ) |
|
Theorem | ipsstrd 11696 |
A constructed inner product space is a structure. (Contributed by
Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), 𝐼〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → × ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐴 Struct 〈1, 8〉) |
|
Theorem | ipsbased 11697 |
The base set of a constructed inner product space. (Contributed by
Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), 𝐼〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → × ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐴)) |
|
Theorem | ipsaddgd 11698 |
The additive operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), 𝐼〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → × ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) ⇒ ⊢ (𝜑 → + =
(+g‘𝐴)) |
|
Theorem | ipsmulrd 11699 |
The multiplicative operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), 𝐼〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → × ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) ⇒ ⊢ (𝜑 → × =
(.r‘𝐴)) |
|
Theorem | ipsscad 11700 |
The set of scalars of a constructed inner product space. (Contributed
by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
8-Feb-2023.)
|
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), 𝐼〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → + ∈ 𝑊)
& ⊢ (𝜑 → × ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌)
& ⊢ (𝜑 → · ∈ 𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝑆 = (Scalar‘𝐴)) |