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 ⊢ ( 𝜑 → 𝐴 ∈ On )
nadddilem3.2 ⊢ ( 𝜑 → 𝐵 ∈ On )
nadddilem3.3 ⊢ ( 𝜑 → 𝐶 ∈ On )
nadddilem3.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
nadddilem3.5 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 +no 𝐶 ) )
nadddilem3.6 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
nadddilem3.7 ⊢ ( 𝜑 → 𝑌 ⊆ ( 𝑍 +no 𝐶 ) )
nadddilem3.8 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) )
nadddilem3.9 ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝐵 ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) )
nadddilem3.10 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐵 ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) )
Assertion nadddilem3 ( 𝜑 → ( ( 𝑋 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑌 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑋 ·no 𝑌 ) ) )

Proof

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