Metamath Proof Explorer

Theorem addsdilem3

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

Ref Expression
Hypotheses addsdilem3.1 
|- ( ph -> A e. No )
addsdilem3.2 
|- ( ph -> B e. No )
addsdilem3.3 
|- ( ph -> C e. No )
addsdilem3.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 ) ) )
addsdilem3.5 
|- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( A x.s ( yO +s C ) ) = ( ( A x.s yO ) +s ( A x.s C ) ) )
addsdilem3.6 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( xO x.s ( yO +s C ) ) = ( ( xO x.s yO ) +s ( xO x.s C ) ) )
addsdilem3.7 
|- ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
addsdilem3.8 
|- ( ps -> Y e. ( ( _Left ` B ) u. ( _Right ` B ) ) )
Assertion addsdilem3 
|- ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( Y +s C ) ) ) -s ( X x.s ( Y +s C ) ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) -s ( X x.s Y ) ) +s ( A x.s C ) ) )

Proof

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