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

Metamath Proof Explorer

Theorem opprlem

Description: Lemma for opprbas and oppradd . (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by AV, 6-Nov-2024)

Ref Expression
Hypotheses opprbas.1 ⊢ O = opp r ⁡ R
opprlem.2 ⊢ E = Slot E ⁡ ndx
opprlem.3 ⊢ E ⁡ ndx ≠ ⋅ ndx
Assertion opprlem ⊢ E ⁡ R = E ⁡ O

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ O = opp r ⁡ R
2 opprlem.2 ⊢ E = Slot E ⁡ ndx
3 opprlem.3 ⊢ E ⁡ ndx ≠ ⋅ ndx
4 2 3 setsnid ⊢ E ⁡ R = E ⁡ R sSet ⋅ ndx tpos ⋅ R
5 eqid ⊢ Base R = Base R
6 eqid ⊢ ⋅ R = ⋅ R
7 5 6 1 opprval ⊢ O = R sSet ⋅ ndx tpos ⋅ R
8 7 fveq2i ⊢ E ⁡ O = E ⁡ R sSet ⋅ ndx tpos ⋅ R
9 4 8 eqtr4i ⊢ E ⁡ R = E ⁡ O