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 ⟩