Theorem imasvalstr

Description: Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 30-Apr-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypothesis	imasvalstr.u	⊢ 𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
Assertion	imasvalstr	⊢ 𝑈 Struct ⟨ 1 , ; 1 2 ⟩

Proof

Step	Hyp	Ref	Expression
1		imasvalstr.u	⊢ 𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
2		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } )
3	2	ipsstr	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) Struct ⟨ 1 , 8 ⟩
4		9nn	⊢ 9 ∈ ℕ
5		tsetndx	⊢ ( TopSet ‘ ndx ) = 9
6		9lt10	⊢ 9 < ; 1 0
7		10nn	⊢ ; 1 0 ∈ ℕ
8		plendx	⊢ ( le ‘ ndx ) = ; 1 0
9		1nn0	⊢ 1 ∈ ℕ0
10		0nn0	⊢ 0 ∈ ℕ0
11		2nn	⊢ 2 ∈ ℕ
12		2pos	⊢ 0 < 2
13	9 10 11 12	declt	⊢ ; 1 0 < ; 1 2
14	9 11	decnncl	⊢ ; 1 2 ∈ ℕ
15		dsndx	⊢ ( dist ‘ ndx ) = ; 1 2
16	4 5 6 7 8 13 14 15	strle3	⊢ { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } Struct ⟨ 9 , ; 1 2 ⟩
17		8lt9	⊢ 8 < 9
18	3 16 17	strleun	⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ) Struct ⟨ 1 , ; 1 2 ⟩
19	1 18	eqbrtri	⊢ 𝑈 Struct ⟨ 1 , ; 1 2 ⟩