Step |
Hyp |
Ref |
Expression |
1 |
|
phlfn.h |
⊢ 𝐻 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) |
2 |
|
df-pr |
⊢ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } = ( { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ∪ { ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) |
3 |
2
|
uneq2i |
⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ ( { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ∪ { ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ) |
4 |
|
unass |
⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) ∪ { ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ ( { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ∪ { ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ) |
5 |
3 1 4
|
3eqtr4i |
⊢ 𝐻 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) ∪ { ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) |
6 |
|
eqid |
⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) |
7 |
6
|
lmodstr |
⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) Struct ⟨ 1 , 6 ⟩ |
8 |
|
8nn |
⊢ 8 ∈ ℕ |
9 |
|
ipndx |
⊢ ( ·𝑖 ‘ ndx ) = 8 |
10 |
8 9
|
strle1 |
⊢ { ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } Struct ⟨ 8 , 8 ⟩ |
11 |
|
6lt8 |
⊢ 6 < 8 |
12 |
7 10 11
|
strleun |
⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) ∪ { ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) Struct ⟨ 1 , 8 ⟩ |
13 |
5 12
|
eqbrtri |
⊢ 𝐻 Struct ⟨ 1 , 8 ⟩ |