Metamath Proof Explorer

Theorem nadddilem1

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

Ref Expression
Hypotheses nadddilem1.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
nadddilem1.2 ⊢ ( 𝜑 → 𝐵 ∈ On )
nadddilem1.3 ⊢ ( 𝜑 → 𝐶 ∈ On )
nadddilem1.4 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) )
nadddilem1.5 ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) )
nadddilem1.6 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑓 ∈ 𝐶 ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) )
Assertion nadddilem1 ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 nadddilem1.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 nadddilem1.2 ⊢ ( 𝜑 → 𝐵 ∈ On )
3 nadddilem1.3 ⊢ ( 𝜑 → 𝐶 ∈ On )
4 nadddilem1.4 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) )
5 nadddilem1.5 ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) )
6 nadddilem1.6 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑓 ∈ 𝐶 ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → 𝐴 ∈ On )
8 3 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → 𝐶 ∈ On )
9 7 8 nmulcld ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → ( 𝐴 ·no 𝐶 ) ∈ On )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → 𝑌 ∈ ( 𝐴 ·no 𝐶 ) )
11 9 10 onelond ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → 𝑌 ∈ On )
12 ltnmul ⊢ ( ( 𝑌 ∈ On ∧ 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) )
13 11 7 8 12 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → ( 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) )
14 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → 𝐴 ∈ On )
15 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → 𝐵 ∈ On )
16 14 15 nmulcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝐴 ·no 𝐵 ) ∈ On )
17 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → 𝑌 ∈ On )
18 simprll ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → 𝑧 ∈ 𝐴 )
19 14 18 onelond ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → 𝑧 ∈ On )
20 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → 𝐶 ∈ On )
21 simprlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → 𝑤 ∈ 𝐶 )
22 20 21 onelond ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → 𝑤 ∈ On )
23 19 22 nmulcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑧 ·no 𝑤 ) ∈ On )
24 16 17 23 naddassd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) +no ( 𝑧 ·no 𝑤 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ) )
25 17 23 naddcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ∈ On )
26 16 25 naddcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ) ∈ On )
27 15 20 naddcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝐵 +no 𝐶 ) ∈ On )
28 14 27 nmulcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ∈ On )
29 28 23 naddcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) ∈ On )
30 simprr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) )
31 19 20 nmulcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑧 ·no 𝐶 ) ∈ On )
32 14 22 nmulcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝐴 ·no 𝑤 ) ∈ On )
33 31 32 naddcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ∈ On )
34 naddss2 ⊢ ( ( ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ∈ On ∧ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ∈ On ∧ ( 𝐴 ·no 𝐵 ) ∈ On ) → ( ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ↔ ( ( 𝐴 ·no 𝐵 ) +no ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) )
35 25 33 16 34 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ↔ ( ( 𝐴 ·no 𝐵 ) +no ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) )
36 30 35 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) )
37 oveq2 ⊢ ( 𝑓 = 𝑤 → ( 𝐵 +no 𝑓 ) = ( 𝐵 +no 𝑤 ) )
38 37 oveq2d ⊢ ( 𝑓 = 𝑤 → ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) )
39 oveq2 ⊢ ( 𝑓 = 𝑤 → ( 𝐴 ·no 𝑓 ) = ( 𝐴 ·no 𝑤 ) )
40 39 oveq2d ⊢ ( 𝑓 = 𝑤 → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑤 ) ) )
41 38 40 eqeq12d ⊢ ( 𝑓 = 𝑤 → ( ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) ↔ ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑤 ) ) ) )
42 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ∀ 𝑓 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) )
43 41 42 21 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑤 ) ) )
44 43 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) = ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) )
45 16 32 31 nadd32d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) = ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝑧 ·no 𝐶 ) ) +no ( 𝐴 ·no 𝑤 ) ) )
46 16 31 32 naddassd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝑧 ·no 𝐶 ) ) +no ( 𝐴 ·no 𝑤 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) )
47 44 45 46 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no 𝐵 ) +no ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) = ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) )
48 naddel2 ⊢ ( ( 𝑤 ∈ On ∧ 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑤 ∈ 𝐶 ↔ ( 𝐵 +no 𝑤 ) ∈ ( 𝐵 +no 𝐶 ) ) )
49 22 20 15 48 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑤 ∈ 𝐶 ↔ ( 𝐵 +no 𝑤 ) ∈ ( 𝐵 +no 𝐶 ) ) )
50 21 49 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝐵 +no 𝑤 ) ∈ ( 𝐵 +no 𝐶 ) )
51 nmuladdel ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 +no 𝐶 ) ∈ On ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐵 +no 𝑤 ) ∈ ( 𝐵 +no 𝐶 ) ) ) → ( ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no ( 𝐵 +no 𝑤 ) ) ) )
52 14 27 18 50 51 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no ( 𝐵 +no 𝑤 ) ) ) )
53 15 22 naddcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝐵 +no 𝑤 ) ∈ On )
54 14 53 nmulcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) ∈ On )
55 19 15 nmulcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑧 ·no 𝐵 ) ∈ On )
56 54 31 55 naddassd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) +no ( 𝑧 ·no 𝐵 ) ) = ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( ( 𝑧 ·no 𝐶 ) +no ( 𝑧 ·no 𝐵 ) ) ) )
57 oveq1 ⊢ ( 𝑑 = 𝑧 → ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) )
58 oveq1 ⊢ ( 𝑑 = 𝑧 → ( 𝑑 ·no 𝐵 ) = ( 𝑧 ·no 𝐵 ) )
59 oveq1 ⊢ ( 𝑑 = 𝑧 → ( 𝑑 ·no 𝐶 ) = ( 𝑧 ·no 𝐶 ) )
60 58 59 oveq12d ⊢ ( 𝑑 = 𝑧 → ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝐶 ) ) )
61 57 60 eqeq12d ⊢ ( 𝑑 = 𝑧 → ( ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝐶 ) ) ) )
62 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) )
63 61 62 18 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝐶 ) ) )
64 55 31 naddcomd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝐶 ) ) = ( ( 𝑧 ·no 𝐶 ) +no ( 𝑧 ·no 𝐵 ) ) )
65 63 64 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑧 ·no 𝐶 ) +no ( 𝑧 ·no 𝐵 ) ) )
66 65 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) ) = ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( ( 𝑧 ·no 𝐶 ) +no ( 𝑧 ·no 𝐵 ) ) ) )
67 56 66 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) +no ( 𝑧 ·no 𝐵 ) ) = ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) ) )
68 19 27 nmulcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) ∈ On )
69 54 68 naddcomd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) ) = ( ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) ) )
70 67 69 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) +no ( 𝑧 ·no 𝐵 ) ) = ( ( 𝑧 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) ) )
71 28 23 55 naddassd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) +no ( 𝑧 ·no 𝐵 ) ) = ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( ( 𝑧 ·no 𝑤 ) +no ( 𝑧 ·no 𝐵 ) ) ) )
72 23 55 naddcomd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝑧 ·no 𝑤 ) +no ( 𝑧 ·no 𝐵 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝑤 ) ) )
73 oveq1 ⊢ ( 𝑑 = 𝑧 → ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( 𝑧 ·no ( 𝐵 +no 𝑓 ) ) )
74 oveq1 ⊢ ( 𝑑 = 𝑧 → ( 𝑑 ·no 𝑓 ) = ( 𝑧 ·no 𝑓 ) )
75 58 74 oveq12d ⊢ ( 𝑑 = 𝑧 → ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝑓 ) ) )
76 73 75 eqeq12d ⊢ ( 𝑑 = 𝑧 → ( ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) ↔ ( 𝑧 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝑓 ) ) ) )
77 37 oveq2d ⊢ ( 𝑓 = 𝑤 → ( 𝑧 ·no ( 𝐵 +no 𝑓 ) ) = ( 𝑧 ·no ( 𝐵 +no 𝑤 ) ) )
78 oveq2 ⊢ ( 𝑓 = 𝑤 → ( 𝑧 ·no 𝑓 ) = ( 𝑧 ·no 𝑤 ) )
79 78 oveq2d ⊢ ( 𝑓 = 𝑤 → ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝑓 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝑤 ) ) )
80 77 79 eqeq12d ⊢ ( 𝑓 = 𝑤 → ( ( 𝑧 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝑓 ) ) ↔ ( 𝑧 ·no ( 𝐵 +no 𝑤 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝑤 ) ) ) )
81 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ∀ 𝑑 ∈ 𝐴 ∀ 𝑓 ∈ 𝐶 ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) )
82 76 80 81 18 21 rspc2dv ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( 𝑧 ·no ( 𝐵 +no 𝑤 ) ) = ( ( 𝑧 ·no 𝐵 ) +no ( 𝑧 ·no 𝑤 ) ) )
83 72 82 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝑧 ·no 𝑤 ) +no ( 𝑧 ·no 𝐵 ) ) = ( 𝑧 ·no ( 𝐵 +no 𝑤 ) ) )
84 83 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( ( 𝑧 ·no 𝑤 ) +no ( 𝑧 ·no 𝐵 ) ) ) = ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no ( 𝐵 +no 𝑤 ) ) ) )
85 71 84 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) +no ( 𝑧 ·no 𝐵 ) ) = ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no ( 𝐵 +no 𝑤 ) ) ) )
86 52 70 85 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) +no ( 𝑧 ·no 𝐵 ) ) ∈ ( ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) +no ( 𝑧 ·no 𝐵 ) ) )
87 54 31 naddcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) ∈ On )
88 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 𝐵 ) ) ) )
89 87 29 55 88 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) ↔ ( ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) +no ( 𝑧 ·no 𝐵 ) ) ∈ ( ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) +no ( 𝑧 ·no 𝐵 ) ) ) )
90 86 89 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no ( 𝐵 +no 𝑤 ) ) +no ( 𝑧 ·no 𝐶 ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) )
91 47 90 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no 𝐵 ) +no ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) )
92 26 29 36 91 ontr2d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) )
93 24 92 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) +no ( 𝑧 ·no 𝑤 ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) )
94 16 17 naddcld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ On )
95 naddel1 ⊢ ( ( ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ On ∧ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ∈ On ∧ ( 𝑧 ·no 𝑤 ) ∈ On ) → ( ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ↔ ( ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) +no ( 𝑧 ·no 𝑤 ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) ) )
96 94 28 23 95 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ↔ ( ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) +no ( 𝑧 ·no 𝑤 ) ) ∈ ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝑧 ·no 𝑤 ) ) ) )
97 93 96 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ∧ ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) ) ) → ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) )
98 97 expr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐶 ) ) → ( ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) → ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ) )
99 98 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 ( 𝑌 +no ( 𝑧 ·no 𝑤 ) ) ⊆ ( ( 𝑧 ·no 𝐶 ) +no ( 𝐴 ·no 𝑤 ) ) → ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ) )
100 13 99 sylbid ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → ( 𝑌 ∈ ( 𝐴 ·no 𝐶 ) → ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ) )
101 100 syldbl2 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐴 ·no 𝐶 ) ) → ( ( 𝐴 ·no 𝐵 ) +no 𝑌 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) )