Home | Intuitionistic Logic Explorer Theorem List (p. 122 of 135) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2strstr1g 12101 | A constructed two-slot structure. Version of 2strstrg 12098 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 12102 | The base set of a constructed two-slot structure. Version of 2strbasg 12099 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 12103 | The other slot of a constructed two-slot structure. Version of 2stropg 12100 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 12104 | 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 12105 | 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 12106 | 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 12107 | 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 12108 | Index value of the df-mulr 12074 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (.r‘ndx) = 3 | ||
Theorem | mulrid 12109 | Utility theorem: index-independent form of df-mulr 12074. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ .r = Slot (.r‘ndx) | ||
Theorem | mulrslid 12110 | Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.) |
⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ) | ||
Theorem | plusgndxnmulrndx 12111 | 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 12112 | 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 12113 | 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 12114 | 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 12115 | 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 12116 | 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 12117 | Index value of the df-starv 12075 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (*𝑟‘ndx) = 4 | ||
Theorem | starvid 12118 | Utility theorem: index-independent form of df-starv 12075. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ *𝑟 = Slot (*𝑟‘ndx) | ||
Theorem | starvslid 12119 | Slot property of *𝑟. (Contributed by Jim Kingdon, 4-Feb-2023.) |
⊢ (*𝑟 = Slot (*𝑟‘ndx) ∧ (*𝑟‘ndx) ∈ ℕ) | ||
Theorem | srngstrd 12120 | 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 12121 | 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 12122 | 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 12123 | 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 12124 | The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → + ∈ 𝑊) & ⊢ (𝜑 → · ∈ 𝑋) & ⊢ (𝜑 → ∗ ∈ 𝑌) ⇒ ⊢ (𝜑 → ∗ = (*𝑟‘𝑅)) | ||
Theorem | scandx 12125 | Index value of the df-sca 12076 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (Scalar‘ndx) = 5 | ||
Theorem | scaid 12126 | Utility theorem: index-independent form of scalar df-sca 12076. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ Scalar = Slot (Scalar‘ndx) | ||
Theorem | scaslid 12127 | Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.) |
⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ) | ||
Theorem | vscandx 12128 | Index value of the df-vsca 12077 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ( ·𝑠 ‘ndx) = 6 | ||
Theorem | vscaid 12129 | Utility theorem: index-independent form of scalar product df-vsca 12077. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx) | ||
Theorem | vscaslid 12130 | Slot property of ·𝑠. (Contributed by Jim Kingdon, 5-Feb-2023.) |
⊢ ( ·𝑠 = Slot ( ·𝑠 ‘ndx) ∧ ( ·𝑠 ‘ndx) ∈ ℕ) | ||
Theorem | lmodstrd 12131 | 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 12132 | 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 12133 | 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 12134 | 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 12135 | 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 12136 | Index value of the df-ip 12078 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (·𝑖‘ndx) = 8 | ||
Theorem | ipid 12137 | Utility theorem: index-independent form of df-ip 12078. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ ·𝑖 = Slot (·𝑖‘ndx) | ||
Theorem | ipslid 12138 | Slot property of ·𝑖. (Contributed by Jim Kingdon, 7-Feb-2023.) |
⊢ (·𝑖 = Slot (·𝑖‘ndx) ∧ (·𝑖‘ndx) ∈ ℕ) | ||
Theorem | ipsstrd 12139 | 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 12140 | 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 12141 | 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 12142 | 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 12143 | 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‘𝐴)) | ||
Theorem | ipsvscad 12144 | The scalar product operation 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), 𝐼〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → + ∈ 𝑊) & ⊢ (𝜑 → × ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) & ⊢ (𝜑 → · ∈ 𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) ⇒ ⊢ (𝜑 → · = ( ·𝑠 ‘𝐴)) | ||
Theorem | ipsipd 12145 | The multiplicative operation 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), 𝐼〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → + ∈ 𝑊) & ⊢ (𝜑 → × ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) & ⊢ (𝜑 → · ∈ 𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐼 = (·𝑖‘𝐴)) | ||
Theorem | tsetndx 12146 | Index value of the df-tset 12079 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (TopSet‘ndx) = 9 | ||
Theorem | tsetid 12147 | Utility theorem: index-independent form of df-tset 12079. (Contributed by NM, 20-Oct-2012.) |
⊢ TopSet = Slot (TopSet‘ndx) | ||
Theorem | tsetslid 12148 | Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.) |
⊢ (TopSet = Slot (TopSet‘ndx) ∧ (TopSet‘ndx) ∈ ℕ) | ||
Theorem | topgrpstrd 12149 | A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → + ∈ 𝑊) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑊 Struct 〈1, 9〉) | ||
Theorem | topgrpbasd 12150 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → + ∈ 𝑊) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑊)) | ||
Theorem | topgrpplusgd 12151 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → + ∈ 𝑊) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) ⇒ ⊢ (𝜑 → + = (+g‘𝑊)) | ||
Theorem | topgrptsetd 12152 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → + ∈ 𝑊) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | plendx 12153 | Index value of the df-ple 12080 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ (le‘ndx) = ;10 | ||
Theorem | pleid 12154 | Utility theorem: self-referencing, index-independent form of df-ple 12080. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.) |
⊢ le = Slot (le‘ndx) | ||
Theorem | pleslid 12155 | Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.) |
⊢ (le = Slot (le‘ndx) ∧ (le‘ndx) ∈ ℕ) | ||
Theorem | dsndx 12156 | Index value of the df-ds 12082 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (dist‘ndx) = ;12 | ||
Theorem | dsid 12157 | Utility theorem: index-independent form of df-ds 12082. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ dist = Slot (dist‘ndx) | ||
Theorem | dsslid 12158 | Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.) |
⊢ (dist = Slot (dist‘ndx) ∧ (dist‘ndx) ∈ ℕ) | ||
Syntax | crest 12159 | Extend class notation with the function returning a subspace topology. |
class ↾t | ||
Syntax | ctopn 12160 | Extend class notation with the topology extractor function. |
class TopOpen | ||
Definition | df-rest 12161* | Function returning the subspace topology induced by the topology 𝑦 and the set 𝑥. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ↾t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥))) | ||
Definition | df-topn 12162 | Define the topology extractor function. This differs from df-tset 12079 when a structure has been restricted using df-ress 12006; in this case the TopSet component will still have a topology over the larger set, and this function fixes this by restricting the topology as well. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen = (𝑤 ∈ V ↦ ((TopSet‘𝑤) ↾t (Base‘𝑤))) | ||
Theorem | restfn 12163 | The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.) |
⊢ ↾t Fn (V × V) | ||
Theorem | topnfn 12164 | The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen Fn V | ||
Theorem | restval 12165* | The subspace topology induced by the topology 𝐽 on the set 𝐴. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) | ||
Theorem | elrest 12166* | The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))) | ||
Theorem | elrestr 12167 | Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽) → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) | ||
Theorem | restid2 12168 | The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽) | ||
Theorem | restsspw 12169 | The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 | ||
Theorem | restid 12170 | The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 𝑉 → (𝐽 ↾t 𝑋) = 𝐽) | ||
Theorem | topnvalg 12171 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑉 → (𝐽 ↾t 𝐵) = (TopOpen‘𝑊)) | ||
Theorem | topnidg 12172 | Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐵) → 𝐽 = (TopOpen‘𝑊)) | ||
Theorem | topnpropgd 12173 | The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon, 13-Feb-2023.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿)) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝐿 ∈ 𝑊) ⇒ ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) | ||
Syntax | ctg 12174 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 12175 | Extend class notation with a function whose value is a product topology. |
class ∏t | ||
Syntax | c0g 12176 | Extend class notation with group identity element. |
class 0g | ||
Syntax | cgsu 12177 | Extend class notation to include finitely supported group sums. |
class Σg | ||
Definition | df-0g 12178* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 12179. The related theorems will be provided later. (Contributed by NM, 20-Aug-2011.) |
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) | ||
Definition | df-gsum 12179* |
Define the group sum for the structure 𝐺 of a finite sequence of
elements whose values are defined by the expression 𝐵 and
whose set
of indices is 𝐴. It may be viewed as a product (if
𝐺
is a
multiplication), a sum (if 𝐺 is an addition) or any other
operation.
The variable 𝑘 is normally a free variable in 𝐵 (i.e.,
𝐵
can
be thought of as 𝐵(𝑘)). The definition is meaningful in
different contexts, depending on the size of the index set 𝐴 and
each demanding different properties of 𝐺.
1. If 𝐴 = ∅ and 𝐺 has an identity element, then the sum equals this identity. 2. If 𝐴 = (𝑀...𝑁) and 𝐺 is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e. (𝐵(1) + 𝐵(2)) + 𝐵(3) etc. 3. If 𝐴 is a finite set (or is nonzero for finitely many indices) and 𝐺 is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined. 4. If 𝐴 is an infinite set and 𝐺 is a Hausdorff topological group, then there is a meaningful sum, but Σg cannot handle this case. (Contributed by FL, 5-Sep-2010.) (Revised by FL, 17-Oct-2011.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))))) | ||
Definition | df-topgen 12180* | Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78. (Contributed by NM, 16-Jul-2006.) |
⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)}) | ||
Definition | df-pt 12181* | Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})) | ||
Syntax | cprds 12182 | The function constructing structure products. |
class Xs | ||
Syntax | cpws 12183 | The function constructing structure powers. |
class ↑s | ||
Definition | df-prds 12184* | Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) |
⊢ Xs = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({〈(Base‘ndx), 𝑣〉, 〈(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx), 𝑠〉, 〈( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))〉, 〈(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))〉, 〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}〉, 〈(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))〉} ∪ {〈(Hom ‘ndx), ℎ〉, 〈(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ (𝑐ℎ(2nd ‘𝑎)), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}))) | ||
Theorem | reldmprds 12185 | The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) |
⊢ Rel dom Xs | ||
Definition | df-pws 12186* | Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟}))) | ||
Syntax | cpsmet 12187 | Extend class notation with the class of all pseudometric spaces. |
class PsMet | ||
Syntax | cxmet 12188 | Extend class notation with the class of all extended metric spaces. |
class ∞Met | ||
Syntax | cmet 12189 | Extend class notation with the class of all metrics. |
class Met | ||
Syntax | cbl 12190 | Extend class notation with the metric space ball function. |
class ball | ||
Syntax | cfbas 12191 | Extend class definition to include the class of filter bases. |
class fBas | ||
Syntax | cfg 12192 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 12193 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 12194 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 12195* | Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) | ||
Definition | df-xmet 12196* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 12197, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) | ||
Definition | df-met 12197* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. (Contributed by NM, 25-Aug-2006.) |
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) | ||
Definition | df-bl 12198* | Define the metric space ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧})) | ||
Definition | df-mopn 12199 | Define a function whose value is the family of open sets of a metric space. (Contributed by NM, 1-Sep-2006.) |
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) | ||
Definition | df-fbas 12200* | Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.) |
⊢ fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |