Proof of Theorem mulsunif2lem
| Step | Hyp | Ref
| Expression |
| 1 | | mulsunif2.1 |
. . 3
⊢ (𝜑 → 𝐿 <<s 𝑅) |
| 2 | | mulsunif2.2 |
. . 3
⊢ (𝜑 → 𝑀 <<s 𝑆) |
| 3 | | mulsunif2.3 |
. . 3
⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) |
| 4 | | mulsunif2.4 |
. . 3
⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆)) |
| 5 | 1, 2, 3, 4 | mulsunif 28176 |
. 2
⊢ (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
| 6 | 1 | scutcld 27848 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 |s 𝑅) ∈ No
) |
| 7 | 3, 6 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ No
) |
| 8 | 2 | scutcld 27848 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 |s 𝑆) ∈ No
) |
| 9 | 4, 8 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ No
) |
| 10 | 7, 9 | mulscld 28161 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No
) |
| 11 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝐴 ·s 𝐵) ∈ No
) |
| 12 | | ssltss1 27833 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No
) |
| 13 | 1, 12 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ⊆ No
) |
| 14 | 13 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐿) → 𝑝 ∈ No
) |
| 15 | 14 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑝 ∈ No
) |
| 16 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐵 ∈ No
) |
| 17 | 15, 16 | mulscld 28161 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑝 ·s 𝐵) ∈ No
) |
| 18 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐴 ∈ No
) |
| 19 | | ssltss1 27833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 <<s 𝑆 → 𝑀 ⊆ No
) |
| 20 | 2, 19 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ⊆ No
) |
| 21 | 20 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑀) → 𝑞 ∈ No
) |
| 22 | 21 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑞 ∈ No
) |
| 23 | 18, 22 | mulscld 28161 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝐴 ·s 𝑞) ∈ No
) |
| 24 | 15, 22 | mulscld 28161 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑝 ·s 𝑞) ∈ No
) |
| 25 | 23, 24 | subscld 28093 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)) ∈ No
) |
| 26 | 11, 17, 25 | subsubs4d 28124 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))) = ((𝐴 ·s 𝐵) -s ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 ·s 𝐵) -s (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) = ((𝐴 ·s 𝐵) -s ((𝐴 ·s 𝐵) -s ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))))) |
| 28 | 17, 25 | addscld 28013 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))) ∈ No
) |
| 29 | 11, 28 | nncansd 28126 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 ·s 𝐵) -s ((𝐴 ·s 𝐵) -s ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) |
| 30 | 27, 29 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 ·s 𝐵) -s (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) |
| 31 | 18, 15 | subscld 28093 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝐴 -s 𝑝) ∈ No
) |
| 32 | 31, 16, 22 | subsdid 28184 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)) = (((𝐴 -s 𝑝) ·s 𝐵) -s ((𝐴 -s 𝑝) ·s 𝑞))) |
| 33 | 18, 15, 16 | subsdird 28185 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 -s 𝑝) ·s 𝐵) = ((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵))) |
| 34 | 18, 15, 22 | subsdird 28185 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 -s 𝑝) ·s 𝑞) = ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))) |
| 35 | 33, 34 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝐴 -s 𝑝) ·s 𝐵) -s ((𝐴 -s 𝑝) ·s 𝑞)) = (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) |
| 36 | 32, 35 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)) = (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞))) = ((𝐴 ·s 𝐵) -s (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))) |
| 38 | 17, 23, 24 | addsubsassd 28111 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) |
| 39 | 30, 37, 38 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))) |
| 40 | 39 | eqeq2d 2748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞))))) |
| 41 | 40 | 2rexbidva 3220 |
. . . . 5
⊢ (𝜑 → (∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞))))) |
| 42 | 41 | abbidv 2808 |
. . . 4
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} = {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))}) |
| 43 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝐴 ·s 𝐵) ∈ No
) |
| 44 | | ssltss2 27834 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No
) |
| 45 | 1, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ⊆ No
) |
| 46 | 45 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No
) |
| 47 | 46 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑟 ∈ No
) |
| 48 | | ssltss2 27834 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 <<s 𝑆 → 𝑆 ⊆ No
) |
| 49 | 2, 48 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ No
) |
| 50 | 49 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No
) |
| 51 | 50 | adantrl 716 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑠 ∈ No
) |
| 52 | 47, 51 | mulscld 28161 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 ·s 𝑠) ∈ No
) |
| 53 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 ∈ No
) |
| 54 | 53, 51 | mulscld 28161 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝐴 ·s 𝑠) ∈ No
) |
| 55 | 52, 54 | subscld 28093 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) ∈ No
) |
| 56 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 ∈ No
) |
| 57 | 47, 56 | mulscld 28161 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 ·s 𝐵) ∈ No
) |
| 58 | 57, 43 | subscld 28093 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)) ∈ No
) |
| 59 | 43, 55, 58 | subsubs2d 28125 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝐴 ·s 𝐵) -s (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))) = ((𝐴 ·s 𝐵) +s (((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))))) |
| 60 | 43, 58, 55 | addsubsassd 28111 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝐴 ·s 𝐵) +s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))) = ((𝐴 ·s 𝐵) +s (((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))))) |
| 61 | | pncan3s 28103 |
. . . . . . . . . . 11
⊢ (((𝐴 ·s 𝐵) ∈
No ∧ (𝑟
·s 𝐵)
∈ No ) → ((𝐴 ·s 𝐵) +s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))) = (𝑟 ·s 𝐵)) |
| 62 | 43, 57, 61 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝐴 ·s 𝐵) +s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))) = (𝑟 ·s 𝐵)) |
| 63 | 62 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝐴 ·s 𝐵) +s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))) = ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)))) |
| 64 | 59, 60, 63 | 3eqtr2d 2783 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝐴 ·s 𝐵) -s (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))) = ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)))) |
| 65 | 47, 53 | subscld 28093 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 -s 𝐴) ∈ No
) |
| 66 | 65, 51, 56 | subsdid 28184 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)) = (((𝑟 -s 𝐴) ·s 𝑠) -s ((𝑟 -s 𝐴) ·s 𝐵))) |
| 67 | 47, 53, 51 | subsdird 28185 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 -s 𝐴) ·s 𝑠) = ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))) |
| 68 | 47, 53, 56 | subsdird 28185 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 -s 𝐴) ·s 𝐵) = ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))) |
| 69 | 67, 68 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 -s 𝐴) ·s 𝑠) -s ((𝑟 -s 𝐴) ·s 𝐵)) = (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))) |
| 70 | 66, 69 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)) = (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))) |
| 71 | 70 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵))) = ((𝐴 ·s 𝐵) -s (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))))) |
| 72 | 57, 54, 52 | addsubsassd 28111 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝑟 ·s 𝐵) +s ((𝐴 ·s 𝑠) -s (𝑟 ·s 𝑠)))) |
| 73 | 57, 52, 54 | subsubs2d 28125 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))) = ((𝑟 ·s 𝐵) +s ((𝐴 ·s 𝑠) -s (𝑟 ·s 𝑠)))) |
| 74 | 72, 73 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)))) |
| 75 | 64, 71, 74 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))) |
| 76 | 75 | eqeq2d 2748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵))))) |
| 77 | 76 | 2rexbidva 3220 |
. . . . 5
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵))))) |
| 78 | 77 | abbidv 2808 |
. . . 4
⊢ (𝜑 → {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} = {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))}) |
| 79 | 42, 78 | uneq12d 4169 |
. . 3
⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) = ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))})) |
| 80 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → 𝐴 ∈ No
) |
| 81 | 49 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ No
) |
| 82 | 81 | adantrl 716 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → 𝑢 ∈ No
) |
| 83 | 80, 82 | mulscld 28161 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (𝐴 ·s 𝑢) ∈ No
) |
| 84 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (𝐴 ·s 𝐵) ∈ No
) |
| 85 | 83, 84 | subscld 28093 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) ∈ No
) |
| 86 | 13 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → 𝑡 ∈ No
) |
| 87 | 86 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → 𝑡 ∈ No
) |
| 88 | 87, 82 | mulscld 28161 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (𝑡 ·s 𝑢) ∈ No
) |
| 89 | 9 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → 𝐵 ∈ No
) |
| 90 | 87, 89 | mulscld 28161 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (𝑡 ·s 𝐵) ∈ No
) |
| 91 | 85, 88, 90 | subsubs2d 28125 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)))) |
| 92 | 90, 88 | subscld 28093 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)) ∈ No
) |
| 93 | 83, 92, 84 | addsubsd 28112 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵)) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)))) |
| 94 | 91, 93 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))) = (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵))) |
| 95 | 94 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))) = ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵)))) |
| 96 | 83, 92 | addscld 28013 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) ∈ No
) |
| 97 | | pncan3s 28103 |
. . . . . . . . . 10
⊢ (((𝐴 ·s 𝐵) ∈
No ∧ ((𝐴
·s 𝑢)
+s ((𝑡
·s 𝐵)
-s (𝑡
·s 𝑢)))
∈ No ) → ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵))) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)))) |
| 98 | 84, 96, 97 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵))) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)))) |
| 99 | 95, 98 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)))) |
| 100 | 82, 89 | subscld 28093 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (𝑢 -s 𝐵) ∈ No
) |
| 101 | 80, 87, 100 | subsdird 28185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)) = ((𝐴 ·s (𝑢 -s 𝐵)) -s (𝑡 ·s (𝑢 -s 𝐵)))) |
| 102 | 80, 82, 89 | subsdid 28184 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (𝐴 ·s (𝑢 -s 𝐵)) = ((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵))) |
| 103 | 87, 82, 89 | subsdid 28184 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (𝑡 ·s (𝑢 -s 𝐵)) = ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))) |
| 104 | 102, 103 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 ·s (𝑢 -s 𝐵)) -s (𝑡 ·s (𝑢 -s 𝐵))) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))) |
| 105 | 101, 104 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))) |
| 106 | 105 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))) = ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))))) |
| 107 | 90, 83 | addscomd 28000 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → ((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵))) |
| 108 | 107 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵)) -s (𝑡 ·s 𝑢))) |
| 109 | 83, 90, 88 | addsubsassd 28111 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)))) |
| 110 | 108, 109 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)))) |
| 111 | 99, 106, 110 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) |
| 112 | 111 | eqeq2d 2748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆)) → (𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))) |
| 113 | 112 | 2rexbidva 3220 |
. . . . 5
⊢ (𝜑 → (∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))) |
| 114 | 113 | abbidv 2808 |
. . . 4
⊢ (𝜑 → {𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} = {𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))}) |
| 115 | 45 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → 𝑣 ∈ No
) |
| 116 | 115 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → 𝑣 ∈ No
) |
| 117 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → 𝐵 ∈ No
) |
| 118 | 116, 117 | mulscld 28161 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (𝑣 ·s 𝐵) ∈ No
) |
| 119 | 20 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑀) → 𝑤 ∈ No
) |
| 120 | 119 | adantrl 716 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → 𝑤 ∈ No
) |
| 121 | 116, 120 | mulscld 28161 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (𝑣 ·s 𝑤) ∈ No
) |
| 122 | 118, 121 | subscld 28093 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) ∈ No
) |
| 123 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (𝐴 ·s 𝐵) ∈ No
) |
| 124 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → 𝐴 ∈ No
) |
| 125 | 124, 120 | mulscld 28161 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (𝐴 ·s 𝑤) ∈ No
) |
| 126 | 122, 123,
125 | subsubs2d 28125 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s ((𝐴 ·s 𝑤) -s (𝐴 ·s 𝐵)))) |
| 127 | 122, 125,
123 | addsubsassd 28111 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵)) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s ((𝐴 ·s 𝑤) -s (𝐴 ·s 𝐵)))) |
| 128 | 126, 127 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))) = ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵))) |
| 129 | 128 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((𝐴 ·s 𝐵) +s (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))) = ((𝐴 ·s 𝐵) +s ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵)))) |
| 130 | 122, 125 | addscld 28013 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) ∈ No
) |
| 131 | | pncan3s 28103 |
. . . . . . . . . 10
⊢ (((𝐴 ·s 𝐵) ∈
No ∧ (((𝑣
·s 𝐵)
-s (𝑣
·s 𝑤))
+s (𝐴
·s 𝑤))
∈ No ) → ((𝐴 ·s 𝐵) +s ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤))) |
| 132 | 123, 130,
131 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((𝐴 ·s 𝐵) +s ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤))) |
| 133 | 129, 132 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((𝐴 ·s 𝐵) +s (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤))) |
| 134 | 117, 120 | subscld 28093 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (𝐵 -s 𝑤) ∈ No
) |
| 135 | 116, 124,
134 | subsdird 28185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)) = ((𝑣 ·s (𝐵 -s 𝑤)) -s (𝐴 ·s (𝐵 -s 𝑤)))) |
| 136 | 116, 117,
120 | subsdid 28184 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (𝑣 ·s (𝐵 -s 𝑤)) = ((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤))) |
| 137 | 124, 117,
120 | subsdid 28184 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (𝐴 ·s (𝐵 -s 𝑤)) = ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))) |
| 138 | 136, 137 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((𝑣 ·s (𝐵 -s 𝑤)) -s (𝐴 ·s (𝐵 -s 𝑤))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))) |
| 139 | 135, 138 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))) |
| 140 | 139 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤))) = ((𝐴 ·s 𝐵) +s (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))))) |
| 141 | 118, 125,
121 | addsubsd 28112 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤))) |
| 142 | 133, 140,
141 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))) |
| 143 | 142 | eqeq2d 2748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀)) → (𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤))))) |
| 144 | 143 | 2rexbidva 3220 |
. . . . 5
⊢ (𝜑 → (∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤))))) |
| 145 | 144 | abbidv 2808 |
. . . 4
⊢ (𝜑 → {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))} = {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))}) |
| 146 | 114, 145 | uneq12d 4169 |
. . 3
⊢ (𝜑 → ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))})) |
| 147 | 79, 146 | oveq12d 7449 |
. 2
⊢ (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) = (({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))}) |s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))}))) |
| 148 | 5, 147 | eqtrd 2777 |
1
⊢ (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))}) |s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))}))) |