Metamath Proof Explorer

Theorem nmulrid

Description: Identity law for natural multiplication. (Contributed by Scott Fenton, 21-Jul-2026)

Ref Expression
Assertion nmulrid 
|- ( A e. On -> ( A .no 1o ) = A )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = b -> ( a .no 1o ) = ( b .no 1o ) )
2 id 
 |-  ( a = b -> a = b )
3 1 2 eqeq12d 
 |-  ( a = b -> ( ( a .no 1o ) = a <-> ( b .no 1o ) = b ) )
4 oveq1 
 |-  ( a = A -> ( a .no 1o ) = ( A .no 1o ) )
5 id 
 |-  ( a = A -> a = A )
6 4 5 eqeq12d 
 |-  ( a = A -> ( ( a .no 1o ) = a <-> ( A .no 1o ) = A ) )
7 1on 
 |-  1o e. On
8 nmulval 
 |-  ( ( a e. On /\ 1o e. On ) -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } )
9 7 8 mpan2 
 |-  ( a e. On -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } )
10 9 adantr 
 |-  ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } )
11 df1o2 
 |-  1o = { (/) }
12 11 raleqi 
 |-  ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. y e. { (/) } ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) )
13 0ex 
 |-  (/) e. _V
14 oveq2 
 |-  ( y = (/) -> ( a .no y ) = ( a .no (/) ) )
15 14 oveq2d 
 |-  ( y = (/) -> ( ( b .no 1o ) +no ( a .no y ) ) = ( ( b .no 1o ) +no ( a .no (/) ) ) )
16 oveq2 
 |-  ( y = (/) -> ( b .no y ) = ( b .no (/) ) )
17 16 oveq2d 
 |-  ( y = (/) -> ( x +no ( b .no y ) ) = ( x +no ( b .no (/) ) ) )
18 15 17 eleq12d 
 |-  ( y = (/) -> ( ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) ) )
19 13 18 ralsn 
 |-  ( A. y e. { (/) } ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) )
20 12 19 bitri 
 |-  ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) )
21 simprr 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b .no 1o ) = b )
22 nmulr0 
 |-  ( a e. On -> ( a .no (/) ) = (/) )
23 22 ad2antrr 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( a .no (/) ) = (/) )
24 21 23 oveq12d 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( b .no 1o ) +no ( a .no (/) ) ) = ( b +no (/) ) )
25 onss 
 |-  ( a e. On -> a C_ On )
26 25 adantr 
 |-  ( ( a e. On /\ x e. On ) -> a C_ On )
27 26 sselda 
 |-  ( ( ( a e. On /\ x e. On ) /\ b e. a ) -> b e. On )
28 27 adantrr 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> b e. On )
29 naddrid 
 |-  ( b e. On -> ( b +no (/) ) = b )
30 28 29 syl 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b +no (/) ) = b )
31 24 30 eqtrd 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( b .no 1o ) +no ( a .no (/) ) ) = b )
32 nmulr0 
 |-  ( b e. On -> ( b .no (/) ) = (/) )
33 28 32 syl 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b .no (/) ) = (/) )
34 33 oveq2d 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no ( b .no (/) ) ) = ( x +no (/) ) )
35 naddrid 
 |-  ( x e. On -> ( x +no (/) ) = x )
36 35 ad2antlr 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no (/) ) = x )
37 34 36 eqtrd 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no ( b .no (/) ) ) = x )
38 31 37 eleq12d 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) <-> b e. x ) )
39 20 38 bitrid 
 |-  ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) )
40 39 expr 
 |-  ( ( ( a e. On /\ x e. On ) /\ b e. a ) -> ( ( b .no 1o ) = b -> ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) )
41 40 ralimdva 
 |-  ( ( a e. On /\ x e. On ) -> ( A. b e. a ( b .no 1o ) = b -> A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) )
42 41 imp 
 |-  ( ( ( a e. On /\ x e. On ) /\ A. b e. a ( b .no 1o ) = b ) -> A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) )
43 ralbi 
 |-  ( A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) )
44 42 43 syl 
 |-  ( ( ( a e. On /\ x e. On ) /\ A. b e. a ( b .no 1o ) = b ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) )
45 44 an32s 
 |-  ( ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) /\ x e. On ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) )
46 dfss3 
 |-  ( a C_ x <-> A. b e. a b e. x )
47 45 46 bitr4di 
 |-  ( ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) /\ x e. On ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> a C_ x ) )
48 47 rabbidva 
 |-  ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } = { x e. On | a C_ x } )
49 48 inteqd 
 |-  ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } = |^| { x e. On | a C_ x } )
50 intmin 
 |-  ( a e. On -> |^| { x e. On | a C_ x } = a )
51 50 adantr 
 |-  ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> |^| { x e. On | a C_ x } = a )
52 10 49 51 3eqtrd 
 |-  ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> ( a .no 1o ) = a )
53 52 ex 
 |-  ( a e. On -> ( A. b e. a ( b .no 1o ) = b -> ( a .no 1o ) = a ) )
54 3 6 53 tfis3 
 |-  ( A e. On -> ( A .no 1o ) = A )