This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem phlstr

Description: A constructed pre-Hilbert space is a structure. Starting from lmodstr (which has 4 members), we chain strleun once more, adding an ordered pair to the function, to get all 5 members. (Contributed by Mario Carneiro, 1-Oct-2013) (Revised by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypothesis phlfn.h ⊢ 𝐻 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑇 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } )
Assertion phlstr 𝐻 Struct ⟨ 1 , 8 ⟩

Proof

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 ⟩