Step | Hyp | Ref
| Expression |
1 | | addclpr 6520 |
. . . . 5
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (B
+P 𝐶) ∈
P) |
2 | | df-imp 6452 |
. . . . . 6
⊢
·P = (y
∈ P, z ∈
P ↦ 〈{f ∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(1st ‘y) ∧ ℎ
∈ (1st ‘z) ∧ f = (g
·Q ℎ))}, {f
∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(2nd ‘y) ∧ ℎ
∈ (2nd ‘z) ∧ f = (g
·Q ℎ))}〉) |
3 | | mulclnq 6360 |
. . . . . 6
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g ·Q ℎ) ∈
Q) |
4 | 2, 3 | genpelvl 6495 |
. . . . 5
⊢
((A ∈ P ∧ (B
+P 𝐶) ∈
P) → (w ∈ (1st ‘(A ·P (B +P 𝐶))) ↔ ∃x ∈ (1st ‘A)∃v ∈
(1st ‘(B
+P 𝐶))w =
(x ·Q
v))) |
5 | 1, 4 | sylan2 270 |
. . . 4
⊢
((A ∈ P ∧ (B ∈ P ∧ 𝐶 ∈
P)) → (w ∈ (1st ‘(A ·P (B +P 𝐶))) ↔ ∃x ∈ (1st ‘A)∃v ∈
(1st ‘(B
+P 𝐶))w =
(x ·Q
v))) |
6 | 5 | 3impb 1099 |
. . 3
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (w ∈ (1st ‘(A ·P (B +P 𝐶))) ↔ ∃x ∈ (1st ‘A)∃v ∈
(1st ‘(B
+P 𝐶))w =
(x ·Q
v))) |
7 | | df-iplp 6451 |
. . . . . . . . . . 11
⊢
+P = (w ∈ P, x ∈
P ↦ 〈{f ∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(1st ‘w) ∧ ℎ
∈ (1st ‘x) ∧ f = (g
+Q ℎ))}, {f
∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(2nd ‘w) ∧ ℎ
∈ (2nd ‘x) ∧ f = (g
+Q ℎ))}〉) |
8 | | addclnq 6359 |
. . . . . . . . . . 11
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g +Q ℎ) ∈
Q) |
9 | 7, 8 | genpelvl 6495 |
. . . . . . . . . 10
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (v ∈ (1st ‘(B +P 𝐶)) ↔ ∃y ∈ (1st ‘B)∃z ∈
(1st ‘𝐶)v =
(y +Q z))) |
10 | 9 | 3adant1 921 |
. . . . . . . . 9
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (v ∈ (1st ‘(B +P 𝐶)) ↔ ∃y ∈ (1st ‘B)∃z ∈
(1st ‘𝐶)v =
(y +Q z))) |
11 | 10 | adantr 261 |
. . . . . . . 8
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) → (v
∈ (1st ‘(B +P 𝐶)) ↔ ∃y ∈ (1st ‘B)∃z ∈
(1st ‘𝐶)v =
(y +Q z))) |
12 | | prop 6458 |
. . . . . . . . . . . . . . . . 17
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
13 | | elprnql 6464 |
. . . . . . . . . . . . . . . . 17
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ x ∈ (1st ‘A)) → x
∈ Q) |
14 | 12, 13 | sylan 267 |
. . . . . . . . . . . . . . . 16
⊢
((A ∈ P ∧ x ∈ (1st ‘A)) → x
∈ Q) |
15 | 14 | 3ad2antl1 1065 |
. . . . . . . . . . . . . . 15
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ x ∈
(1st ‘A)) → x ∈
Q) |
16 | 15 | adantrr 448 |
. . . . . . . . . . . . . 14
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) → x
∈ Q) |
17 | 16 | adantr 261 |
. . . . . . . . . . . . 13
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
x ∈
Q) |
18 | | prop 6458 |
. . . . . . . . . . . . . . . . . 18
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
19 | | elprnql 6464 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ y ∈ (1st ‘B)) → y
∈ Q) |
20 | 18, 19 | sylan 267 |
. . . . . . . . . . . . . . . . 17
⊢
((B ∈ P ∧ y ∈ (1st ‘B)) → y
∈ Q) |
21 | | prop 6458 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 ∈ P → 〈(1st
‘𝐶), (2nd
‘𝐶)〉 ∈ P) |
22 | | elprnql 6464 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P ∧ z ∈
(1st ‘𝐶))
→ z ∈ Q) |
23 | 21, 22 | sylan 267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ P ∧ z ∈ (1st ‘𝐶)) → z ∈
Q) |
24 | 20, 23 | anim12i 321 |
. . . . . . . . . . . . . . . 16
⊢
(((B ∈ P ∧ y ∈ (1st ‘B)) ∧ (𝐶 ∈ P ∧ z ∈ (1st ‘𝐶))) → (y ∈
Q ∧ z ∈
Q)) |
25 | 24 | an4s 522 |
. . . . . . . . . . . . . . 15
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ (y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶))) → (y ∈
Q ∧ z ∈
Q)) |
26 | 25 | 3adantl1 1059 |
. . . . . . . . . . . . . 14
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶))) → (y ∈
Q ∧ z ∈
Q)) |
27 | 26 | ad2ant2r 478 |
. . . . . . . . . . . . 13
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
(y ∈
Q ∧ z ∈
Q)) |
28 | | 3anass 888 |
. . . . . . . . . . . . 13
⊢
((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) ↔ (x ∈
Q ∧ (y ∈
Q ∧ z ∈
Q))) |
29 | 17, 27, 28 | sylanbrc 394 |
. . . . . . . . . . . 12
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
(x ∈
Q ∧ y ∈
Q ∧ z ∈
Q)) |
30 | | simprr 484 |
. . . . . . . . . . . . 13
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) → w =
(x ·Q
v)) |
31 | | simpr 103 |
. . . . . . . . . . . . 13
⊢
(((y ∈ (1st ‘B) ∧ z ∈
(1st ‘𝐶))
∧ v =
(y +Q z)) → v =
(y +Q z)) |
32 | 30, 31 | anim12i 321 |
. . . . . . . . . . . 12
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
(w = (x
·Q v) ∧ v = (y +Q z))) |
33 | | oveq2 5463 |
. . . . . . . . . . . . . . 15
⊢ (v = (y
+Q z) →
(x ·Q
v) = (x
·Q (y
+Q z))) |
34 | 33 | eqeq2d 2048 |
. . . . . . . . . . . . . 14
⊢ (v = (y
+Q z) →
(w = (x
·Q v)
↔ w = (x ·Q (y +Q z)))) |
35 | 34 | biimpac 282 |
. . . . . . . . . . . . 13
⊢
((w = (x ·Q v) ∧ v = (y
+Q z)) →
w = (x
·Q (y
+Q z))) |
36 | | distrnqg 6371 |
. . . . . . . . . . . . . 14
⊢
((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (x ·Q (y +Q z)) = ((x
·Q y)
+Q (x
·Q z))) |
37 | 36 | eqeq2d 2048 |
. . . . . . . . . . . . 13
⊢
((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (w = (x
·Q (y
+Q z)) ↔
w = ((x
·Q y)
+Q (x
·Q z)))) |
38 | 35, 37 | syl5ib 143 |
. . . . . . . . . . . 12
⊢
((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → ((w = (x
·Q v) ∧ v = (y +Q z)) → w =
((x ·Q
y) +Q (x ·Q z)))) |
39 | 29, 32, 38 | sylc 56 |
. . . . . . . . . . 11
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
w = ((x
·Q y)
+Q (x
·Q z))) |
40 | | mulclpr 6553 |
. . . . . . . . . . . . . 14
⊢
((A ∈ P ∧ B ∈ P) → (A ·P B) ∈
P) |
41 | 40 | 3adant3 923 |
. . . . . . . . . . . . 13
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (A
·P B) ∈ P) |
42 | 41 | ad2antrr 457 |
. . . . . . . . . . . 12
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
(A ·P
B) ∈
P) |
43 | | mulclpr 6553 |
. . . . . . . . . . . . . 14
⊢
((A ∈ P ∧ 𝐶 ∈
P) → (A
·P 𝐶) ∈
P) |
44 | 43 | 3adant2 922 |
. . . . . . . . . . . . 13
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (A
·P 𝐶) ∈
P) |
45 | 44 | ad2antrr 457 |
. . . . . . . . . . . 12
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
(A ·P 𝐶) ∈ P) |
46 | | simpll 481 |
. . . . . . . . . . . . 13
⊢
(((y ∈ (1st ‘B) ∧ z ∈
(1st ‘𝐶))
∧ v =
(y +Q z)) → y
∈ (1st ‘B)) |
47 | 2, 3 | genpprecll 6497 |
. . . . . . . . . . . . . . . 16
⊢
((A ∈ P ∧ B ∈ P) → ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) → (x
·Q y) ∈ (1st ‘(A ·P B)))) |
48 | 47 | 3adant3 923 |
. . . . . . . . . . . . . . 15
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → ((x ∈ (1st ‘A) ∧ y ∈
(1st ‘B)) → (x ·Q y) ∈
(1st ‘(A
·P B)))) |
49 | 48 | impl 362 |
. . . . . . . . . . . . . 14
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ x ∈
(1st ‘A)) ∧ y ∈ (1st ‘B)) → (x
·Q y) ∈ (1st ‘(A ·P B))) |
50 | 49 | adantlrr 452 |
. . . . . . . . . . . . 13
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ y ∈
(1st ‘B)) → (x ·Q y) ∈
(1st ‘(A
·P B))) |
51 | 46, 50 | sylan2 270 |
. . . . . . . . . . . 12
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
(x ·Q
y) ∈
(1st ‘(A
·P B))) |
52 | | simplr 482 |
. . . . . . . . . . . . 13
⊢
(((y ∈ (1st ‘B) ∧ z ∈
(1st ‘𝐶))
∧ v =
(y +Q z)) → z
∈ (1st ‘𝐶)) |
53 | 2, 3 | genpprecll 6497 |
. . . . . . . . . . . . . . . 16
⊢
((A ∈ P ∧ 𝐶 ∈
P) → ((x ∈ (1st ‘A) ∧ z ∈
(1st ‘𝐶))
→ (x
·Q z) ∈ (1st ‘(A ·P 𝐶)))) |
54 | 53 | 3adant2 922 |
. . . . . . . . . . . . . . 15
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → ((x ∈ (1st ‘A) ∧ z ∈
(1st ‘𝐶))
→ (x
·Q z) ∈ (1st ‘(A ·P 𝐶)))) |
55 | 54 | impl 362 |
. . . . . . . . . . . . . 14
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ x ∈
(1st ‘A)) ∧ z ∈ (1st ‘𝐶)) → (x ·Q z) ∈
(1st ‘(A
·P 𝐶))) |
56 | 55 | adantlrr 452 |
. . . . . . . . . . . . 13
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ z ∈
(1st ‘𝐶))
→ (x
·Q z) ∈ (1st ‘(A ·P 𝐶))) |
57 | 52, 56 | sylan2 270 |
. . . . . . . . . . . 12
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
(x ·Q
z) ∈
(1st ‘(A
·P 𝐶))) |
58 | 7, 8 | genpprecll 6497 |
. . . . . . . . . . . . 13
⊢
(((A
·P B) ∈ P ∧ (A
·P 𝐶) ∈
P) → (((x
·Q y) ∈ (1st ‘(A ·P B)) ∧ (x ·Q z) ∈
(1st ‘(A
·P 𝐶))) → ((x ·Q y) +Q (x ·Q z)) ∈
(1st ‘((A
·P B)
+P (A
·P 𝐶))))) |
59 | 58 | imp 115 |
. . . . . . . . . . . 12
⊢
((((A
·P B) ∈ P ∧ (A
·P 𝐶) ∈
P) ∧ ((x ·Q y) ∈
(1st ‘(A
·P B))
∧ (x
·Q z) ∈ (1st ‘(A ·P 𝐶)))) → ((x ·Q y) +Q (x ·Q z)) ∈
(1st ‘((A
·P B)
+P (A
·P 𝐶)))) |
60 | 42, 45, 51, 57, 59 | syl22anc 1135 |
. . . . . . . . . . 11
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
((x ·Q
y) +Q (x ·Q z)) ∈
(1st ‘((A
·P B)
+P (A
·P 𝐶)))) |
61 | 39, 60 | eqeltrd 2111 |
. . . . . . . . . 10
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) ∧ ((y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶)) ∧
v = (y
+Q z))) →
w ∈
(1st ‘((A
·P B)
+P (A
·P 𝐶)))) |
62 | 61 | exp32 347 |
. . . . . . . . 9
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) → ((y
∈ (1st ‘B) ∧ z ∈
(1st ‘𝐶))
→ (v = (y +Q z) → w
∈ (1st ‘((A ·P B) +P (A ·P 𝐶)))))) |
63 | 62 | rexlimdvv 2433 |
. . . . . . . 8
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) → (∃y ∈ (1st ‘B)∃z ∈
(1st ‘𝐶)v =
(y +Q z) → w
∈ (1st ‘((A ·P B) +P (A ·P 𝐶))))) |
64 | 11, 63 | sylbid 139 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (x ∈
(1st ‘A) ∧ w = (x ·Q v))) → (v
∈ (1st ‘(B +P 𝐶)) → w ∈
(1st ‘((A
·P B)
+P (A
·P 𝐶))))) |
65 | 64 | exp32 347 |
. . . . . 6
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (x ∈ (1st ‘A) → (w =
(x ·Q
v) → (v ∈
(1st ‘(B
+P 𝐶)) → w ∈
(1st ‘((A
·P B)
+P (A
·P 𝐶))))))) |
66 | 65 | com34 77 |
. . . . 5
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (x ∈ (1st ‘A) → (v
∈ (1st ‘(B +P 𝐶)) → (w = (x
·Q v)
→ w ∈ (1st ‘((A ·P B) +P (A ·P 𝐶))))))) |
67 | 66 | impd 242 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → ((x ∈ (1st ‘A) ∧ v ∈
(1st ‘(B
+P 𝐶))) → (w = (x
·Q v)
→ w ∈ (1st ‘((A ·P B) +P (A ·P 𝐶)))))) |
68 | 67 | rexlimdvv 2433 |
. . 3
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (∃x ∈
(1st ‘A)∃v ∈ (1st ‘(B +P 𝐶))w =
(x ·Q
v) → w ∈
(1st ‘((A
·P B)
+P (A
·P 𝐶))))) |
69 | 6, 68 | sylbid 139 |
. 2
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (w ∈ (1st ‘(A ·P (B +P 𝐶))) → w ∈
(1st ‘((A
·P B)
+P (A
·P 𝐶))))) |
70 | 69 | ssrdv 2945 |
1
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (1st ‘(A ·P (B +P 𝐶))) ⊆ (1st
‘((A
·P B)
+P (A
·P 𝐶)))) |