Step |
Hyp |
Ref |
Expression |
1 |
|
imasvalstr.u |
⊢ 𝑈 = ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 , 〈 ( ·𝑖 ‘ ndx ) , , 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , 𝑂 〉 , 〈 ( le ‘ ndx ) , 𝐿 〉 , 〈 ( dist ‘ ndx ) , 𝐷 〉 } ) |
2 |
|
eqid |
⊢ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 , 〈 ( ·𝑖 ‘ ndx ) , , 〉 } ) = ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 , 〈 ( ·𝑖 ‘ ndx ) , , 〉 } ) |
3 |
2
|
ipsstr |
⊢ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 , 〈 ( ·𝑖 ‘ ndx ) , , 〉 } ) Struct 〈 1 , 8 〉 |
4 |
|
9nn |
⊢ 9 ∈ ℕ |
5 |
|
tsetndx |
⊢ ( TopSet ‘ ndx ) = 9 |
6 |
|
9lt10 |
⊢ 9 < ; 1 0 |
7 |
|
10nn |
⊢ ; 1 0 ∈ ℕ |
8 |
|
plendx |
⊢ ( le ‘ ndx ) = ; 1 0 |
9 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
10 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
11 |
|
2nn |
⊢ 2 ∈ ℕ |
12 |
|
2pos |
⊢ 0 < 2 |
13 |
9 10 11 12
|
declt |
⊢ ; 1 0 < ; 1 2 |
14 |
9 11
|
decnncl |
⊢ ; 1 2 ∈ ℕ |
15 |
|
dsndx |
⊢ ( dist ‘ ndx ) = ; 1 2 |
16 |
4 5 6 7 8 13 14 15
|
strle3 |
⊢ { 〈 ( TopSet ‘ ndx ) , 𝑂 〉 , 〈 ( le ‘ ndx ) , 𝐿 〉 , 〈 ( dist ‘ ndx ) , 𝐷 〉 } Struct 〈 9 , ; 1 2 〉 |
17 |
|
8lt9 |
⊢ 8 < 9 |
18 |
3 16 17
|
strleun |
⊢ ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 , 〈 ( ·𝑖 ‘ ndx ) , , 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , 𝑂 〉 , 〈 ( le ‘ ndx ) , 𝐿 〉 , 〈 ( dist ‘ ndx ) , 𝐷 〉 } ) Struct 〈 1 , ; 1 2 〉 |
19 |
1 18
|
eqbrtri |
⊢ 𝑈 Struct 〈 1 , ; 1 2 〉 |