Theorem nadddilem2

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

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

Proof

Step	Hyp	Ref	Expression
1		nadddilem2.1	⊢ ( 𝜑 → 𝐴 ∈ On )
2		nadddilem2.2	⊢ ( 𝜑 → 𝐵 ∈ On )
3		nadddilem2.3	⊢ ( 𝜑 → 𝐶 ∈ On )
4		nadddilem2.4	⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) )
5		nadddilem2.5	⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝐵 ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) )
6		nadddilem2.6	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐶 ( 𝐴 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝑓 ) ) )
7		nadddilem2.7	⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐵 ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) )
8		nadddilem2.8	⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐴 ∀ 𝑓 ∈ 𝐶 ( 𝑑 ·no ( 𝐵 +no 𝑓 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝑓 ) ) )
9		oveq1	⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) )
10		oveq1	⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no 𝐵 ) = ( 𝑝 ·no 𝐵 ) )
11		oveq1	⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no 𝐶 ) = ( 𝑝 ·no 𝐶 ) )
12	10 11	oveq12d	⊢ ( 𝑑 = 𝑝 → ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) )
13	9 12	eqeq12d	⊢ ( 𝑑 = 𝑝 → ( ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) ) )
14	13	cbvralvw	⊢ ( ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) )
15	2 3	naddcomd	⊢ ( 𝜑 → ( 𝐵 +no 𝐶 ) = ( 𝐶 +no 𝐵 ) )
16	15	oveq2d	⊢ ( 𝜑 → ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) )
18	1	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝐴 ∈ On )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
20	18 19	onelond	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ On )
21	2	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝐵 ∈ On )
22	20 21	nmulcld	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ·no 𝐵 ) ∈ On )
23	3	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝐶 ∈ On )
24	20 23	nmulcld	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ·no 𝐶 ) ∈ On )
25	22 24	naddcomd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) )
26	17 25	eqeq12d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) ↔ ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
27	26	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝐵 ) +no ( 𝑝 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
28	14 27	bitrid	⊢ ( 𝜑 → ( ∀ 𝑑 ∈ 𝐴 ( 𝑑 ·no ( 𝐵 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝐵 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) ) )
29	4 28	mpbid	⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ·no ( 𝐶 +no 𝐵 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝐵 ) ) )
30		oveq1	⊢ ( 𝑒 = 𝑞 → ( 𝑒 +no 𝐶 ) = ( 𝑞 +no 𝐶 ) )
31	30	oveq2d	⊢ ( 𝑒 = 𝑞 → ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( 𝐴 ·no ( 𝑞 +no 𝐶 ) ) )
32		oveq2	⊢ ( 𝑒 = 𝑞 → ( 𝐴 ·no 𝑒 ) = ( 𝐴 ·no 𝑞 ) )
33	32	oveq1d	⊢ ( 𝑒 = 𝑞 → ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐶 ) ) )
34	31 33	eqeq12d	⊢ ( 𝑒 = 𝑞 → ( ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) ↔ ( 𝐴 ·no ( 𝑞 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐶 ) ) ) )
35	34	cbvralvw	⊢ ( ∀ 𝑒 ∈ 𝐵 ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) ↔ ∀ 𝑞 ∈ 𝐵 ( 𝐴 ·no ( 𝑞 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐶 ) ) )
36	2	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝐵 ∈ On )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝑞 ∈ 𝐵 )
38	36 37	onelond	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝑞 ∈ On )
39	3	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝐶 ∈ On )
40	38 39	naddcomd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑞 +no 𝐶 ) = ( 𝐶 +no 𝑞 ) )
41	40	oveq2d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐴 ·no ( 𝑞 +no 𝐶 ) ) = ( 𝐴 ·no ( 𝐶 +no 𝑞 ) ) )
42	1	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝐴 ∈ On )
43	42 38	nmulcld	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐴 ·no 𝑞 ) ∈ On )
44	42 39	nmulcld	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐴 ·no 𝐶 ) ∈ On )
45	43 44	naddcomd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐶 ) ) = ( ( 𝐴 ·no 𝐶 ) +no ( 𝐴 ·no 𝑞 ) ) )
46	41 45	eqeq12d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐴 ·no ( 𝑞 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐶 ) ) ↔ ( 𝐴 ·no ( 𝐶 +no 𝑞 ) ) = ( ( 𝐴 ·no 𝐶 ) +no ( 𝐴 ·no 𝑞 ) ) ) )
47	46	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑞 ∈ 𝐵 ( 𝐴 ·no ( 𝑞 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑞 ) +no ( 𝐴 ·no 𝐶 ) ) ↔ ∀ 𝑞 ∈ 𝐵 ( 𝐴 ·no ( 𝐶 +no 𝑞 ) ) = ( ( 𝐴 ·no 𝐶 ) +no ( 𝐴 ·no 𝑞 ) ) ) )
48	35 47	bitrid	⊢ ( 𝜑 → ( ∀ 𝑒 ∈ 𝐵 ( 𝐴 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝐴 ·no 𝑒 ) +no ( 𝐴 ·no 𝐶 ) ) ↔ ∀ 𝑞 ∈ 𝐵 ( 𝐴 ·no ( 𝐶 +no 𝑞 ) ) = ( ( 𝐴 ·no 𝐶 ) +no ( 𝐴 ·no 𝑞 ) ) ) )
49	5 48	mpbid	⊢ ( 𝜑 → ∀ 𝑞 ∈ 𝐵 ( 𝐴 ·no ( 𝐶 +no 𝑞 ) ) = ( ( 𝐴 ·no 𝐶 ) +no ( 𝐴 ·no 𝑞 ) ) )
50		oveq1	⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( 𝑝 ·no ( 𝑒 +no 𝐶 ) ) )
51		oveq1	⊢ ( 𝑑 = 𝑝 → ( 𝑑 ·no 𝑒 ) = ( 𝑝 ·no 𝑒 ) )
52	51 11	oveq12d	⊢ ( 𝑑 = 𝑝 → ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) = ( ( 𝑝 ·no 𝑒 ) +no ( 𝑝 ·no 𝐶 ) ) )
53	50 52	eqeq12d	⊢ ( 𝑑 = 𝑝 → ( ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ( 𝑝 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝑒 ) +no ( 𝑝 ·no 𝐶 ) ) ) )
54	30	oveq2d	⊢ ( 𝑒 = 𝑞 → ( 𝑝 ·no ( 𝑒 +no 𝐶 ) ) = ( 𝑝 ·no ( 𝑞 +no 𝐶 ) ) )
55		oveq2	⊢ ( 𝑒 = 𝑞 → ( 𝑝 ·no 𝑒 ) = ( 𝑝 ·no 𝑞 ) )
56	55	oveq1d	⊢ ( 𝑒 = 𝑞 → ( ( 𝑝 ·no 𝑒 ) +no ( 𝑝 ·no 𝐶 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐶 ) ) )
57	54 56	eqeq12d	⊢ ( 𝑒 = 𝑞 → ( ( 𝑝 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝑒 ) +no ( 𝑝 ·no 𝐶 ) ) ↔ ( 𝑝 ·no ( 𝑞 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐶 ) ) ) )
58	53 57	cbvral2vw	⊢ ( ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐵 ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐵 ( 𝑝 ·no ( 𝑞 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐶 ) ) )
59	40	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑞 +no 𝐶 ) = ( 𝐶 +no 𝑞 ) )
60	59	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ·no ( 𝑞 +no 𝐶 ) ) = ( 𝑝 ·no ( 𝐶 +no 𝑞 ) ) )
61	20	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → 𝑝 ∈ On )
62	38	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → 𝑞 ∈ On )
63	61 62	nmulcld	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ·no 𝑞 ) ∈ On )
64	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → 𝐶 ∈ On )
65	61 64	nmulcld	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ·no 𝐶 ) ∈ On )
66	63 65	naddcomd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐶 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝑞 ) ) )
67	60 66	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( 𝑝 ·no ( 𝑞 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐶 ) ) ↔ ( 𝑝 ·no ( 𝐶 +no 𝑞 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝑞 ) ) ) )
68	67	2ralbidva	⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐵 ( 𝑝 ·no ( 𝑞 +no 𝐶 ) ) = ( ( 𝑝 ·no 𝑞 ) +no ( 𝑝 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐵 ( 𝑝 ·no ( 𝐶 +no 𝑞 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝑞 ) ) ) )
69	58 68	bitrid	⊢ ( 𝜑 → ( ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐵 ( 𝑑 ·no ( 𝑒 +no 𝐶 ) ) = ( ( 𝑑 ·no 𝑒 ) +no ( 𝑑 ·no 𝐶 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐵 ( 𝑝 ·no ( 𝐶 +no 𝑞 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝑞 ) ) ) )
70	7 69	mpbid	⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐵 ( 𝑝 ·no ( 𝐶 +no 𝑞 ) ) = ( ( 𝑝 ·no 𝐶 ) +no ( 𝑝 ·no 𝑞 ) ) )
71	1 3 2 29 49 70	nadddilem1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ) → ( ( 𝐴 ·no 𝐶 ) +no 𝑥 ) ∈ ( 𝐴 ·no ( 𝐶 +no 𝐵 ) ) )
72	1 2	nmulcld	⊢ ( 𝜑 → ( 𝐴 ·no 𝐵 ) ∈ On )
73	72	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ) → ( 𝐴 ·no 𝐵 ) ∈ On )
74		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ) → 𝑥 ∈ ( 𝐴 ·no 𝐵 ) )
75	73 74	onelond	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ) → 𝑥 ∈ On )
76	1 3	nmulcld	⊢ ( 𝜑 → ( 𝐴 ·no 𝐶 ) ∈ On )
77	76	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ) → ( 𝐴 ·no 𝐶 ) ∈ On )
78	75 77	naddcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ) → ( 𝑥 +no ( 𝐴 ·no 𝐶 ) ) = ( ( 𝐴 ·no 𝐶 ) +no 𝑥 ) )
79	15	oveq2d	⊢ ( 𝜑 → ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝐴 ·no ( 𝐶 +no 𝐵 ) ) )
80	79	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ) → ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) = ( 𝐴 ·no ( 𝐶 +no 𝐵 ) ) )
81	71 78 80	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ) → ( 𝑥 +no ( 𝐴 ·no 𝐶 ) ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) )
82	81	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ( 𝑥 +no ( 𝐴 ·no 𝐶 ) ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) )
83	1 2 3 4 6 8	nadddilem1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ·no 𝐶 ) ) → ( ( 𝐴 ·no 𝐵 ) +no 𝑦 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) )
84	83	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 ·no 𝐶 ) ( ( 𝐴 ·no 𝐵 ) +no 𝑦 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) )
85	2 3	naddcld	⊢ ( 𝜑 → ( 𝐵 +no 𝐶 ) ∈ On )
86	1 85	nmulcld	⊢ ( 𝜑 → ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ∈ On )
87		naddle	⊢ ( ( ( 𝐴 ·no 𝐵 ) ∈ On ∧ ( 𝐴 ·no 𝐶 ) ∈ On ∧ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ∈ On ) → ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) ⊆ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ↔ ( ∀ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ( 𝑥 +no ( 𝐴 ·no 𝐶 ) ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 ·no 𝐶 ) ( ( 𝐴 ·no 𝐵 ) +no 𝑦 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ) ) )
88	72 76 86 87	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) ⊆ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ↔ ( ∀ 𝑥 ∈ ( 𝐴 ·no 𝐵 ) ( 𝑥 +no ( 𝐴 ·no 𝐶 ) ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 ·no 𝐶 ) ( ( 𝐴 ·no 𝐵 ) +no 𝑦 ) ∈ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) ) ) )
89	82 84 88	mpbir2and	⊢ ( 𝜑 → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐶 ) ) ⊆ ( 𝐴 ·no ( 𝐵 +no 𝐶 ) ) )