znbaslemOLD - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > znbaslemOLD		Structured version Visualization version GIF version

Theorem znbaslemOLD 20848

Description: Obsolete version of znbaslem 20847 as of 3-Nov-2024. Lemma for znbas 20856. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (New usage is discouraged.) (Proof modification is discouraged.)

**Hypotheses**
Ref	Expression
znval2.s	⊢ 𝑆 = (RSpan‘ℤ_ring)
znval2.u	⊢ 𝑈 = (ℤ_ring /_s (ℤ_ring ~_QG (𝑆‘{𝑁})))
znval2.y	⊢ 𝑌 = (ℤ/nℤ‘𝑁)
znbaslemOLD.e	⊢ 𝐸 = Slot 𝐾
znbaslemOLD.k	⊢ 𝐾 ∈ ℕ
znbaslemOLD.l	⊢ 𝐾 < ;10

**Assertion**
Ref	Expression
znbaslemOLD	⊢ (𝑁 ∈ ℕ₀ → (𝐸‘𝑈) = (𝐸‘𝑌))

**Proof of Theorem znbaslemOLD**
Step	Hyp	Ref	Expression
1		znbaslemOLD.e	. . . 4 ⊢ 𝐸 = Slot 𝐾
2		znbaslemOLD.k	. . . 4 ⊢ 𝐾 ∈ ℕ
3	1, 2	ndxid 16995	. . 3 ⊢ 𝐸 = Slot (𝐸‘ndx)
4	2	nnrei 12087	. . . . 5 ⊢ 𝐾 ∈ ℝ
5		znbaslemOLD.l	. . . . 5 ⊢ 𝐾 < ;10
6	4, 5	ltneii 11193	. . . 4 ⊢ 𝐾 ≠ ;10
7	1, 2	ndxarg 16994	. . . . 5 ⊢ (𝐸‘ndx) = 𝐾
8		plendx 17173	. . . . 5 ⊢ (le‘ndx) = ;10
9	7, 8	neeq12i 3008	. . . 4 ⊢ ((𝐸‘ndx) ≠ (le‘ndx) ↔ 𝐾 ≠ ;10)
10	6, 9	mpbir 230	. . 3 ⊢ (𝐸‘ndx) ≠ (le‘ndx)
11	3, 10	setsnid 17007	. 2 ⊢ (𝐸‘𝑈) = (𝐸‘(𝑈 sSet ⟨(le‘ndx), (le‘𝑌)⟩))
12		znval2.s	. . . 4 ⊢ 𝑆 = (RSpan‘ℤ_ring)
13		znval2.u	. . . 4 ⊢ 𝑈 = (ℤ_ring /_s (ℤ_ring ~_QG (𝑆‘{𝑁})))
14		znval2.y	. . . 4 ⊢ 𝑌 = (ℤ/nℤ‘𝑁)
15		eqid 2737	. . . 4 ⊢ (le‘𝑌) = (le‘𝑌)
16	12, 13, 14, 15	znval2 20846	. . 3 ⊢ (𝑁 ∈ ℕ₀ → 𝑌 = (𝑈 sSet ⟨(le‘ndx), (le‘𝑌)⟩))
17	16	fveq2d 6833	. 2 ⊢ (𝑁 ∈ ℕ₀ → (𝐸‘𝑌) = (𝐸‘(𝑈 sSet ⟨(le‘ndx), (le‘𝑌)⟩)))
18	11, 17	eqtr4id 2796	1 ⊢ (𝑁 ∈ ℕ₀ → (𝐸‘𝑈) = (𝐸‘𝑌))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 {csn 4577 ⟨cop 4583 class class class wbr 5096 ‘cfv 6483 (class class class)co 7341 0cc0 10976 1c1 10977 < clt 11114 ℕcn 12078 ℕ₀cn0 12338 cdc 12542 sSet csts 16961 Slot cslot 16979 ndxcnx 16991 lecple 17066 /_s cqus 17313 ~_QG cqg 18847 RSpancrsp 20538 ℤ_ringczring 20775 ℤ/nℤczn 20809

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5247 ax-nul 5254 ax-pow 5312 ax-pr 5376 ax-un 7654 ax-cnex 11032 ax-resscn 11033 ax-1cn 11034 ax-icn 11035 ax-addcl 11036 ax-addrcl 11037 ax-mulcl 11038 ax-mulrcl 11039 ax-mulcom 11040 ax-addass 11041 ax-mulass 11042 ax-distr 11043 ax-i2m1 11044 ax-1ne0 11045 ax-1rid 11046 ax-rnegex 11047 ax-rrecex 11048 ax-cnre 11049 ax-pre-lttri 11050 ax-pre-lttrn 11051 ax-pre-ltadd 11052 ax-pre-mulgt0 11053 ax-addf 11055 ax-mulf 11056

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3731 df-csb 3847 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3920 df-nul 4274 df-if 4478 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4857 df-iun 4947 df-br 5097 df-opab 5159 df-mpt 5180 df-tr 5214 df-id 5522 df-eprel 5528 df-po 5536 df-so 5537 df-fr 5579 df-we 5581 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6242 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6435 df-fun 6485 df-fn 6486 df-f 6487 df-f1 6488 df-fo 6489 df-f1o 6490 df-fv 6491 df-riota 7297 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7785 df-1st 7903 df-2nd 7904 df-frecs 8171 df-wrecs 8202 df-recs 8276 df-rdg 8315 df-1o 8371 df-er 8573 df-en 8809 df-dom 8810 df-sdom 8811 df-fin 8812 df-pnf 11116 df-mnf 11117 df-xr 11118 df-ltxr 11119 df-le 11120 df-sub 11312 df-neg 11313 df-nn 12079 df-2 12141 df-3 12142 df-4 12143 df-5 12144 df-6 12145 df-7 12146 df-8 12147 df-9 12148 df-n0 12339 df-z 12425 df-dec 12543 df-uz 12688 df-fz 13345 df-struct 16945 df-sets 16962 df-slot 16980 df-ndx 16992 df-base 17010 df-ress 17039 df-plusg 17072 df-mulr 17073 df-starv 17074 df-tset 17078 df-ple 17079 df-ds 17081 df-unif 17082 df-0g 17249 df-mgm 18423 df-sgrp 18472 df-mnd 18483 df-grp 18676 df-minusg 18677 df-subg 18848 df-cmn 19483 df-mgp 19815 df-ur 19832 df-ring 19879 df-cring 19880 df-subrg 20126 df-cnfld 20703 df-zring 20776 df-zn 20813

This theorem is referenced by: znbas2OLD 20850 znaddOLD 20852 znmulOLD 20854

W3C validator