Metamath Proof Explorer

Theorem mulsasslem3

Description: Lemma for mulsass . Demonstrate the central equality. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses mulsasslem3.1 
|- ( ph -> A e. No )
mulsasslem3.2 
|- ( ph -> B e. No )
mulsasslem3.3 
|- ( ph -> C e. No )
mulsasslem3.4 
|- P C_ ( ( _Left ` A ) u. ( _Right ` A ) )
mulsasslem3.5 
|- Q C_ ( ( _Left ` B ) u. ( _Right ` B ) )
mulsasslem3.6 
|- R C_ ( ( _Left ` C ) u. ( _Right ` C ) )
mulsasslem3.7 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) )
mulsasslem3.8 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) )
mulsasslem3.9 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) )
mulsasslem3.10 
|- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) )
mulsasslem3.11 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) )
mulsasslem3.12 
|- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) )
mulsasslem3.13 
|- ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) )
Assertion mulsasslem3 
|- ( ph -> ( E. x e. P E. y e. Q E. z e. R a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> E. x e. P E. y e. Q E. z e. R a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mulsasslem3.1 
 |-  ( ph -> A e. No )
2 mulsasslem3.2 
 |-  ( ph -> B e. No )
3 mulsasslem3.3 
 |-  ( ph -> C e. No )
4 mulsasslem3.4 
 |-  P C_ ( ( _Left ` A ) u. ( _Right ` A ) )
5 mulsasslem3.5 
 |-  Q C_ ( ( _Left ` B ) u. ( _Right ` B ) )
6 mulsasslem3.6 
 |-  R C_ ( ( _Left ` C ) u. ( _Right ` C ) )
7 mulsasslem3.7 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) )
8 mulsasslem3.8 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) )
9 mulsasslem3.9 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) )
10 mulsasslem3.10 
 |-  ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) )
11 mulsasslem3.11 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) )
12 mulsasslem3.12 
 |-  ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) )
13 mulsasslem3.13 
 |-  ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) )
14 oveq1 
 |-  ( xO = x -> ( xO x.s B ) = ( x x.s B ) )
15 14 oveq1d 
 |-  ( xO = x -> ( ( xO x.s B ) x.s C ) = ( ( x x.s B ) x.s C ) )
16 oveq1 
 |-  ( xO = x -> ( xO x.s ( B x.s C ) ) = ( x x.s ( B x.s C ) ) )
17 15 16 eqeq12d 
 |-  ( xO = x -> ( ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) <-> ( ( x x.s B ) x.s C ) = ( x x.s ( B x.s C ) ) ) )
18 11 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) )
19 simprll 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> x e. P )
20 4 19 sselid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> x e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
21 17 18 20 rspcdva 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s C ) = ( x x.s ( B x.s C ) ) )
22 oveq2 
 |-  ( yO = y -> ( A x.s yO ) = ( A x.s y ) )
23 22 oveq1d 
 |-  ( yO = y -> ( ( A x.s yO ) x.s C ) = ( ( A x.s y ) x.s C ) )
24 oveq1 
 |-  ( yO = y -> ( yO x.s C ) = ( y x.s C ) )
25 24 oveq2d 
 |-  ( yO = y -> ( A x.s ( yO x.s C ) ) = ( A x.s ( y x.s C ) ) )
26 23 25 eqeq12d 
 |-  ( yO = y -> ( ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) <-> ( ( A x.s y ) x.s C ) = ( A x.s ( y x.s C ) ) ) )
27 12 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) )
28 simprlr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> y e. Q )
29 5 28 sselid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> y e. ( ( _Left ` B ) u. ( _Right ` B ) ) )
30 26 27 29 rspcdva 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s C ) = ( A x.s ( y x.s C ) ) )
31 oveq2 
 |-  ( zO = z -> ( ( A x.s B ) x.s zO ) = ( ( A x.s B ) x.s z ) )
32 oveq2 
 |-  ( zO = z -> ( B x.s zO ) = ( B x.s z ) )
33 32 oveq2d 
 |-  ( zO = z -> ( A x.s ( B x.s zO ) ) = ( A x.s ( B x.s z ) ) )
34 31 33 eqeq12d 
 |-  ( zO = z -> ( ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) <-> ( ( A x.s B ) x.s z ) = ( A x.s ( B x.s z ) ) ) )
35 13 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) )
36 simprr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> z e. R )
37 6 36 sselid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> z e. ( ( _Left ` C ) u. ( _Right ` C ) ) )
38 34 35 37 rspcdva 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s B ) x.s z ) = ( A x.s ( B x.s z ) ) )
39 leftssno 
 |-  ( _Left ` A ) C_ No
40 rightssno 
 |-  ( _Right ` A ) C_ No
41 39 40 unssi 
 |-  ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No
42 4 41 sstri 
 |-  P C_ No
43 42 19 sselid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> x e. No )
44 2 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> B e. No )
45 43 44 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s B ) e. No )
46 leftssno 
 |-  ( _Left ` C ) C_ No
47 rightssno 
 |-  ( _Right ` C ) C_ No
48 46 47 unssi 
 |-  ( ( _Left ` C ) u. ( _Right ` C ) ) C_ No
49 6 48 sstri 
 |-  R C_ No
50 49 36 sselid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> z e. No )
51 45 50 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s z ) e. No )
52 1 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A e. No )
53 leftssno 
 |-  ( _Left ` B ) C_ No
54 rightssno 
 |-  ( _Right ` B ) C_ No
55 53 54 unssi 
 |-  ( ( _Left ` B ) u. ( _Right ` B ) ) C_ No
56 5 55 sstri 
 |-  Q C_ No
57 56 28 sselid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> y e. No )
58 52 57 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s y ) e. No )
59 58 50 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s z ) e. No )
60 51 59 addscomd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) )
61 60 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) )
62 43 57 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s y ) e. No )
63 62 50 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s z ) e. No )
64 59 51 63 addsubsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) )
65 61 64 eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) )
66 65 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) +s ( ( x x.s y ) x.s C ) ) )
67 51 63 subscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) e. No )
68 3 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> C e. No )
69 62 68 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s C ) e. No )
70 59 67 69 addsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) )
71 22 oveq1d 
 |-  ( yO = y -> ( ( A x.s yO ) x.s zO ) = ( ( A x.s y ) x.s zO ) )
72 oveq1 
 |-  ( yO = y -> ( yO x.s zO ) = ( y x.s zO ) )
73 72 oveq2d 
 |-  ( yO = y -> ( A x.s ( yO x.s zO ) ) = ( A x.s ( y x.s zO ) ) )
74 71 73 eqeq12d 
 |-  ( yO = y -> ( ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) <-> ( ( A x.s y ) x.s zO ) = ( A x.s ( y x.s zO ) ) ) )
75 oveq2 
 |-  ( zO = z -> ( ( A x.s y ) x.s zO ) = ( ( A x.s y ) x.s z ) )
76 oveq2 
 |-  ( zO = z -> ( y x.s zO ) = ( y x.s z ) )
77 76 oveq2d 
 |-  ( zO = z -> ( A x.s ( y x.s zO ) ) = ( A x.s ( y x.s z ) ) )
78 75 77 eqeq12d 
 |-  ( zO = z -> ( ( ( A x.s y ) x.s zO ) = ( A x.s ( y x.s zO ) ) <-> ( ( A x.s y ) x.s z ) = ( A x.s ( y x.s z ) ) ) )
79 10 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) )
80 74 78 79 29 37 rspc2dv 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s z ) = ( A x.s ( y x.s z ) ) )
81 51 69 63 addsubsd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) )
82 14 oveq1d 
 |-  ( xO = x -> ( ( xO x.s B ) x.s zO ) = ( ( x x.s B ) x.s zO ) )
83 oveq1 
 |-  ( xO = x -> ( xO x.s ( B x.s zO ) ) = ( x x.s ( B x.s zO ) ) )
84 82 83 eqeq12d 
 |-  ( xO = x -> ( ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) <-> ( ( x x.s B ) x.s zO ) = ( x x.s ( B x.s zO ) ) ) )
85 oveq2 
 |-  ( zO = z -> ( ( x x.s B ) x.s zO ) = ( ( x x.s B ) x.s z ) )
86 32 oveq2d 
 |-  ( zO = z -> ( x x.s ( B x.s zO ) ) = ( x x.s ( B x.s z ) ) )
87 85 86 eqeq12d 
 |-  ( zO = z -> ( ( ( x x.s B ) x.s zO ) = ( x x.s ( B x.s zO ) ) <-> ( ( x x.s B ) x.s z ) = ( x x.s ( B x.s z ) ) ) )
88 9 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) )
89 84 87 88 20 37 rspc2dv 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s z ) = ( x x.s ( B x.s z ) ) )
90 oveq1 
 |-  ( xO = x -> ( xO x.s yO ) = ( x x.s yO ) )
91 90 oveq1d 
 |-  ( xO = x -> ( ( xO x.s yO ) x.s C ) = ( ( x x.s yO ) x.s C ) )
92 oveq1 
 |-  ( xO = x -> ( xO x.s ( yO x.s C ) ) = ( x x.s ( yO x.s C ) ) )
93 91 92 eqeq12d 
 |-  ( xO = x -> ( ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) <-> ( ( x x.s yO ) x.s C ) = ( x x.s ( yO x.s C ) ) ) )
94 oveq2 
 |-  ( yO = y -> ( x x.s yO ) = ( x x.s y ) )
95 94 oveq1d 
 |-  ( yO = y -> ( ( x x.s yO ) x.s C ) = ( ( x x.s y ) x.s C ) )
96 24 oveq2d 
 |-  ( yO = y -> ( x x.s ( yO x.s C ) ) = ( x x.s ( y x.s C ) ) )
97 95 96 eqeq12d 
 |-  ( yO = y -> ( ( ( x x.s yO ) x.s C ) = ( x x.s ( yO x.s C ) ) <-> ( ( x x.s y ) x.s C ) = ( x x.s ( y x.s C ) ) ) )
98 8 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) )
99 93 97 98 20 29 rspc2dv 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s C ) = ( x x.s ( y x.s C ) ) )
100 89 99 oveq12d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) = ( ( x x.s ( B x.s z ) ) +s ( x x.s ( y x.s C ) ) ) )
101 44 50 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( B x.s z ) e. No )
102 43 101 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( B x.s z ) ) e. No )
103 57 68 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( y x.s C ) e. No )
104 43 103 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( y x.s C ) ) e. No )
105 102 104 addscomd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( B x.s z ) ) +s ( x x.s ( y x.s C ) ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) )
106 100 105 eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) )
107 90 oveq1d 
 |-  ( xO = x -> ( ( xO x.s yO ) x.s zO ) = ( ( x x.s yO ) x.s zO ) )
108 oveq1 
 |-  ( xO = x -> ( xO x.s ( yO x.s zO ) ) = ( x x.s ( yO x.s zO ) ) )
109 107 108 eqeq12d 
 |-  ( xO = x -> ( ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) )
110 94 oveq1d 
 |-  ( yO = y -> ( ( x x.s yO ) x.s zO ) = ( ( x x.s y ) x.s zO ) )
111 72 oveq2d 
 |-  ( yO = y -> ( x x.s ( yO x.s zO ) ) = ( x x.s ( y x.s zO ) ) )
112 110 111 eqeq12d 
 |-  ( yO = y -> ( ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) <-> ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) )
113 oveq2 
 |-  ( zO = z -> ( ( x x.s y ) x.s zO ) = ( ( x x.s y ) x.s z ) )
114 76 oveq2d 
 |-  ( zO = z -> ( x x.s ( y x.s zO ) ) = ( x x.s ( y x.s z ) ) )
115 113 114 eqeq12d 
 |-  ( zO = z -> ( ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) <-> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) ) )
116 7 adantr 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) )
117 109 112 115 116 20 29 37 rspc3dv 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) )
118 106 117 oveq12d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) )
119 81 118 eqtr3d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) )
120 80 119 oveq12d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s z ) +s ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) )
121 66 70 120 3eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) )
122 38 121 oveq12d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s B ) x.s z ) -s ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( B x.s z ) ) -s ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) )
123 52 44 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s B ) e. No )
124 123 50 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s B ) x.s z ) e. No )
125 51 59 addscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) e. No )
126 125 63 subscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) e. No )
127 124 126 69 subsubs4d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s B ) x.s z ) -s ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) )
128 52 101 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( B x.s z ) ) e. No )
129 57 50 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( y x.s z ) e. No )
130 52 129 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( y x.s z ) ) e. No )
131 104 102 addscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) e. No )
132 43 129 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( y x.s z ) ) e. No )
133 131 132 subscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) e. No )
134 128 130 133 subsubs4d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( B x.s z ) ) -s ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) )
135 122 127 134 3eqtr4d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) )
136 30 135 oveq12d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) )
137 58 68 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s C ) e. No )
138 124 126 subscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) e. No )
139 137 138 69 addsubsd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) )
140 137 138 69 addsubsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) )
141 139 140 eqtr3d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) )
142 52 103 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( y x.s C ) ) e. No )
143 142 128 130 addsubsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) )
144 143 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) )
145 128 130 subscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) e. No )
146 142 145 133 addsubsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) )
147 144 146 eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) )
148 136 141 147 3eqtr4d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) )
149 21 148 oveq12d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) )
150 45 68 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s C ) e. No )
151 150 137 addscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) e. No )
152 151 69 subscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) e. No )
153 152 124 126 addsubsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) )
154 150 137 69 addsubsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) )
155 154 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) )
156 137 69 subscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) e. No )
157 150 156 138 addsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) )
158 153 155 157 3eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) )
159 44 68 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( B x.s C ) e. No )
160 43 159 mulscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( B x.s C ) ) e. No )
161 142 128 addscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) e. No )
162 161 130 subscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) e. No )
163 160 162 133 addsubsassd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) )
164 149 158 163 3eqtr4d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) )
165 45 58 addscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) +s ( A x.s y ) ) e. No )
166 165 62 68 subsdird 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) = ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) -s ( ( x x.s y ) x.s C ) ) )
167 45 58 68 addsdird 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) = ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) )
168 167 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) )
169 166 168 eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) )
170 169 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) = ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) )
171 165 62 50 subsdird 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) = ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) -s ( ( x x.s y ) x.s z ) ) )
172 45 58 50 addsdird 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) = ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) )
173 172 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) )
174 171 173 eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) = ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) )
175 170 174 oveq12d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) = ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) )
176 103 101 addscld 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( y x.s C ) +s ( B x.s z ) ) e. No )
177 52 176 129 subsdid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) )
178 52 103 101 addsdid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) )
179 178 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) )
180 177 179 eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) )
181 180 oveq2d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) )
182 43 176 129 subsdid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) )
183 43 103 101 addsdid 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) )
184 183 oveq1d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) )
185 182 184 eqtrd 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) )
186 181 185 oveq12d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) )
187 164 175 186 3eqtr4d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) )
188 187 eqeq2d 
 |-  ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) )
189 188 anassrs 
 |-  ( ( ( ph /\ ( x e. P /\ y e. Q ) ) /\ z e. R ) -> ( a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) )
190 189 rexbidva 
 |-  ( ( ph /\ ( x e. P /\ y e. Q ) ) -> ( E. z e. R a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> E. z e. R a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) )
191 190 2rexbidva 
 |-  ( ph -> ( E. x e. P E. y e. Q E. z e. R a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> E. x e. P E. y e. Q E. z e. R a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) )