Metamath Proof Explorer

Theorem nadddilem2

Description: Lemma for nadddi . Prove the reverse implication. (Contributed by Scott Fenton, 31-Jul-2026)

Ref Expression
Hypotheses nadddilem2.1 
|- ( ph -> A e. On )
nadddilem2.2 
|- ( ph -> B e. On )
nadddilem2.3 
|- ( ph -> C e. On )
nadddilem2.4 
|- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
nadddilem2.5 
|- ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) )
nadddilem2.6 
|- ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) )
nadddilem2.7 
|- ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) )
nadddilem2.8 
|- ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) )
Assertion nadddilem2 
|- ( ph -> ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) )

Proof

Step Hyp Ref Expression
1 nadddilem2.1 
 |-  ( ph -> A e. On )
2 nadddilem2.2 
 |-  ( ph -> B e. On )
3 nadddilem2.3 
 |-  ( ph -> C e. On )
4 nadddilem2.4 
 |-  ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
5 nadddilem2.5 
 |-  ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) )
6 nadddilem2.6 
 |-  ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) )
7 nadddilem2.7 
 |-  ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) )
8 nadddilem2.8 
 |-  ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) )
9 oveq1 
 |-  ( d = p -> ( d .no ( B +no C ) ) = ( p .no ( B +no C ) ) )
10 oveq1 
 |-  ( d = p -> ( d .no B ) = ( p .no B ) )
11 oveq1 
 |-  ( d = p -> ( d .no C ) = ( p .no C ) )
12 10 11 oveq12d 
 |-  ( d = p -> ( ( d .no B ) +no ( d .no C ) ) = ( ( p .no B ) +no ( p .no C ) ) )
13 9 12 eqeq12d 
 |-  ( d = p -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) )
14 13 cbvralvw 
 |-  ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) )
15 2 3 naddcomd 
 |-  ( ph -> ( B +no C ) = ( C +no B ) )
16 15 oveq2d 
 |-  ( ph -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) )
17 16 adantr 
 |-  ( ( ph /\ p e. A ) -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) )
18 1 adantr 
 |-  ( ( ph /\ p e. A ) -> A e. On )
19 simpr 
 |-  ( ( ph /\ p e. A ) -> p e. A )
20 18 19 onelond 
 |-  ( ( ph /\ p e. A ) -> p e. On )
21 2 adantr 
 |-  ( ( ph /\ p e. A ) -> B e. On )
22 20 21 nmulcld 
 |-  ( ( ph /\ p e. A ) -> ( p .no B ) e. On )
23 3 adantr 
 |-  ( ( ph /\ p e. A ) -> C e. On )
24 20 23 nmulcld 
 |-  ( ( ph /\ p e. A ) -> ( p .no C ) e. On )
25 22 24 naddcomd 
 |-  ( ( ph /\ p e. A ) -> ( ( p .no B ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no B ) ) )
26 17 25 eqeq12d 
 |-  ( ( ph /\ p e. A ) -> ( ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) )
27 26 ralbidva 
 |-  ( ph -> ( A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) )
28 14 27 bitrid 
 |-  ( ph -> ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) )
29 4 28 mpbid 
 |-  ( ph -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) )
30 oveq1 
 |-  ( e = q -> ( e +no C ) = ( q +no C ) )
31 30 oveq2d 
 |-  ( e = q -> ( A .no ( e +no C ) ) = ( A .no ( q +no C ) ) )
32 oveq2 
 |-  ( e = q -> ( A .no e ) = ( A .no q ) )
33 32 oveq1d 
 |-  ( e = q -> ( ( A .no e ) +no ( A .no C ) ) = ( ( A .no q ) +no ( A .no C ) ) )
34 31 33 eqeq12d 
 |-  ( e = q -> ( ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) ) )
35 34 cbvralvw 
 |-  ( A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) )
36 2 adantr 
 |-  ( ( ph /\ q e. B ) -> B e. On )
37 simpr 
 |-  ( ( ph /\ q e. B ) -> q e. B )
38 36 37 onelond 
 |-  ( ( ph /\ q e. B ) -> q e. On )
39 3 adantr 
 |-  ( ( ph /\ q e. B ) -> C e. On )
40 38 39 naddcomd 
 |-  ( ( ph /\ q e. B ) -> ( q +no C ) = ( C +no q ) )
41 40 oveq2d 
 |-  ( ( ph /\ q e. B ) -> ( A .no ( q +no C ) ) = ( A .no ( C +no q ) ) )
42 1 adantr 
 |-  ( ( ph /\ q e. B ) -> A e. On )
43 42 38 nmulcld 
 |-  ( ( ph /\ q e. B ) -> ( A .no q ) e. On )
44 42 39 nmulcld 
 |-  ( ( ph /\ q e. B ) -> ( A .no C ) e. On )
45 43 44 naddcomd 
 |-  ( ( ph /\ q e. B ) -> ( ( A .no q ) +no ( A .no C ) ) = ( ( A .no C ) +no ( A .no q ) ) )
46 41 45 eqeq12d 
 |-  ( ( ph /\ q e. B ) -> ( ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) <-> ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) )
47 46 ralbidva 
 |-  ( ph -> ( A. q e. B ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) )
48 35 47 bitrid 
 |-  ( ph -> ( A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) )
49 5 48 mpbid 
 |-  ( ph -> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) )
50 oveq1 
 |-  ( d = p -> ( d .no ( e +no C ) ) = ( p .no ( e +no C ) ) )
51 oveq1 
 |-  ( d = p -> ( d .no e ) = ( p .no e ) )
52 51 11 oveq12d 
 |-  ( d = p -> ( ( d .no e ) +no ( d .no C ) ) = ( ( p .no e ) +no ( p .no C ) ) )
53 50 52 eqeq12d 
 |-  ( d = p -> ( ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> ( p .no ( e +no C ) ) = ( ( p .no e ) +no ( p .no C ) ) ) )
54 30 oveq2d 
 |-  ( e = q -> ( p .no ( e +no C ) ) = ( p .no ( q +no C ) ) )
55 oveq2 
 |-  ( e = q -> ( p .no e ) = ( p .no q ) )
56 55 oveq1d 
 |-  ( e = q -> ( ( p .no e ) +no ( p .no C ) ) = ( ( p .no q ) +no ( p .no C ) ) )
57 54 56 eqeq12d 
 |-  ( e = q -> ( ( p .no ( e +no C ) ) = ( ( p .no e ) +no ( p .no C ) ) <-> ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) ) )
58 53 57 cbvral2vw 
 |-  ( A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> A. p e. A A. q e. B ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) )
59 40 adantrl 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( q +no C ) = ( C +no q ) )
60 59 oveq2d 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no ( q +no C ) ) = ( p .no ( C +no q ) ) )
61 20 adantrr 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> p e. On )
62 38 adantrl 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> q e. On )
63 61 62 nmulcld 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no q ) e. On )
64 3 adantr 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> C e. On )
65 61 64 nmulcld 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no C ) e. On )
66 63 65 naddcomd 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( ( p .no q ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no q ) ) )
67 60 66 eqeq12d 
 |-  ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) <-> ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) )
68 67 2ralbidva 
 |-  ( ph -> ( A. p e. A A. q e. B ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) <-> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) )
69 58 68 bitrid 
 |-  ( ph -> ( A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) )
70 7 69 mpbid 
 |-  ( ph -> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) )
71 1 3 2 29 49 70 nadddilem1 
 |-  ( ( ph /\ x e. ( A .no B ) ) -> ( ( A .no C ) +no x ) e. ( A .no ( C +no B ) ) )
72 1 2 nmulcld 
 |-  ( ph -> ( A .no B ) e. On )
73 72 adantr 
 |-  ( ( ph /\ x e. ( A .no B ) ) -> ( A .no B ) e. On )
74 simpr 
 |-  ( ( ph /\ x e. ( A .no B ) ) -> x e. ( A .no B ) )
75 73 74 onelond 
 |-  ( ( ph /\ x e. ( A .no B ) ) -> x e. On )
76 1 3 nmulcld 
 |-  ( ph -> ( A .no C ) e. On )
77 76 adantr 
 |-  ( ( ph /\ x e. ( A .no B ) ) -> ( A .no C ) e. On )
78 75 77 naddcomd 
 |-  ( ( ph /\ x e. ( A .no B ) ) -> ( x +no ( A .no C ) ) = ( ( A .no C ) +no x ) )
79 15 oveq2d 
 |-  ( ph -> ( A .no ( B +no C ) ) = ( A .no ( C +no B ) ) )
80 79 adantr 
 |-  ( ( ph /\ x e. ( A .no B ) ) -> ( A .no ( B +no C ) ) = ( A .no ( C +no B ) ) )
81 71 78 80 3eltr4d 
 |-  ( ( ph /\ x e. ( A .no B ) ) -> ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) )
82 81 ralrimiva 
 |-  ( ph -> A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) )
83 1 2 3 4 6 8 nadddilem1 
 |-  ( ( ph /\ y e. ( A .no C ) ) -> ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) )
84 83 ralrimiva 
 |-  ( ph -> A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) )
85 2 3 naddcld 
 |-  ( ph -> ( B +no C ) e. On )
86 1 85 nmulcld 
 |-  ( ph -> ( A .no ( B +no C ) ) e. On )
87 naddle 
 |-  ( ( ( A .no B ) e. On /\ ( A .no C ) e. On /\ ( A .no ( B +no C ) ) e. On ) -> ( ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) <-> ( A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) /\ A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) ) ) )
88 72 76 86 87 syl3anc 
 |-  ( ph -> ( ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) <-> ( A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) /\ A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) ) ) )
89 82 84 88 mpbir2and 
 |-  ( ph -> ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) )