Theorem opprlemOLD

Description: Obsolete version of opprlem as of 6-Nov-2024. Lemma for opprbas and oppradd . (Contributed by Mario Carneiro, 1-Dec-2014) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2		opprlemOLD.2	⊢ 𝐸 = Slot 𝑁
3		opprlemOLD.3	⊢ 𝑁 ∈ ℕ
4		opprlemOLD.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	⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑂 )