distrlem4prl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > distrlem4prl		GIF version

Theorem distrlem4prl 6560

Description: Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)

**Assertion**
Ref	Expression
distrlem4prl	⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))

Distinct variable groups: x,y,z,f,A x,B,y,z,f x,𝐶,y,z,f

Proof of Theorem distrlem4prl Dummy variables w v u g ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltmnqg 6385	. . . . . . 7 ⊢ ((w ∈ Q ∧ v ∈ Q ∧ u ∈ Q) → (w <_Q v ↔ (u ·_Q w) <_Q (u ·_Q v)))
2	1	adantl 262	. . . . . 6 ⊢ ((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) ∧ (w ∈ Q ∧ v ∈ Q ∧ u ∈ Q)) → (w <_Q v ↔ (u ·_Q w) <_Q (u ·_Q v)))
3		simp1 903	. . . . . . 7 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → A ∈ P)
4		simpll 481	. . . . . . 7 ⊢ (((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶))) → x ∈ (1^st ‘A))
5		prop 6458	. . . . . . . 8 ⊢ (A ∈ P → ⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P)
6		elprnql 6464	. . . . . . . 8 ⊢ ((⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P ∧ x ∈ (1^st ‘A)) → x ∈ Q)
7	5, 6	sylan 267	. . . . . . 7 ⊢ ((A ∈ P ∧ x ∈ (1^st ‘A)) → x ∈ Q)
8	3, 4, 7	syl2an 273	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → x ∈ Q)
9		simprl 483	. . . . . . 7 ⊢ (((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶))) → f ∈ (1^st ‘A))
10		elprnql 6464	. . . . . . . 8 ⊢ ((⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P ∧ f ∈ (1^st ‘A)) → f ∈ Q)
11	5, 10	sylan 267	. . . . . . 7 ⊢ ((A ∈ P ∧ f ∈ (1^st ‘A)) → f ∈ Q)
12	3, 9, 11	syl2an 273	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → f ∈ Q)
13		simpl2 907	. . . . . . 7 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → B ∈ P)
14		simprlr 490	. . . . . . 7 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → y ∈ (1^st ‘B))
15		prop 6458	. . . . . . . 8 ⊢ (B ∈ P → ⟨(1^st ‘B), (2^nd ‘B)⟩ ∈ P)
16		elprnql 6464	. . . . . . . 8 ⊢ ((⟨(1^st ‘B), (2^nd ‘B)⟩ ∈ P ∧ y ∈ (1^st ‘B)) → y ∈ Q)
17	15, 16	sylan 267	. . . . . . 7 ⊢ ((B ∈ P ∧ y ∈ (1^st ‘B)) → y ∈ Q)
18	13, 14, 17	syl2anc 391	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → y ∈ Q)
19		mulcomnqg 6367	. . . . . . 7 ⊢ ((w ∈ Q ∧ v ∈ Q) → (w ·_Q v) = (v ·_Q w))
20	19	adantl 262	. . . . . 6 ⊢ ((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) ∧ (w ∈ Q ∧ v ∈ Q)) → (w ·_Q v) = (v ·_Q w))
21	2, 8, 12, 18, 20	caovord2d 5612	. . . . 5 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x <_Q f ↔ (x ·_Q y) <_Q (f ·_Q y)))
22		ltanqg 6384	. . . . . . 7 ⊢ ((w ∈ Q ∧ v ∈ Q ∧ u ∈ Q) → (w <_Q v ↔ (u +_Q w) <_Q (u +_Q v)))
23	22	adantl 262	. . . . . 6 ⊢ ((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) ∧ (w ∈ Q ∧ v ∈ Q ∧ u ∈ Q)) → (w <_Q v ↔ (u +_Q w) <_Q (u +_Q v)))
24		mulclnq 6360	. . . . . . 7 ⊢ ((x ∈ Q ∧ y ∈ Q) → (x ·_Q y) ∈ Q)
25	8, 18, 24	syl2anc 391	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x ·_Q y) ∈ Q)
26		mulclnq 6360	. . . . . . 7 ⊢ ((f ∈ Q ∧ y ∈ Q) → (f ·_Q y) ∈ Q)
27	12, 18, 26	syl2anc 391	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (f ·_Q y) ∈ Q)
28		simpl3 908	. . . . . . . 8 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → 𝐶 ∈ P)
29		simprrr 492	. . . . . . . 8 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → z ∈ (1^st ‘𝐶))
30		prop 6458	. . . . . . . . 9 ⊢ (𝐶 ∈ P → ⟨(1^st ‘𝐶), (2^nd ‘𝐶)⟩ ∈ P)
31		elprnql 6464	. . . . . . . . 9 ⊢ ((⟨(1^st ‘𝐶), (2^nd ‘𝐶)⟩ ∈ P ∧ z ∈ (1^st ‘𝐶)) → z ∈ Q)
32	30, 31	sylan 267	. . . . . . . 8 ⊢ ((𝐶 ∈ P ∧ z ∈ (1^st ‘𝐶)) → z ∈ Q)
33	28, 29, 32	syl2anc 391	. . . . . . 7 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → z ∈ Q)
34		mulclnq 6360	. . . . . . 7 ⊢ ((f ∈ Q ∧ z ∈ Q) → (f ·_Q z) ∈ Q)
35	12, 33, 34	syl2anc 391	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (f ·_Q z) ∈ Q)
36		addcomnqg 6365	. . . . . . 7 ⊢ ((w ∈ Q ∧ v ∈ Q) → (w +_Q v) = (v +_Q w))
37	36	adantl 262	. . . . . 6 ⊢ ((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) ∧ (w ∈ Q ∧ v ∈ Q)) → (w +_Q v) = (v +_Q w))
38	23, 25, 27, 35, 37	caovord2d 5612	. . . . 5 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → ((x ·_Q y) <_Q (f ·_Q y) ↔ ((x ·_Q y) +_Q (f ·_Q z)) <_Q ((f ·_Q y) +_Q (f ·_Q z))))
39	21, 38	bitrd 177	. . . 4 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x <_Q f ↔ ((x ·_Q y) +_Q (f ·_Q z)) <_Q ((f ·_Q y) +_Q (f ·_Q z))))
40		simpl1 906	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → A ∈ P)
41		addclpr 6520	. . . . . . . 8 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → (B +_P 𝐶) ∈ P)
42	41	3adant1 921	. . . . . . 7 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (B +_P 𝐶) ∈ P)
43	42	adantr 261	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (B +_P 𝐶) ∈ P)
44		mulclpr 6553	. . . . . 6 ⊢ ((A ∈ P ∧ (B +_P 𝐶) ∈ P) → (A ·_P (B +_P 𝐶)) ∈ P)
45	40, 43, 44	syl2anc 391	. . . . 5 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (A ·_P (B +_P 𝐶)) ∈ P)
46		distrnqg 6371	. . . . . . 7 ⊢ ((f ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (f ·_Q (y +_Q z)) = ((f ·_Q y) +_Q (f ·_Q z)))
47	12, 18, 33, 46	syl3anc 1134	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (f ·_Q (y +_Q z)) = ((f ·_Q y) +_Q (f ·_Q z)))
48		simprrl 491	. . . . . . 7 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → f ∈ (1^st ‘A))
49		df-iplp 6451	. . . . . . . . . 10 ⊢ +_P = (u ∈ P, v ∈ P ↦ ⟨{w ∈ Q ∣ ∃g ∈ Q ∃ℎ ∈ Q (g ∈ (1^st ‘u) ∧ ℎ ∈ (1^st ‘v) ∧ w = (g +_Q ℎ))}, {w ∈ Q ∣ ∃g ∈ Q ∃ℎ ∈ Q (g ∈ (2^nd ‘u) ∧ ℎ ∈ (2^nd ‘v) ∧ w = (g +_Q ℎ))}⟩)
50		addclnq 6359	. . . . . . . . . 10 ⊢ ((g ∈ Q ∧ ℎ ∈ Q) → (g +_Q ℎ) ∈ Q)
51	49, 50	genpprecll 6497	. . . . . . . . 9 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → ((y ∈ (1^st ‘B) ∧ z ∈ (1^st ‘𝐶)) → (y +_Q z) ∈ (1^st ‘(B +_P 𝐶))))
52	51	imp 115	. . . . . . . 8 ⊢ (((B ∈ P ∧ 𝐶 ∈ P) ∧ (y ∈ (1^st ‘B) ∧ z ∈ (1^st ‘𝐶))) → (y +_Q z) ∈ (1^st ‘(B +_P 𝐶)))
53	13, 28, 14, 29, 52	syl22anc 1135	. . . . . . 7 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (y +_Q z) ∈ (1^st ‘(B +_P 𝐶)))
54		df-imp 6452	. . . . . . . . 9 ⊢ ·_P = (u ∈ P, v ∈ P ↦ ⟨{w ∈ Q ∣ ∃g ∈ Q ∃ℎ ∈ Q (g ∈ (1^st ‘u) ∧ ℎ ∈ (1^st ‘v) ∧ w = (g ·_Q ℎ))}, {w ∈ Q ∣ ∃g ∈ Q ∃ℎ ∈ Q (g ∈ (2^nd ‘u) ∧ ℎ ∈ (2^nd ‘v) ∧ w = (g ·_Q ℎ))}⟩)
55		mulclnq 6360	. . . . . . . . 9 ⊢ ((g ∈ Q ∧ ℎ ∈ Q) → (g ·_Q ℎ) ∈ Q)
56	54, 55	genpprecll 6497	. . . . . . . 8 ⊢ ((A ∈ P ∧ (B +_P 𝐶) ∈ P) → ((f ∈ (1^st ‘A) ∧ (y +_Q z) ∈ (1^st ‘(B +_P 𝐶))) → (f ·_Q (y +_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
57	56	imp 115	. . . . . . 7 ⊢ (((A ∈ P ∧ (B +_P 𝐶) ∈ P) ∧ (f ∈ (1^st ‘A) ∧ (y +_Q z) ∈ (1^st ‘(B +_P 𝐶)))) → (f ·_Q (y +_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))
58	40, 43, 48, 53, 57	syl22anc 1135	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (f ·_Q (y +_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))
59	47, 58	eqeltrrd 2112	. . . . 5 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → ((f ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))
60		prop 6458	. . . . . 6 ⊢ ((A ·_P (B +_P 𝐶)) ∈ P → ⟨(1^st ‘(A ·_P (B +_P 𝐶))), (2^nd ‘(A ·_P (B +_P 𝐶)))⟩ ∈ P)
61		prcdnql 6467	. . . . . 6 ⊢ ((⟨(1^st ‘(A ·_P (B +_P 𝐶))), (2^nd ‘(A ·_P (B +_P 𝐶)))⟩ ∈ P ∧ ((f ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))) → (((x ·_Q y) +_Q (f ·_Q z)) <_Q ((f ·_Q y) +_Q (f ·_Q z)) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
62	60, 61	sylan 267	. . . . 5 ⊢ (((A ·_P (B +_P 𝐶)) ∈ P ∧ ((f ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))) → (((x ·_Q y) +_Q (f ·_Q z)) <_Q ((f ·_Q y) +_Q (f ·_Q z)) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
63	45, 59, 62	syl2anc 391	. . . 4 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (((x ·_Q y) +_Q (f ·_Q z)) <_Q ((f ·_Q y) +_Q (f ·_Q z)) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
64	39, 63	sylbid 139	. . 3 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x <_Q f → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
65	2, 12, 8, 33, 20	caovord2d 5612	. . . . 5 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (f <_Q x ↔ (f ·_Q z) <_Q (x ·_Q z)))
66		mulclnq 6360	. . . . . . 7 ⊢ ((x ∈ Q ∧ z ∈ Q) → (x ·_Q z) ∈ Q)
67	8, 33, 66	syl2anc 391	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x ·_Q z) ∈ Q)
68		ltanqg 6384	. . . . . 6 ⊢ (((f ·_Q z) ∈ Q ∧ (x ·_Q z) ∈ Q ∧ (x ·_Q y) ∈ Q) → ((f ·_Q z) <_Q (x ·_Q z) ↔ ((x ·_Q y) +_Q (f ·_Q z)) <_Q ((x ·_Q y) +_Q (x ·_Q z))))
69	35, 67, 25, 68	syl3anc 1134	. . . . 5 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → ((f ·_Q z) <_Q (x ·_Q z) ↔ ((x ·_Q y) +_Q (f ·_Q z)) <_Q ((x ·_Q y) +_Q (x ·_Q z))))
70	65, 69	bitrd 177	. . . 4 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (f <_Q x ↔ ((x ·_Q y) +_Q (f ·_Q z)) <_Q ((x ·_Q y) +_Q (x ·_Q z))))
71		distrnqg 6371	. . . . . . 7 ⊢ ((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (x ·_Q (y +_Q z)) = ((x ·_Q y) +_Q (x ·_Q z)))
72	8, 18, 33, 71	syl3anc 1134	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x ·_Q (y +_Q z)) = ((x ·_Q y) +_Q (x ·_Q z)))
73		simprll 489	. . . . . . 7 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → x ∈ (1^st ‘A))
74	54, 55	genpprecll 6497	. . . . . . . 8 ⊢ ((A ∈ P ∧ (B +_P 𝐶) ∈ P) → ((x ∈ (1^st ‘A) ∧ (y +_Q z) ∈ (1^st ‘(B +_P 𝐶))) → (x ·_Q (y +_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
75	74	imp 115	. . . . . . 7 ⊢ (((A ∈ P ∧ (B +_P 𝐶) ∈ P) ∧ (x ∈ (1^st ‘A) ∧ (y +_Q z) ∈ (1^st ‘(B +_P 𝐶)))) → (x ·_Q (y +_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))
76	40, 43, 73, 53, 75	syl22anc 1135	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x ·_Q (y +_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))
77	72, 76	eqeltrrd 2112	. . . . 5 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → ((x ·_Q y) +_Q (x ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))
78		prcdnql 6467	. . . . . 6 ⊢ ((⟨(1^st ‘(A ·_P (B +_P 𝐶))), (2^nd ‘(A ·_P (B +_P 𝐶)))⟩ ∈ P ∧ ((x ·_Q y) +_Q (x ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))) → (((x ·_Q y) +_Q (f ·_Q z)) <_Q ((x ·_Q y) +_Q (x ·_Q z)) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
79	60, 78	sylan 267	. . . . 5 ⊢ (((A ·_P (B +_P 𝐶)) ∈ P ∧ ((x ·_Q y) +_Q (x ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))) → (((x ·_Q y) +_Q (f ·_Q z)) <_Q ((x ·_Q y) +_Q (x ·_Q z)) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
80	45, 77, 79	syl2anc 391	. . . 4 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (((x ·_Q y) +_Q (f ·_Q z)) <_Q ((x ·_Q y) +_Q (x ·_Q z)) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
81	70, 80	sylbid 139	. . 3 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (f <_Q x → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
82	64, 81	jaod 636	. 2 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → ((x <_Q f ∨ f <_Q x) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
83		ltsonq 6382	. . . . 5 ⊢ <_Q Or Q
84		nqtri3or 6380	. . . . 5 ⊢ ((x ∈ Q ∧ f ∈ Q) → (x <_Q f ∨ x = f ∨ f <_Q x))
85	83, 84	sotritrieq 4053	. . . 4 ⊢ ((x ∈ Q ∧ f ∈ Q) → (x = f ↔ ¬ (x <_Q f ∨ f <_Q x)))
86	8, 12, 85	syl2anc 391	. . 3 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x = f ↔ ¬ (x <_Q f ∨ f <_Q x)))
87		oveq1 5462	. . . . . . 7 ⊢ (x = f → (x ·_Q z) = (f ·_Q z))
88	87	oveq2d 5471	. . . . . 6 ⊢ (x = f → ((x ·_Q y) +_Q (x ·_Q z)) = ((x ·_Q y) +_Q (f ·_Q z)))
89	72, 88	sylan9eq 2089	. . . . 5 ⊢ ((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) ∧ x = f) → (x ·_Q (y +_Q z)) = ((x ·_Q y) +_Q (f ·_Q z)))
90	76	adantr 261	. . . . 5 ⊢ ((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) ∧ x = f) → (x ·_Q (y +_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))
91	89, 90	eqeltrrd 2112	. . . 4 ⊢ ((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) ∧ x = f) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))
92	91	ex 108	. . 3 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (x = f → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
93	86, 92	sylbird 159	. 2 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → (¬ (x <_Q f ∨ f <_Q x) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶)))))
94		ltdcnq 6381	. . . . 5 ⊢ ((x ∈ Q ∧ f ∈ Q) → DECID x <_Q f)
95		ltdcnq 6381	. . . . . 6 ⊢ ((f ∈ Q ∧ x ∈ Q) → DECID f <_Q x)
96	95	ancoms 255	. . . . 5 ⊢ ((x ∈ Q ∧ f ∈ Q) → DECID f <_Q x)
97		dcor 842	. . . . 5 ⊢ (DECID x <_Q f → (DECID f <_Q x → DECID (x <_Q f ∨ f <_Q x)))
98	94, 96, 97	sylc 56	. . . 4 ⊢ ((x ∈ Q ∧ f ∈ Q) → DECID (x <_Q f ∨ f <_Q x))
99	8, 12, 98	syl2anc 391	. . 3 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → DECID (x <_Q f ∨ f <_Q x))
100		df-dc 742	. . 3 ⊢ (DECID (x <_Q f ∨ f <_Q x) ↔ ((x <_Q f ∨ f <_Q x) ∨ ¬ (x <_Q f ∨ f <_Q x)))
101	99, 100	sylib 127	. 2 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → ((x <_Q f ∨ f <_Q x) ∨ ¬ (x <_Q f ∨ f <_Q x)))
102	82, 93, 101	mpjaod 637	1 ⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1^st ‘A) ∧ y ∈ (1^st ‘B)) ∧ (f ∈ (1^st ‘A) ∧ z ∈ (1^st ‘𝐶)))) → ((x ·_Q y) +_Q (f ·_Q z)) ∈ (1^st ‘(A ·_P (B +_P 𝐶))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 97 ↔ wb 98 ∨ wo 628 DECID wdc 741 ∧ w3a 884 = wceq 1242 ∈ wcel 1390 ⟨cop 3370 class class class wbr 3755 ‘cfv 4845 (class class class)co 5455 1^st c1st 5707 2^nd c2nd 5708 Qcnq 6264 +_Q cplq 6266 ·_Q cmq 6267 <_Q cltq 6269 Pcnp 6275 +_P cpp 6277 ·_P cmp 6278

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-13 1401 ax-14 1402 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-coll 3863 ax-sep 3866 ax-nul 3874 ax-pow 3918 ax-pr 3935 ax-un 4136 ax-setind 4220 ax-iinf 4254

This theorem depends on definitions: df-bi 110 df-dc 742 df-3or 885 df-3an 886 df-tru 1245 df-fal 1248 df-nf 1347 df-sb 1643 df-eu 1900 df-mo 1901 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ne 2203 df-ral 2305 df-rex 2306 df-reu 2307 df-rab 2309 df-v 2553 df-sbc 2759 df-csb 2847 df-dif 2914 df-un 2916 df-in 2918 df-ss 2925 df-nul 3219 df-pw 3353 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-int 3607 df-iun 3650 df-br 3756 df-opab 3810 df-mpt 3811 df-tr 3846 df-eprel 4017 df-id 4021 df-po 4024 df-iso 4025 df-iord 4069 df-on 4071 df-suc 4074 df-iom 4257 df-xp 4294 df-rel 4295 df-cnv 4296 df-co 4297 df-dm 4298 df-rn 4299 df-res 4300 df-ima 4301 df-iota 4810 df-fun 4847 df-fn 4848 df-f 4849 df-f1 4850 df-fo 4851 df-f1o 4852 df-fv 4853 df-ov 5458 df-oprab 5459 df-mpt2 5460 df-1st 5709 df-2nd 5710 df-recs 5861 df-irdg 5897 df-1o 5940 df-2o 5941 df-oadd 5944 df-omul 5945 df-er 6042 df-ec 6044 df-qs 6048 df-ni 6288 df-pli 6289 df-mi 6290 df-lti 6291 df-plpq 6328 df-mpq 6329 df-enq 6331 df-nqqs 6332 df-plqqs 6333 df-mqqs 6334 df-1nqqs 6335 df-rq 6336 df-ltnqqs 6337 df-enq0 6407 df-nq0 6408 df-0nq0 6409 df-plq0 6410 df-mq0 6411 df-inp 6449 df-iplp 6451 df-imp 6452

This theorem is referenced by: distrlem5prl 6562

W3C validator