Metamath Proof Explorer

Theorem nadddilem3

Description: Lemma for nadddi . Prove a subcase of the forward implication. (Contributed by Scott Fenton, 3-Aug-2026)

Ref Expression
Hypotheses nadddilem3.1 
|- ( ph -> A e. On )
nadddilem3.2 
|- ( ph -> B e. On )
nadddilem3.3 
|- ( ph -> C e. On )
nadddilem3.4 
|- ( ph -> X e. A )
nadddilem3.5 
|- ( ph -> Y e. ( B +no C ) )
nadddilem3.6 
|- ( ph -> Z e. B )
nadddilem3.7 
|- ( ph -> Y C_ ( Z +no C ) )
nadddilem3.8 
|- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
nadddilem3.9 
|- ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) )
nadddilem3.10 
|- ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) )
Assertion nadddilem3 
|- ( ph -> ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) )

Proof

Step Hyp Ref Expression
1 nadddilem3.1 
 |-  ( ph -> A e. On )
2 nadddilem3.2 
 |-  ( ph -> B e. On )
3 nadddilem3.3 
 |-  ( ph -> C e. On )
4 nadddilem3.4 
 |-  ( ph -> X e. A )
5 nadddilem3.5 
 |-  ( ph -> Y e. ( B +no C ) )
6 nadddilem3.6 
 |-  ( ph -> Z e. B )
7 nadddilem3.7 
 |-  ( ph -> Y C_ ( Z +no C ) )
8 nadddilem3.8 
 |-  ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
9 nadddilem3.9 
 |-  ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) )
10 nadddilem3.10 
 |-  ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) )
11 2 6 onelond 
 |-  ( ph -> Z e. On )
12 11 3 naddcld 
 |-  ( ph -> ( Z +no C ) e. On )
13 1 4 onelond 
 |-  ( ph -> X e. On )
14 2 3 naddcld 
 |-  ( ph -> ( B +no C ) e. On )
15 14 5 onelond 
 |-  ( ph -> Y e. On )
16 1 4 onelssd 
 |-  ( ph -> X C_ A )
17 nmuladdss 
 |-  ( ( ( A e. On /\ ( Z +no C ) e. On ) /\ ( X e. On /\ Y e. On ) /\ ( X C_ A /\ Y C_ ( Z +no C ) ) ) -> ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) C_ ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) )
18 1 12 13 15 16 7 17 syl222anc 
 |-  ( ph -> ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) C_ ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) )
19 13 12 nmulcld 
 |-  ( ph -> ( X .no ( Z +no C ) ) e. On )
20 1 15 nmulcld 
 |-  ( ph -> ( A .no Y ) e. On )
21 19 20 naddcld 
 |-  ( ph -> ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) e. On )
22 1 12 nmulcld 
 |-  ( ph -> ( A .no ( Z +no C ) ) e. On )
23 13 15 nmulcld 
 |-  ( ph -> ( X .no Y ) e. On )
24 22 23 naddcld 
 |-  ( ph -> ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) e. On )
25 1 2 nmulcld 
 |-  ( ph -> ( A .no B ) e. On )
26 naddss2 
 |-  ( ( ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) e. On /\ ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) e. On /\ ( A .no B ) e. On ) -> ( ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) C_ ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) <-> ( ( A .no B ) +no ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) ) C_ ( ( A .no B ) +no ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) ) ) )
27 21 24 25 26 syl3anc 
 |-  ( ph -> ( ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) C_ ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) <-> ( ( A .no B ) +no ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) ) C_ ( ( A .no B ) +no ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) ) ) )
28 18 27 mpbid 
 |-  ( ph -> ( ( A .no B ) +no ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) ) C_ ( ( A .no B ) +no ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) ) )
29 nmuladdel 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( X e. A /\ Z e. B ) ) -> ( ( X .no B ) +no ( A .no Z ) ) e. ( ( A .no B ) +no ( X .no Z ) ) )
30 1 2 4 6 29 syl22anc 
 |-  ( ph -> ( ( X .no B ) +no ( A .no Z ) ) e. ( ( A .no B ) +no ( X .no Z ) ) )
31 13 11 nmulcld 
 |-  ( ph -> ( X .no Z ) e. On )
32 31 25 naddcomd 
 |-  ( ph -> ( ( X .no Z ) +no ( A .no B ) ) = ( ( A .no B ) +no ( X .no Z ) ) )
33 30 32 eleqtrrd 
 |-  ( ph -> ( ( X .no B ) +no ( A .no Z ) ) e. ( ( X .no Z ) +no ( A .no B ) ) )
34 13 2 nmulcld 
 |-  ( ph -> ( X .no B ) e. On )
35 1 11 nmulcld 
 |-  ( ph -> ( A .no Z ) e. On )
36 34 35 naddcld 
 |-  ( ph -> ( ( X .no B ) +no ( A .no Z ) ) e. On )
37 31 25 naddcld 
 |-  ( ph -> ( ( X .no Z ) +no ( A .no B ) ) e. On )
38 13 3 nmulcld 
 |-  ( ph -> ( X .no C ) e. On )
39 naddel2 
 |-  ( ( ( ( X .no B ) +no ( A .no Z ) ) e. On /\ ( ( X .no Z ) +no ( A .no B ) ) e. On /\ ( X .no C ) e. On ) -> ( ( ( X .no B ) +no ( A .no Z ) ) e. ( ( X .no Z ) +no ( A .no B ) ) <-> ( ( X .no C ) +no ( ( X .no B ) +no ( A .no Z ) ) ) e. ( ( X .no C ) +no ( ( X .no Z ) +no ( A .no B ) ) ) ) )
40 36 37 38 39 syl3anc 
 |-  ( ph -> ( ( ( X .no B ) +no ( A .no Z ) ) e. ( ( X .no Z ) +no ( A .no B ) ) <-> ( ( X .no C ) +no ( ( X .no B ) +no ( A .no Z ) ) ) e. ( ( X .no C ) +no ( ( X .no Z ) +no ( A .no B ) ) ) ) )
41 33 40 mpbid 
 |-  ( ph -> ( ( X .no C ) +no ( ( X .no B ) +no ( A .no Z ) ) ) e. ( ( X .no C ) +no ( ( X .no Z ) +no ( A .no B ) ) ) )
42 38 31 naddcomd 
 |-  ( ph -> ( ( X .no C ) +no ( X .no Z ) ) = ( ( X .no Z ) +no ( X .no C ) ) )
43 42 oveq1d 
 |-  ( ph -> ( ( ( X .no C ) +no ( X .no Z ) ) +no ( A .no B ) ) = ( ( ( X .no Z ) +no ( X .no C ) ) +no ( A .no B ) ) )
44 38 31 25 naddassd 
 |-  ( ph -> ( ( ( X .no C ) +no ( X .no Z ) ) +no ( A .no B ) ) = ( ( X .no C ) +no ( ( X .no Z ) +no ( A .no B ) ) ) )
45 31 38 25 naddassd 
 |-  ( ph -> ( ( ( X .no Z ) +no ( X .no C ) ) +no ( A .no B ) ) = ( ( X .no Z ) +no ( ( X .no C ) +no ( A .no B ) ) ) )
46 43 44 45 3eqtr3d 
 |-  ( ph -> ( ( X .no C ) +no ( ( X .no Z ) +no ( A .no B ) ) ) = ( ( X .no Z ) +no ( ( X .no C ) +no ( A .no B ) ) ) )
47 41 46 eleqtrd 
 |-  ( ph -> ( ( X .no C ) +no ( ( X .no B ) +no ( A .no Z ) ) ) e. ( ( X .no Z ) +no ( ( X .no C ) +no ( A .no B ) ) ) )
48 oveq1 
 |-  ( d = X -> ( d .no ( B +no C ) ) = ( X .no ( B +no C ) ) )
49 oveq1 
 |-  ( d = X -> ( d .no B ) = ( X .no B ) )
50 oveq1 
 |-  ( d = X -> ( d .no C ) = ( X .no C ) )
51 49 50 oveq12d 
 |-  ( d = X -> ( ( d .no B ) +no ( d .no C ) ) = ( ( X .no B ) +no ( X .no C ) ) )
52 48 51 eqeq12d 
 |-  ( d = X -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( X .no ( B +no C ) ) = ( ( X .no B ) +no ( X .no C ) ) ) )
53 52 8 4 rspcdva 
 |-  ( ph -> ( X .no ( B +no C ) ) = ( ( X .no B ) +no ( X .no C ) ) )
54 34 38 naddcomd 
 |-  ( ph -> ( ( X .no B ) +no ( X .no C ) ) = ( ( X .no C ) +no ( X .no B ) ) )
55 53 54 eqtrd 
 |-  ( ph -> ( X .no ( B +no C ) ) = ( ( X .no C ) +no ( X .no B ) ) )
56 55 oveq1d 
 |-  ( ph -> ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) = ( ( ( X .no C ) +no ( X .no B ) ) +no ( A .no Z ) ) )
57 38 34 35 naddassd 
 |-  ( ph -> ( ( ( X .no C ) +no ( X .no B ) ) +no ( A .no Z ) ) = ( ( X .no C ) +no ( ( X .no B ) +no ( A .no Z ) ) ) )
58 56 57 eqtrd 
 |-  ( ph -> ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) = ( ( X .no C ) +no ( ( X .no B ) +no ( A .no Z ) ) ) )
59 25 19 naddcomd 
 |-  ( ph -> ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) = ( ( X .no ( Z +no C ) ) +no ( A .no B ) ) )
60 oveq1 
 |-  ( d = X -> ( d .no ( e +no C ) ) = ( X .no ( e +no C ) ) )
61 oveq1 
 |-  ( d = X -> ( d .no e ) = ( X .no e ) )
62 61 50 oveq12d 
 |-  ( d = X -> ( ( d .no e ) +no ( d .no C ) ) = ( ( X .no e ) +no ( X .no C ) ) )
63 60 62 eqeq12d 
 |-  ( d = X -> ( ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> ( X .no ( e +no C ) ) = ( ( X .no e ) +no ( X .no C ) ) ) )
64 oveq1 
 |-  ( e = Z -> ( e +no C ) = ( Z +no C ) )
65 64 oveq2d 
 |-  ( e = Z -> ( X .no ( e +no C ) ) = ( X .no ( Z +no C ) ) )
66 oveq2 
 |-  ( e = Z -> ( X .no e ) = ( X .no Z ) )
67 66 oveq1d 
 |-  ( e = Z -> ( ( X .no e ) +no ( X .no C ) ) = ( ( X .no Z ) +no ( X .no C ) ) )
68 65 67 eqeq12d 
 |-  ( e = Z -> ( ( X .no ( e +no C ) ) = ( ( X .no e ) +no ( X .no C ) ) <-> ( X .no ( Z +no C ) ) = ( ( X .no Z ) +no ( X .no C ) ) ) )
69 63 68 10 4 6 rspc2dv 
 |-  ( ph -> ( X .no ( Z +no C ) ) = ( ( X .no Z ) +no ( X .no C ) ) )
70 69 oveq1d 
 |-  ( ph -> ( ( X .no ( Z +no C ) ) +no ( A .no B ) ) = ( ( ( X .no Z ) +no ( X .no C ) ) +no ( A .no B ) ) )
71 70 45 eqtrd 
 |-  ( ph -> ( ( X .no ( Z +no C ) ) +no ( A .no B ) ) = ( ( X .no Z ) +no ( ( X .no C ) +no ( A .no B ) ) ) )
72 59 71 eqtrd 
 |-  ( ph -> ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) = ( ( X .no Z ) +no ( ( X .no C ) +no ( A .no B ) ) ) )
73 47 58 72 3eltr4d 
 |-  ( ph -> ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) e. ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) )
74 13 14 nmulcld 
 |-  ( ph -> ( X .no ( B +no C ) ) e. On )
75 74 35 naddcld 
 |-  ( ph -> ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) e. On )
76 25 19 naddcld 
 |-  ( ph -> ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) e. On )
77 naddel1 
 |-  ( ( ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) e. On /\ ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) e. On /\ ( A .no Y ) e. On ) -> ( ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) e. ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) <-> ( ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) +no ( A .no Y ) ) e. ( ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) +no ( A .no Y ) ) ) )
78 75 76 20 77 syl3anc 
 |-  ( ph -> ( ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) e. ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) <-> ( ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) +no ( A .no Y ) ) e. ( ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) +no ( A .no Y ) ) ) )
79 73 78 mpbid 
 |-  ( ph -> ( ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) +no ( A .no Y ) ) e. ( ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) +no ( A .no Y ) ) )
80 74 35 20 nadd32d 
 |-  ( ph -> ( ( ( X .no ( B +no C ) ) +no ( A .no Z ) ) +no ( A .no Y ) ) = ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) +no ( A .no Z ) ) )
81 25 19 20 naddassd 
 |-  ( ph -> ( ( ( A .no B ) +no ( X .no ( Z +no C ) ) ) +no ( A .no Y ) ) = ( ( A .no B ) +no ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) ) )
82 79 80 81 3eltr3d 
 |-  ( ph -> ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) +no ( A .no Z ) ) e. ( ( A .no B ) +no ( ( X .no ( Z +no C ) ) +no ( A .no Y ) ) ) )
83 28 82 sseldd 
 |-  ( ph -> ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) +no ( A .no Z ) ) e. ( ( A .no B ) +no ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) ) )
84 25 22 23 naddassd 
 |-  ( ph -> ( ( ( A .no B ) +no ( A .no ( Z +no C ) ) ) +no ( X .no Y ) ) = ( ( A .no B ) +no ( ( A .no ( Z +no C ) ) +no ( X .no Y ) ) ) )
85 83 84 eleqtrrd 
 |-  ( ph -> ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) +no ( A .no Z ) ) e. ( ( ( A .no B ) +no ( A .no ( Z +no C ) ) ) +no ( X .no Y ) ) )
86 64 oveq2d 
 |-  ( e = Z -> ( A .no ( e +no C ) ) = ( A .no ( Z +no C ) ) )
87 oveq2 
 |-  ( e = Z -> ( A .no e ) = ( A .no Z ) )
88 87 oveq1d 
 |-  ( e = Z -> ( ( A .no e ) +no ( A .no C ) ) = ( ( A .no Z ) +no ( A .no C ) ) )
89 86 88 eqeq12d 
 |-  ( e = Z -> ( ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> ( A .no ( Z +no C ) ) = ( ( A .no Z ) +no ( A .no C ) ) ) )
90 89 9 6 rspcdva 
 |-  ( ph -> ( A .no ( Z +no C ) ) = ( ( A .no Z ) +no ( A .no C ) ) )
91 1 3 nmulcld 
 |-  ( ph -> ( A .no C ) e. On )
92 35 91 naddcomd 
 |-  ( ph -> ( ( A .no Z ) +no ( A .no C ) ) = ( ( A .no C ) +no ( A .no Z ) ) )
93 90 92 eqtrd 
 |-  ( ph -> ( A .no ( Z +no C ) ) = ( ( A .no C ) +no ( A .no Z ) ) )
94 93 oveq2d 
 |-  ( ph -> ( ( A .no B ) +no ( A .no ( Z +no C ) ) ) = ( ( A .no B ) +no ( ( A .no C ) +no ( A .no Z ) ) ) )
95 25 91 35 naddassd 
 |-  ( ph -> ( ( ( A .no B ) +no ( A .no C ) ) +no ( A .no Z ) ) = ( ( A .no B ) +no ( ( A .no C ) +no ( A .no Z ) ) ) )
96 94 95 eqtr4d 
 |-  ( ph -> ( ( A .no B ) +no ( A .no ( Z +no C ) ) ) = ( ( ( A .no B ) +no ( A .no C ) ) +no ( A .no Z ) ) )
97 96 oveq1d 
 |-  ( ph -> ( ( ( A .no B ) +no ( A .no ( Z +no C ) ) ) +no ( X .no Y ) ) = ( ( ( ( A .no B ) +no ( A .no C ) ) +no ( A .no Z ) ) +no ( X .no Y ) ) )
98 25 91 naddcld 
 |-  ( ph -> ( ( A .no B ) +no ( A .no C ) ) e. On )
99 98 35 23 nadd32d 
 |-  ( ph -> ( ( ( ( A .no B ) +no ( A .no C ) ) +no ( A .no Z ) ) +no ( X .no Y ) ) = ( ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) +no ( A .no Z ) ) )
100 97 99 eqtrd 
 |-  ( ph -> ( ( ( A .no B ) +no ( A .no ( Z +no C ) ) ) +no ( X .no Y ) ) = ( ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) +no ( A .no Z ) ) )
101 85 100 eleqtrd 
 |-  ( ph -> ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) +no ( A .no Z ) ) e. ( ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) +no ( A .no Z ) ) )
102 74 20 naddcld 
 |-  ( ph -> ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) e. On )
103 98 23 naddcld 
 |-  ( ph -> ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) e. On )
104 naddel1 
 |-  ( ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) e. On /\ ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) e. On /\ ( A .no Z ) e. On ) -> ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) <-> ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) +no ( A .no Z ) ) e. ( ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) +no ( A .no Z ) ) ) )
105 102 103 35 104 syl3anc 
 |-  ( ph -> ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) <-> ( ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) +no ( A .no Z ) ) e. ( ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) +no ( A .no Z ) ) ) )
106 101 105 mpbird 
 |-  ( ph -> ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) )