Theorem opprlemOLD 20344

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

Hypotheses

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

Assertion

Ref	Expression
opprlemOLD	⊢ (𝐸‘𝑅) = (𝐸‘𝑂)

Proof of Theorem opprlemOLD

Step	Hyp	Ref	Expression
1		opprlemOLD.2	. . . 4 ⊢ 𝐸 = Slot 𝑁
2		opprlemOLD.3	. . . 4 ⊢ 𝑁 ∈ ℕ
3	1, 2	ndxid 17220	. . 3 ⊢ 𝐸 = Slot (𝐸‘ndx)
4	2	nnrei 12283	. . . . 5 ⊢ 𝑁 ∈ ℝ
5		opprlemOLD.4	. . . . 5 ⊢ 𝑁 < 3
6	4, 5	ltneii 11384	. . . 4 ⊢ 𝑁 ≠ 3
7	1, 2	ndxarg 17219	. . . . 5 ⊢ (𝐸‘ndx) = 𝑁
8		mulrndx 17328	. . . . 5 ⊢ (.r‘ndx) = 3
9	7, 8	neeq12i 3000	. . . 4 ⊢ ((𝐸‘ndx) ≠ (.r‘ndx) ↔ 𝑁 ≠ 3)
10	6, 9	mpbir 230	. . 3 ⊢ (𝐸‘ndx) ≠ (.r‘ndx)
11	3, 10	setsnid 17232	. 2 ⊢ (𝐸‘𝑅) = (𝐸‘(𝑅 sSet ⟨(.r‘ndx), tpos (.r‘𝑅)⟩))
12		eqid 2729	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
13		eqid 2729	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
14		opprbas.1	. . . 4 ⊢ 𝑂 = (oppr‘𝑅)
15	12, 13, 14	opprval 20339	. . 3 ⊢ 𝑂 = (𝑅 sSet ⟨(.r‘ndx), tpos (.r‘𝑅)⟩)
16	15	fveq2i 6908	. 2 ⊢ (𝐸‘𝑂) = (𝐸‘(𝑅 sSet ⟨(.r‘ndx), tpos (.r‘𝑅)⟩))
17	11, 16	eqtr4i 2760	1 ⊢ (𝐸‘𝑅) = (𝐸‘𝑂)

Syntax hints:   = wceq 1534   ∈ wcel 2100   ≠ wne 2933  ⟨cop 4642   class class class wbr 5156  ‘cfv 6558  (class class class)co 7430  tpos ctpos 8248   < clt 11305  ℕcn 12274  3c3 12330   sSet csts 17186  Slot cslot 17204  ndxcnx 17216  Basecbs 17234  ._rcmulr 17288  opp_rcoppr 20337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-cnex 11221  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-i2m1 11233  ax-1ne0 11234  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-pss 3979  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-iun 5008  df-br 5157  df-opab 5219  df-mpt 5240  df-tr 5274  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5641  df-we 5643  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-pred 6317  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7885  df-2nd 8012  df-tpos 8249  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-pnf 11307  df-mnf 11308  df-ltxr 11310  df-nn 12275  df-2 12337  df-3 12338  df-sets 17187  df-slot 17205  df-ndx 17217  df-mulr 17301  df-oppr 20338

This theorem is referenced by:  opprbasOLD  20346  oppraddOLD  20348