| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } |
| 2 |
1
|
rngstr |
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } Struct ⟨ 1 , 3 ⟩ |
| 3 |
|
5nn |
⊢ 5 ∈ ℕ |
| 4 |
|
scandx |
⊢ ( Scalar ‘ ndx ) = 5 |
| 5 |
|
5lt6 |
⊢ 5 < 6 |
| 6 |
|
6nn |
⊢ 6 ∈ ℕ |
| 7 |
|
vscandx |
⊢ ( ·𝑠 ‘ ndx ) = 6 |
| 8 |
|
6lt9 |
⊢ 6 < 9 |
| 9 |
|
9nn |
⊢ 9 ∈ ℕ |
| 10 |
|
tsetndx |
⊢ ( TopSet ‘ ndx ) = 9 |
| 11 |
3 4 5 6 7 8 9 10
|
strle3 |
⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } Struct ⟨ 5 , 9 ⟩ |
| 12 |
|
3lt5 |
⊢ 3 < 5 |
| 13 |
2 11 12
|
strleun |
⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) Struct ⟨ 1 , 9 ⟩ |