Metamath Proof Explorer

Theorem nmulr0

Description: Natural multiplication by zero. (Contributed by Scott Fenton, 10-Jun-2026)

Ref Expression
Assertion nmulr0 
|- ( A e. On -> ( A .no (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 nmulval 
 |-  ( ( A e. On /\ (/) e. On ) -> ( A .no (/) ) = |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )
3 1 2 mpan2 
 |-  ( A e. On -> ( A .no (/) ) = |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )
4 ral0 
 |-  A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) )
5 4 rgenw 
 |-  A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) )
6 oveq1 
 |-  ( x = (/) -> ( x +no ( a .no b ) ) = ( (/) +no ( a .no b ) ) )
7 6 eleq2d 
 |-  ( x = (/) -> ( ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) )
8 7 2ralbidv 
 |-  ( x = (/) -> ( A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) )
9 8 elrab3 
 |-  ( (/) e. On -> ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) )
10 1 9 ax-mp 
 |-  ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) )
11 5 10 mpbir 
 |-  (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) }
12 int0el 
 |-  ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } -> |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = (/) )
13 11 12 ax-mp 
 |-  |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = (/)
14 3 13 eqtrdi 
 |-  ( A e. On -> ( A .no (/) ) = (/) )