Step |
Hyp |
Ref |
Expression |
1 |
|
ipspart.a |
⊢ 𝐴 = ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 , 〈 ( ·𝑖 ‘ ndx ) , 𝐼 〉 } ) |
2 |
1
|
ipsstr |
⊢ 𝐴 Struct 〈 1 , 8 〉 |
3 |
|
baseid |
⊢ Base = Slot ( Base ‘ ndx ) |
4 |
|
snsstp1 |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 } ⊆ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } |
5 |
|
ssun1 |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ⊆ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , · 〉 , 〈 ( ·𝑖 ‘ ndx ) , 𝐼 〉 } ) |
6 |
5 1
|
sseqtrri |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( .r ‘ ndx ) , × 〉 } ⊆ 𝐴 |
7 |
4 6
|
sstri |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 } ⊆ 𝐴 |
8 |
2 3 7
|
strfv |
⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐴 ) ) |