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	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	opprlem.2	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	opprlem.3	⊢ ( 𝐸 ‘ ndx ) ≠ ( .r ‘ ndx )
Assertion	opprlem	⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2		opprlem.2	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
3		opprlem.3	⊢ ( 𝐸 ‘ ndx ) ≠ ( .r ‘ ndx )
4	2 3	setsnid	⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑅 ) ⟩ ) )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7	5 6 1	opprval	⊢ 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑅 ) ⟩ )
8	7	fveq2i	⊢ ( 𝐸 ‘ 𝑂 ) = ( 𝐸 ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑅 ) ⟩ ) )
9	4 8	eqtr4i	⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑂 )