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

Metamath Proof Explorer

Theorem estrreslem1

Description: Lemma 1 for estrres . (Contributed by AV, 14-Mar-2020) (Proof shortened by AV, 28-Oct-2024)

Ref Expression
Hypotheses estrres.c ⊢ φ → C = Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙
estrres.b ⊢ φ → B ∈ V
Assertion estrreslem1 ⊢ φ → B = Base C

Proof

Step Hyp Ref Expression
1 estrres.c ⊢ φ → C = Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙
2 estrres.b ⊢ φ → B ∈ V
3 1 fveq2d ⊢ φ → Base C = Base Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙
4 baseid ⊢ Base = Slot Base ndx
5 tpex ⊢ Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙ ∈ V
6 5 a1i ⊢ φ → Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙ ∈ V
7 4 6 strfvnd ⊢ φ → Base Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙ = Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙ ⁡ Base ndx
8 fvexd ⊢ φ → Base ndx ∈ V
9 slotsbhcdif ⊢ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx ∧ Hom ⁡ ndx ≠ comp ⁡ ndx
10 3simpa ⊢ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx ∧ Hom ⁡ ndx ≠ comp ⁡ ndx → Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx
11 9 10 mp1i ⊢ φ → Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx
12 fvtp1g ⊢ Base ndx ∈ V ∧ B ∈ V ∧ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx → Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙ ⁡ Base ndx = B
13 8 2 11 12 syl21anc ⊢ φ → Base ndx B Hom ⁡ ndx H comp ⁡ ndx · ˙ ⁡ Base ndx = B
14 3 7 13 3eqtrrd ⊢ φ → B = Base C