Metamath Proof Explorer

Theorem nadddilem4

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

Ref Expression
Hypotheses nadddilem4.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
nadddilem4.2 ⊢ ( 𝜑 → 𝐵 ∈ On )
nadddilem4.3 ⊢ ( 𝜑 → 𝐶 ∈ On )
nadddilem4.4 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) )
nadddilem4.5 ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝐵 ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) )
nadddilem4.6 ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) )
nadddilem4.7 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐵 ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) )
nadddilem4.8 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑓 ∈ 𝐶 ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) )
Assertion nadddilem4 ( 𝜑 → ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 nadddilem4.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 nadddilem4.2 ⊢ ( 𝜑 → 𝐵 ∈ On )
3 nadddilem4.3 ⊢ ( 𝜑 → 𝐶 ∈ On )
4 nadddilem4.4 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) )
5 nadddilem4.5 ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝐵 ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) )
6 nadddilem4.6 ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) )
7 nadddilem4.7 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐵 ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) )
8 nadddilem4.8 ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑓 ∈ 𝐶 ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) )
9 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → 𝑦 ∈ ( 𝐵 +no 𝐶 ) )
10 2 3 naddcld ⊢ ( 𝜑 → ( 𝐵 +no 𝐶 ) ∈ On )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → ( 𝐵 +no 𝐶 ) ∈ On )
12 11 9 onelond ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → 𝑦 ∈ On )
13 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → 𝐵 ∈ On )
14 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → 𝐶 ∈ On )
15 ltnadd ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑦 ∈ ( 𝐵 +no 𝐶 ) ↔ ( ∃ 𝑧 ∈ 𝐵 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ∨ ∃ 𝑤 ∈ 𝐶 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) )
16 12 13 14 15 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → ( 𝑦 ∈ ( 𝐵 +no 𝐶 ) ↔ ( ∃ 𝑧 ∈ 𝐵 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ∨ ∃ 𝑤 ∈ 𝐶 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) )
17 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → 𝐴 ∈ On )
18 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → 𝐵 ∈ On )
19 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → 𝐶 ∈ On )
20 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → 𝑥 ∈ 𝐴 )
21 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → 𝑦 ∈ ( 𝐵 +no 𝐶 ) )
22 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → 𝑧 ∈ 𝐵 )
23 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → 𝑦 ⊆ ( 𝑧 +no 𝐶 ) )
24 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) )
25 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → ∀ 𝑒 ∈ 𝐵 ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) )
26 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐵 ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) )
27 17 18 19 20 21 22 23 24 25 26 nadddilem3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ) ) → ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) )
28 27 rexlimdvaa ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → ( ∃ 𝑧 ∈ 𝐵 𝑦 ⊆ ( 𝑧 +no 𝐶 ) → ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) ) )
29 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝐴 ∈ On )
30 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝐶 ∈ On )
31 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝐵 ∈ On )
32 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝑥 ∈ 𝐴 )
33 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝑦 ∈ ( 𝐵 +no 𝐶 ) )
34 31 30 naddcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( 𝐵 +no 𝐶 ) = ( 𝐶 +no 𝐵 ) )
35 33 34 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝑦 ∈ ( 𝐶 +no 𝐵 ) )
36 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝑤 ∈ 𝐶 )
37 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝑦 ⊆ ( 𝐵 +no 𝑤 ) )
38 30 36 onelond ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝑤 ∈ On )
39 31 38 naddcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( 𝐵 +no 𝑤 ) = ( 𝑤 +no 𝐵 ) )
40 37 39 sseqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → 𝑦 ⊆ ( 𝑤 +no 𝐵 ) )
41 oveq1 ⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) )
42 oveq1 ⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no 𝐵 ) = ( 𝑝 ·no 𝐵 ) )
43 oveq1 ⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no 𝐶 ) = ( 𝑝 ·no 𝐶 ) )
44 42 43 oveq12d ⊢ ( 𝑑 = 𝑝 → ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) )
45 41 44 eqeq12d ⊢ ( 𝑑 = 𝑝 → ( ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) ) )
46 45 cbvralvw ⊢ ( ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) )
47 2 3 naddcomd ⊢ ( 𝜑 → ( 𝐵 +no 𝐶 ) = ( 𝐶 +no 𝐵 ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝐵 +no 𝐶 ) = ( 𝐶 +no 𝐵 ) )
49 48 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) )
50 1 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝐴 ∈ On )
51 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
52 50 51 onelond ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ On )
53 2 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝐵 ∈ On )
54 52 53 nmulcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ·no 𝐵 ) ∈ On )
55 3 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝐶 ∈ On )
56 52 55 nmulcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ·no 𝐶 ) ∈ On )
57 54 56 naddcomd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) )
58 49 57 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) ↔ ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
59 58 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
60 46 59 bitrid ⊢ ( 𝜑 → ( ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
61 4 60 mpbid ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) )
63 oveq2 ⊢ ( 𝑓 = 𝑞 → ( 𝐵 +no 𝑓 ) = ( 𝐵 +no 𝑞 ) )
64 63 oveq2d ⊢ ( 𝑓 = 𝑞 → ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( 𝐴 ·no ( 𝐵 +no 𝑞 ) ) )
65 oveq2 ⊢ ( 𝑓 = 𝑞 → ( 𝐴 ·no 𝑓 ) = ( 𝐴 ·no 𝑞 ) )
66 65 oveq2d ⊢ ( 𝑓 = 𝑞 → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑞 ) ) )
67 64 66 eqeq12d ⊢ ( 𝑓 = 𝑞 → ( ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) ↔ ( 𝐴 ·no ( 𝐵 +no 𝑞 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑞 ) ) ) )
68 67 cbvralvw ⊢ ( ∀ 𝑓 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) ↔ ∀ 𝑞 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑞 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑞 ) ) )
69 2 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → 𝐵 ∈ On )
70 3 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → 𝐶 ∈ On )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → 𝑞 ∈ 𝐶 )
72 70 71 onelond ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → 𝑞 ∈ On )
73 69 72 naddcomd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → ( 𝐵 +no 𝑞 ) = ( 𝑞 +no 𝐵 ) )
74 73 oveq2d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → ( 𝐴 ·no ( 𝐵 +no 𝑞 ) ) = ( 𝐴 ·no ( 𝑞 +no 𝐵 ) ) )
75 1 2 nmulcld ⊢ ( 𝜑 → ( 𝐴 ·no 𝐵 ) ∈ On )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → ( 𝐴 ·no 𝐵 ) ∈ On )
77 1 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → 𝐴 ∈ On )
78 77 72 nmulcld ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → ( 𝐴 ·no 𝑞 ) ∈ On )
79 76 78 naddcomd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑞 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐵 ) ) )
80 74 79 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐶 ) → ( ( 𝐴 ·no ( 𝐵 +no 𝑞 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑞 ) ) ↔ ( 𝐴 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐵 ) ) ) )
81 80 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑞 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑞 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑞 ) ) ↔ ∀ 𝑞 ∈ 𝐶 ( 𝐴 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐵 ) ) ) )
82 68 81 bitrid ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) ↔ ∀ 𝑞 ∈ 𝐶 ( 𝐴 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐵 ) ) ) )
83 6 82 mpbid ⊢ ( 𝜑 → ∀ 𝑞 ∈ 𝐶 ( 𝐴 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐵 ) ) )
84 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ∀ 𝑞 ∈ 𝐶 ( 𝐴 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐵 ) ) )
85 oveq1 ⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( 𝑝 ·no ( 𝐵 +no 𝑓 ) ) )
86 oveq1 ⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no 𝑓 ) = ( 𝑝 ·no 𝑓 ) )
87 42 86 oveq12d ⊢ ( 𝑑 = 𝑝 → ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑓 ) ) )
88 85 87 eqeq12d ⊢ ( 𝑑 = 𝑝 → ( ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) ↔ ( 𝑝 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑓 ) ) ) )
89 63 oveq2d ⊢ ( 𝑓 = 𝑞 → ( 𝑝 ·no ( 𝐵 +no 𝑓 ) ) = ( 𝑝 ·no ( 𝐵 +no 𝑞 ) ) )
90 oveq2 ⊢ ( 𝑓 = 𝑞 → ( 𝑝 ·no 𝑓 ) = ( 𝑝 ·no 𝑞 ) )
91 90 oveq2d ⊢ ( 𝑓 = 𝑞 → ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑓 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑞 ) ) )
92 89 91 eqeq12d ⊢ ( 𝑓 = 𝑞 → ( ( 𝑝 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑓 ) ) ↔ ( 𝑝 ·no ( 𝐵 +no 𝑞 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑞 ) ) ) )
93 88 92 cbvral2vw ⊢ ( ∀ 𝑑 ∈ 𝐴 ∀ 𝑓 ∈ 𝐶 ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐶 ( 𝑝 ·no ( 𝐵 +no 𝑞 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑞 ) ) )
94 73 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐶 ) ) → ( 𝐵 +no 𝑞 ) = ( 𝑞 +no 𝐵 ) )
95 94 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐶 ) ) → ( 𝑝 ·no ( 𝐵 +no 𝑞 ) ) = ( 𝑝 ·no ( 𝑞 +no 𝐵 ) ) )
96 54 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐶 ) ) → ( 𝑝 ·no 𝐵 ) ∈ On )
97 52 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐶 ) ) → 𝑝 ∈ On )
98 72 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐶 ) ) → 𝑞 ∈ On )
99 97 98 nmulcld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐶 ) ) → ( 𝑝 ·no 𝑞 ) ∈ On )
100 96 99 naddcomd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐶 ) ) → ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑞 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐵 ) ) )
101 95 100 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐶 ) ) → ( ( 𝑝 ·no ( 𝐵 +no 𝑞 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑞 ) ) ↔ ( 𝑝 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
102 101 2ralbidva ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐶 ( 𝑝 ·no ( 𝐵 +no 𝑞 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝑞 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐶 ( 𝑝 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
103 93 102 bitrid ⊢ ( 𝜑 → ( ∀ 𝑑 ∈ 𝐴 ∀ 𝑓 ∈ 𝐶 ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐶 ( 𝑝 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
104 8 103 mpbid ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐶 ( 𝑝 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐵 ) ) )
105 104 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐶 ( 𝑝 ·no ( 𝑞 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐵 ) ) )
106 29 30 31 32 35 36 40 62 84 105 nadddilem3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( ( 𝑥 ·no ( 𝐶 +no 𝐵 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐶 ) +no ( 𝐴 ·no 𝐵 ) ) +no ( 𝑥 ·no 𝑦 ) ) )
107 34 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝑥 ·no ( 𝐶 +no 𝐵 ) ) )
108 107 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) = ( ( 𝑥 ·no ( 𝐶 +no 𝐵 ) ) +no ( 𝐴 ·no 𝑦 ) ) )
109 75 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( 𝐴 ·no 𝐵 ) ∈ On )
110 1 3 nmulcld ⊢ ( 𝜑 → ( 𝐴 ·no 𝐶 ) ∈ On )
111 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( 𝐴 ·no 𝐶 ) ∈ On )
112 109 111 naddcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) = ( ( 𝐴 ·no 𝐶 ) +no ( 𝐴 ·no 𝐵 ) ) )
113 112 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) = ( ( ( 𝐴 ·no 𝐶 ) +no ( 𝐴 ·no 𝐵 ) ) +no ( 𝑥 ·no 𝑦 ) ) )
114 106 108 113 3eltr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) ) → ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) )
115 114 rexlimdvaa ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → ( ∃ 𝑤 ∈ 𝐶 𝑦 ⊆ ( 𝐵 +no 𝑤 ) → ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) ) )
116 28 115 jaod ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → ( ( ∃ 𝑧 ∈ 𝐵 𝑦 ⊆ ( 𝑧 +no 𝐶 ) ∨ ∃ 𝑤 ∈ 𝐶 𝑦 ⊆ ( 𝐵 +no 𝑤 ) ) → ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) ) )
117 16 116 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → ( 𝑦 ∈ ( 𝐵 +no 𝐶 ) → ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) ) )
118 9 117 mpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ) ) → ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) )
119 118 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) )
120 75 110 naddcld ⊢ ( 𝜑 → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) ∈ On )
121 nmulle ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 +no 𝐶 ) ∈ On ∧ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) ∈ On ) → ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) ) )
122 1 10 120 121 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐵 +no 𝐶 ) ( ( 𝑥 ·no ( 𝐵 +no 𝐶 ) ) +no ( 𝐴 ·no 𝑦 ) ) ∈ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) +no ( 𝑥 ·no 𝑦 ) ) ) )
123 119 122 mpbird ⊢ ( 𝜑 → ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) )