Metamath Proof Explorer


Theorem znbaslem

Description: Lemma for znbas . (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)

Ref Expression
Hypotheses znval2.s S = RSpan ring
znval2.u U = ring / 𝑠 ring ~ QG S N
znval2.y Y = /N
znbaslem.e E = Slot K
znbaslem.k K
znbaslem.l K < 10
Assertion znbaslem N 0 E U = E Y

Proof

Step Hyp Ref Expression
1 znval2.s S = RSpan ring
2 znval2.u U = ring / 𝑠 ring ~ QG S N
3 znval2.y Y = /N
4 znbaslem.e E = Slot K
5 znbaslem.k K
6 znbaslem.l K < 10
7 4 5 ndxid E = Slot E ndx
8 5 nnrei K
9 8 6 ltneii K 10
10 4 5 ndxarg E ndx = K
11 plendx ndx = 10
12 10 11 neeq12i E ndx ndx K 10
13 9 12 mpbir E ndx ndx
14 7 13 setsnid E U = E U sSet ndx Y
15 eqid Y = Y
16 1 2 3 15 znval2 N 0 Y = U sSet ndx Y
17 16 fveq2d N 0 E Y = E U sSet ndx Y
18 14 17 eqtr4id N 0 E U = E Y