Metamath Proof Explorer

Theorem addsdilem4

Description: Lemma for addsdi . Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025)

Ref Expression
Hypotheses addsdilem4.1 
|- ( ph -> A e. No )
addsdilem4.2 
|- ( ph -> B e. No )
addsdilem4.3 
|- ( ph -> C e. No )
addsdilem4.4 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) )
addsdilem4.5 
|- ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) )
addsdilem4.6 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) )
addsdilem4.7 
|- ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
addsdilem4.8 
|- ( ps -> Z e. ( ( _Left ` C ) u. ( _Right ` C ) ) )
Assertion addsdilem4 
|- ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) -s ( X x.s ( B +s Z ) ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) )

Proof

Step Hyp Ref Expression
1 addsdilem4.1 
 |-  ( ph -> A e. No )
2 addsdilem4.2 
 |-  ( ph -> B e. No )
3 addsdilem4.3 
 |-  ( ph -> C e. No )
4 addsdilem4.4 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) )
5 addsdilem4.5 
 |-  ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) )
6 addsdilem4.6 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) )
7 addsdilem4.7 
 |-  ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
8 addsdilem4.8 
 |-  ( ps -> Z e. ( ( _Left ` C ) u. ( _Right ` C ) ) )
9 oveq1 
 |-  ( xO = X -> ( xO x.s ( B +s C ) ) = ( X x.s ( B +s C ) ) )
10 oveq1 
 |-  ( xO = X -> ( xO x.s B ) = ( X x.s B ) )
11 oveq1 
 |-  ( xO = X -> ( xO x.s C ) = ( X x.s C ) )
12 10 11 oveq12d 
 |-  ( xO = X -> ( ( xO x.s B ) +s ( xO x.s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) )
13 9 12 eqeq12d 
 |-  ( xO = X -> ( ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) <-> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) )
14 4 adantr 
 |-  ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) )
15 7 adantl 
 |-  ( ( ph /\ ps ) -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
16 13 14 15 rspcdva 
 |-  ( ( ph /\ ps ) -> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) )
17 oveq2 
 |-  ( zO = Z -> ( B +s zO ) = ( B +s Z ) )
18 17 oveq2d 
 |-  ( zO = Z -> ( A x.s ( B +s zO ) ) = ( A x.s ( B +s Z ) ) )
19 oveq2 
 |-  ( zO = Z -> ( A x.s zO ) = ( A x.s Z ) )
20 19 oveq2d 
 |-  ( zO = Z -> ( ( A x.s B ) +s ( A x.s zO ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) )
21 18 20 eqeq12d 
 |-  ( zO = Z -> ( ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) <-> ( A x.s ( B +s Z ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) )
22 5 adantr 
 |-  ( ( ph /\ ps ) -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) )
23 8 adantl 
 |-  ( ( ph /\ ps ) -> Z e. ( ( _Left ` C ) u. ( _Right ` C ) ) )
24 21 22 23 rspcdva 
 |-  ( ( ph /\ ps ) -> ( A x.s ( B +s Z ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) )
25 16 24 oveq12d 
 |-  ( ( ph /\ ps ) -> ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) = ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) )
26 oveq1 
 |-  ( xO = X -> ( xO x.s ( B +s zO ) ) = ( X x.s ( B +s zO ) ) )
27 oveq1 
 |-  ( xO = X -> ( xO x.s zO ) = ( X x.s zO ) )
28 10 27 oveq12d 
 |-  ( xO = X -> ( ( xO x.s B ) +s ( xO x.s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) )
29 26 28 eqeq12d 
 |-  ( xO = X -> ( ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) <-> ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) )
30 17 oveq2d 
 |-  ( zO = Z -> ( X x.s ( B +s zO ) ) = ( X x.s ( B +s Z ) ) )
31 oveq2 
 |-  ( zO = Z -> ( X x.s zO ) = ( X x.s Z ) )
32 31 oveq2d 
 |-  ( zO = Z -> ( ( X x.s B ) +s ( X x.s zO ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) )
33 30 32 eqeq12d 
 |-  ( zO = Z -> ( ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) <-> ( X x.s ( B +s Z ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) )
34 6 adantr 
 |-  ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) )
35 29 33 34 15 23 rspc2dv 
 |-  ( ( ph /\ ps ) -> ( X x.s ( B +s Z ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) )
36 25 35 oveq12d 
 |-  ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) -s ( X x.s ( B +s Z ) ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( ( X x.s B ) +s ( X x.s Z ) ) ) )
37 leftssno 
 |-  ( _Left ` A ) C_ No
38 rightssno 
 |-  ( _Right ` A ) C_ No
39 37 38 unssi 
 |-  ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No
40 39 7 sselid 
 |-  ( ps -> X e. No )
41 40 adantl 
 |-  ( ( ph /\ ps ) -> X e. No )
42 2 adantr 
 |-  ( ( ph /\ ps ) -> B e. No )
43 41 42 mulscld 
 |-  ( ( ph /\ ps ) -> ( X x.s B ) e. No )
44 3 adantr 
 |-  ( ( ph /\ ps ) -> C e. No )
45 41 44 mulscld 
 |-  ( ( ph /\ ps ) -> ( X x.s C ) e. No )
46 43 45 addscld 
 |-  ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( X x.s C ) ) e. No )
47 1 2 mulscld 
 |-  ( ph -> ( A x.s B ) e. No )
48 47 adantr 
 |-  ( ( ph /\ ps ) -> ( A x.s B ) e. No )
49 1 adantr 
 |-  ( ( ph /\ ps ) -> A e. No )
50 leftssno 
 |-  ( _Left ` C ) C_ No
51 rightssno 
 |-  ( _Right ` C ) C_ No
52 50 51 unssi 
 |-  ( ( _Left ` C ) u. ( _Right ` C ) ) C_ No
53 52 8 sselid 
 |-  ( ps -> Z e. No )
54 53 adantl 
 |-  ( ( ph /\ ps ) -> Z e. No )
55 49 54 mulscld 
 |-  ( ( ph /\ ps ) -> ( A x.s Z ) e. No )
56 48 55 addscld 
 |-  ( ( ph /\ ps ) -> ( ( A x.s B ) +s ( A x.s Z ) ) e. No )
57 46 56 addscld 
 |-  ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) e. No )
58 41 54 mulscld 
 |-  ( ( ph /\ ps ) -> ( X x.s Z ) e. No )
59 57 43 58 subsubs4d 
 |-  ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( ( X x.s B ) +s ( X x.s Z ) ) ) )
60 46 56 43 addsubsd 
 |-  ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) )
61 43 45 addscomd 
 |-  ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( X x.s C ) ) = ( ( X x.s C ) +s ( X x.s B ) ) )
62 61 oveq1d 
 |-  ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) = ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) )
63 pncans 
 |-  ( ( ( X x.s C ) e. No /\ ( X x.s B ) e. No ) -> ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) = ( X x.s C ) )
64 45 43 63 syl2anc 
 |-  ( ( ph /\ ps ) -> ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) = ( X x.s C ) )
65 62 64 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) = ( X x.s C ) )
66 65 oveq1d 
 |-  ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) = ( ( X x.s C ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) )
67 45 48 55 adds12d 
 |-  ( ( ph /\ ps ) -> ( ( X x.s C ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) = ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) )
68 60 66 67 3eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) = ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) )
69 68 oveq1d 
 |-  ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) -s ( X x.s Z ) ) )
70 45 55 addscld 
 |-  ( ( ph /\ ps ) -> ( ( X x.s C ) +s ( A x.s Z ) ) e. No )
71 48 70 58 addsubsassd 
 |-  ( ( ph /\ ps ) -> ( ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) -s ( X x.s Z ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) )
72 69 71 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) )
73 36 59 72 3eqtr2d 
 |-  ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) -s ( X x.s ( B +s Z ) ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) )