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 φU=BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙𝑖ndx,˙TopSetndxOndxLdistndxDHomndxHcompndx˙
prdsbaslem.1 A=EU
prdsbaslem.2 E=SlotEndx
prdsbaslem.3 φTV
prdsbaslem.4 EndxTBasendxB+ndx+˙ndx×˙ScalarndxSndx·˙𝑖ndx,˙TopSetndxOndxLdistndxDHomndxHcompndx˙
Assertion prdsbaslem φA=T

Proof

Step Hyp Ref Expression
1 prdsbaslem.u φU=BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙𝑖ndx,˙TopSetndxOndxLdistndxDHomndxHcompndx˙
2 prdsbaslem.1 A=EU
3 prdsbaslem.2 E=SlotEndx
4 prdsbaslem.3 φTV
5 prdsbaslem.4 EndxTBasendxB+ndx+˙ndx×˙ScalarndxSndx·˙𝑖ndx,˙TopSetndxOndxLdistndxDHomndxHcompndx˙
6 prdsvalstr BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙𝑖ndx,˙TopSetndxOndxLdistndxDHomndxHcompndx˙Struct115
7 1 6 3 5 4 2 strfv3 φA=T