Metamath Proof Explorer

Theorem mulscutlem

Description: Lemma for mulscut . State the theorem with extra DV conditions. (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses mulscutlem.1 
|- ( ph -> A e. No )
mulscutlem.2 
|- ( ph -> B e. No )
Assertion mulscutlem 
|- ( ph -> ( ( A x.s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <

Proof

Step Hyp Ref Expression
1 mulscutlem.1 
 |-  ( ph -> A e. No )
2 mulscutlem.2 
 |-  ( ph -> B e. No )
3 mulsprop 
 |-  ( ( ( e e. No /\ f e. No ) /\ ( g e. No /\ h e. No ) /\ ( i e. No /\ j e. No ) ) -> ( ( e x.s f ) e. No /\ ( ( g  ( ( g x.s j ) -s ( g x.s i ) )
4 3 a1d 
 |-  ( ( ( e e. No /\ f e. No ) /\ ( g e. No /\ h e. No ) /\ ( i e. No /\ j e. No ) ) -> ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g  ( ( g x.s j ) -s ( g x.s i ) )
5 4 3expa 
 |-  ( ( ( ( e e. No /\ f e. No ) /\ ( g e. No /\ h e. No ) ) /\ ( i e. No /\ j e. No ) ) -> ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g  ( ( g x.s j ) -s ( g x.s i ) )
6 5 ralrimivva 
 |-  ( ( ( e e. No /\ f e. No ) /\ ( g e. No /\ h e. No ) ) -> A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g  ( ( g x.s j ) -s ( g x.s i ) )
7 6 ralrimivva 
 |-  ( ( e e. No /\ f e. No ) -> A. g e. No A. h e. No A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g  ( ( g x.s j ) -s ( g x.s i ) )
8 7 rgen2 
 |-  A. e e. No A. f e. No A. g e. No A. h e. No A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g  ( ( g x.s j ) -s ( g x.s i ) )
9 8 a1i 
 |-  ( ( A e. No /\ B e. No ) -> A. e e. No A. f e. No A. g e. No A. h e. No A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g  ( ( g x.s j ) -s ( g x.s i ) )
10 simpl 
 |-  ( ( A e. No /\ B e. No ) -> A e. No )
11 simpr 
 |-  ( ( A e. No /\ B e. No ) -> B e. No )
12 9 10 11 mulsproplem10 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A x.s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
13 1 2 12 syl2anc 
 |-  ( ph -> ( ( A x.s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <