Metamath Proof Explorer


Theorem opprlem

Description: Lemma for opprbas and oppradd . (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses opprbas.1 𝑂 = ( oppr𝑅 )
opprlem.2 𝐸 = Slot 𝑁
opprlem.3 𝑁 ∈ ℕ
opprlem.4 𝑁 < 3
Assertion opprlem ( 𝐸𝑅 ) = ( 𝐸𝑂 )

Proof

Step Hyp Ref Expression
1 opprbas.1 𝑂 = ( oppr𝑅 )
2 opprlem.2 𝐸 = Slot 𝑁
3 opprlem.3 𝑁 ∈ ℕ
4 opprlem.4 𝑁 < 3
5 2 3 ndxid 𝐸 = Slot ( 𝐸 ‘ ndx )
6 3 nnrei 𝑁 ∈ ℝ
7 6 4 ltneii 𝑁 ≠ 3
8 2 3 ndxarg ( 𝐸 ‘ ndx ) = 𝑁
9 mulrndx ( .r ‘ ndx ) = 3
10 8 9 neeq12i ( ( 𝐸 ‘ ndx ) ≠ ( .r ‘ ndx ) ↔ 𝑁 ≠ 3 )
11 7 10 mpbir ( 𝐸 ‘ ndx ) ≠ ( .r ‘ ndx )
12 5 11 setsnid ( 𝐸𝑅 ) = ( 𝐸 ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r𝑅 ) ⟩ ) )
13 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 eqid ( .r𝑅 ) = ( .r𝑅 )
15 13 14 1 opprval 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r𝑅 ) ⟩ )
16 15 fveq2i ( 𝐸𝑂 ) = ( 𝐸 ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r𝑅 ) ⟩ ) )
17 12 16 eqtr4i ( 𝐸𝑅 ) = ( 𝐸𝑂 )