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	⊢ ( 𝜑 → 𝐴 = 𝑇 )