Step |
Hyp |
Ref |
Expression |
1 |
|
algpart.a |
⊢ 𝐴 = ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 } ) |
2 |
|
eqid |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } |
3 |
2
|
rngstr |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } Struct 〈 1 , 3 〉 |
4 |
|
5nn |
⊢ 5 ∈ ℕ |
5 |
|
scandx |
⊢ ( Scalar ‘ ndx ) = 5 |
6 |
|
5lt6 |
⊢ 5 < 6 |
7 |
|
6nn |
⊢ 6 ∈ ℕ |
8 |
|
vscandx |
⊢ ( ·𝑠 ‘ ndx ) = 6 |
9 |
4 5 6 7 8
|
strle2 |
⊢ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 } Struct 〈 5 , 6 〉 |
10 |
|
3lt5 |
⊢ 3 < 5 |
11 |
3 9 10
|
strleun |
⊢ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 } ) Struct 〈 1 , 6 〉 |
12 |
1 11
|
eqbrtri |
⊢ 𝐴 Struct 〈 1 , 6 〉 |