Metamath Proof Explorer


Theorem imasvalstr

Description: An image structure 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 ⟩