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

Metamath Proof Explorer

Theorem prdsbaslem

Description: Lemma for prdsbas and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 12-Jul-2024)

Ref Expression
Hypotheses prdsbaslem.u ⊢ ( 𝜑 → 𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
prdsbaslem.1 ⊢ 𝐴 = ( 𝐸 ‘ 𝑈 )
prdsbaslem.2 ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
prdsbaslem.3 ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
prdsbaslem.4 ⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝑇 ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) )
Assertion prdsbaslem ( 𝜑 → 𝐴 = 𝑇 )

Proof

Step Hyp Ref Expression
1 prdsbaslem.u ⊢ ( 𝜑 → 𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
2 prdsbaslem.1 ⊢ 𝐴 = ( 𝐸 ‘ 𝑈 )
3 prdsbaslem.2 ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
4 prdsbaslem.3 ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
5 prdsbaslem.4 ⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝑇 ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) )
6 prdsvalstr ⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , 𝐿 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) Struct ⟨ 1 , 1 5 ⟩
7 1 6 3 5 4 2 strfv3 ⊢ ( 𝜑 → 𝐴 = 𝑇 )