MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsunif2lem Structured version   Visualization version   GIF version

Theorem mulsunif2lem 28195
Description: Lemma for mulsunif2 28196. State the theorem with extra disjoint variable conditions. (Contributed by Scott Fenton, 16-Mar-2025.)
Hypotheses
Ref Expression
mulsunif2.1 (𝜑𝐿 <<s 𝑅)
mulsunif2.2 (𝜑𝑀 <<s 𝑆)
mulsunif2.3 (𝜑𝐴 = (𝐿 |s 𝑅))
mulsunif2.4 (𝜑𝐵 = (𝑀 |s 𝑆))
Assertion
Ref Expression
mulsunif2lem (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))} ∪ {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))}) |s ({𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))})))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑣,𝑤   𝐵,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑣,𝑤   𝐿,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑣,𝑤   𝑅,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑣,𝑤   𝑀,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑣,𝑤   𝑆,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑣,𝑤   𝜑,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑣,𝑤

Proof of Theorem mulsunif2lem
StepHypRef Expression
1 mulsunif2.1 . . 3 (𝜑𝐿 <<s 𝑅)
2 mulsunif2.2 . . 3 (𝜑𝑀 <<s 𝑆)
3 mulsunif2.3 . . 3 (𝜑𝐴 = (𝐿 |s 𝑅))
4 mulsunif2.4 . . 3 (𝜑𝐵 = (𝑀 |s 𝑆))
51, 2, 3, 4mulsunif 28176 . 2 (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
61scutcld 27848 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 |s 𝑅) ∈ No )
73, 6eqeltrd 2841 . . . . . . . . . . . . 13 (𝜑𝐴 No )
82scutcld 27848 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 |s 𝑆) ∈ No )
94, 8eqeltrd 2841 . . . . . . . . . . . . 13 (𝜑𝐵 No )
107, 9mulscld 28161 . . . . . . . . . . . 12 (𝜑 → (𝐴 ·s 𝐵) ∈ No )
1110adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝐴 ·s 𝐵) ∈ No )
12 ssltss1 27833 . . . . . . . . . . . . . . 15 (𝐿 <<s 𝑅𝐿 No )
131, 12syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿 No )
1413sselda 3983 . . . . . . . . . . . . 13 ((𝜑𝑝𝐿) → 𝑝 No )
1514adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → 𝑝 No )
169adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → 𝐵 No )
1715, 16mulscld 28161 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝑝 ·s 𝐵) ∈ No )
187adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → 𝐴 No )
19 ssltss1 27833 . . . . . . . . . . . . . . . 16 (𝑀 <<s 𝑆𝑀 No )
202, 19syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑀 No )
2120sselda 3983 . . . . . . . . . . . . . 14 ((𝜑𝑞𝑀) → 𝑞 No )
2221adantrl 716 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → 𝑞 No )
2318, 22mulscld 28161 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝐴 ·s 𝑞) ∈ No )
2415, 22mulscld 28161 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝑝 ·s 𝑞) ∈ No )
2523, 24subscld 28093 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)) ∈ No )
2611, 17, 25subsubs4d 28124 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))) = ((𝐴 ·s 𝐵) -s ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))))
2726oveq2d 7447 . . . . . . . . 9 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 ·s 𝐵) -s (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) = ((𝐴 ·s 𝐵) -s ((𝐴 ·s 𝐵) -s ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))))
2817, 25addscld 28013 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))) ∈ No )
2911, 28nncansd 28126 . . . . . . . . 9 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 ·s 𝐵) -s ((𝐴 ·s 𝐵) -s ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3027, 29eqtrd 2777 . . . . . . . 8 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 ·s 𝐵) -s (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3118, 15subscld 28093 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝐴 -s 𝑝) ∈ No )
3231, 16, 22subsdid 28184 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)) = (((𝐴 -s 𝑝) ·s 𝐵) -s ((𝐴 -s 𝑝) ·s 𝑞)))
3318, 15, 16subsdird 28185 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 -s 𝑝) ·s 𝐵) = ((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)))
3418, 15, 22subsdird 28185 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 -s 𝑝) ·s 𝑞) = ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))
3533, 34oveq12d 7449 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (((𝐴 -s 𝑝) ·s 𝐵) -s ((𝐴 -s 𝑝) ·s 𝑞)) = (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3632, 35eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)) = (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3736oveq2d 7447 . . . . . . . 8 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞))) = ((𝐴 ·s 𝐵) -s (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))))
3817, 23, 24addsubsassd 28111 . . . . . . . 8 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3930, 37, 383eqtr4rd 2788 . . . . . . 7 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞))))
4039eqeq2d 2748 . . . . . 6 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))))
41402rexbidva 3220 . . . . 5 (𝜑 → (∃𝑝𝐿𝑞𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝𝐿𝑞𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))))
4241abbidv 2808 . . . 4 (𝜑 → {𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} = {𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))})
4310adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝐴 ·s 𝐵) ∈ No )
44 ssltss2 27834 . . . . . . . . . . . . . . 15 (𝐿 <<s 𝑅𝑅 No )
451, 44syl 17 . . . . . . . . . . . . . 14 (𝜑𝑅 No )
4645sselda 3983 . . . . . . . . . . . . 13 ((𝜑𝑟𝑅) → 𝑟 No )
4746adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → 𝑟 No )
48 ssltss2 27834 . . . . . . . . . . . . . . 15 (𝑀 <<s 𝑆𝑆 No )
492, 48syl 17 . . . . . . . . . . . . . 14 (𝜑𝑆 No )
5049sselda 3983 . . . . . . . . . . . . 13 ((𝜑𝑠𝑆) → 𝑠 No )
5150adantrl 716 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → 𝑠 No )
5247, 51mulscld 28161 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝑟 ·s 𝑠) ∈ No )
537adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → 𝐴 No )
5453, 51mulscld 28161 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝐴 ·s 𝑠) ∈ No )
5552, 54subscld 28093 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) ∈ No )
569adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → 𝐵 No )
5747, 56mulscld 28161 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝑟 ·s 𝐵) ∈ No )
5857, 43subscld 28093 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)) ∈ No )
5943, 55, 58subsubs2d 28125 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝐴 ·s 𝐵) -s (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))) = ((𝐴 ·s 𝐵) +s (((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)))))
6043, 58, 55addsubsassd 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 𝐵))
6243, 57, 61syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝐴 ·s 𝐵) +s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))) = (𝑟 ·s 𝐵))
6362oveq1d 7446 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝐴 ·s 𝐵) +s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))) = ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))))
6459, 60, 633eqtr2d 2783 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝐴 ·s 𝐵) -s (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))) = ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))))
6547, 53subscld 28093 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝑟 -s 𝐴) ∈ No )
6665, 51, 56subsdid 28184 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)) = (((𝑟 -s 𝐴) ·s 𝑠) -s ((𝑟 -s 𝐴) ·s 𝐵)))
6747, 53, 51subsdird 28185 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 -s 𝐴) ·s 𝑠) = ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)))
6847, 53, 56subsdird 28185 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 -s 𝐴) ·s 𝐵) = ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))
6967, 68oveq12d 7449 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝑟 -s 𝐴) ·s 𝑠) -s ((𝑟 -s 𝐴) ·s 𝐵)) = (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))))
7066, 69eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)) = (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))))
7170oveq2d 7447 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵))) = ((𝐴 ·s 𝐵) -s (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))))
7257, 54, 52addsubsassd 28111 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝑟 ·s 𝐵) +s ((𝐴 ·s 𝑠) -s (𝑟 ·s 𝑠))))
7357, 52, 54subsubs2d 28125 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))) = ((𝑟 ·s 𝐵) +s ((𝐴 ·s 𝑠) -s (𝑟 ·s 𝑠))))
7472, 73eqtr4d 2780 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))))
7564, 71, 743eqtr4rd 2788 . . . . . . 7 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵))))
7675eqeq2d 2748 . . . . . 6 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))))
77762rexbidva 3220 . . . . 5 (𝜑 → (∃𝑟𝑅𝑠𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑟𝑅𝑠𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))))
7877abbidv 2808 . . . 4 (𝜑 → {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} = {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))})
7942, 78uneq12d 4169 . . 3 (𝜑 → ({𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) = ({𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))} ∪ {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))}))
807adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → 𝐴 No )
8149sselda 3983 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑆) → 𝑢 No )
8281adantrl 716 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → 𝑢 No )
8380, 82mulscld 28161 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝐴 ·s 𝑢) ∈ No )
8410adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝐴 ·s 𝐵) ∈ No )
8583, 84subscld 28093 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) ∈ No )
8613sselda 3983 . . . . . . . . . . . . . 14 ((𝜑𝑡𝐿) → 𝑡 No )
8786adantrr 717 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → 𝑡 No )
8887, 82mulscld 28161 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑡 ·s 𝑢) ∈ No )
899adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → 𝐵 No )
9087, 89mulscld 28161 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑡 ·s 𝐵) ∈ No )
9185, 88, 90subsubs2d 28125 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
9290, 88subscld 28093 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)) ∈ No )
9383, 92, 84addsubsd 28112 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵)) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
9491, 93eqtr4d 2780 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))) = (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵)))
9594oveq2d 7447 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))) = ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵))))
9683, 92addscld 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 𝑢))))
9884, 96, 97syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵))) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
9995, 98eqtrd 2777 . . . . . . . 8 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
10082, 89subscld 28093 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑢 -s 𝐵) ∈ No )
10180, 87, 100subsdird 28185 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)) = ((𝐴 ·s (𝑢 -s 𝐵)) -s (𝑡 ·s (𝑢 -s 𝐵))))
10280, 82, 89subsdid 28184 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝐴 ·s (𝑢 -s 𝐵)) = ((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)))
10387, 82, 89subsdid 28184 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑡 ·s (𝑢 -s 𝐵)) = ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))
104102, 103oveq12d 7449 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s (𝑢 -s 𝐵)) -s (𝑡 ·s (𝑢 -s 𝐵))) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))))
105101, 104eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))))
106105oveq2d 7447 . . . . . . . 8 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))) = ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))))
10790, 83addscomd 28000 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵)))
108107oveq1d 7446 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵)) -s (𝑡 ·s 𝑢)))
10983, 90, 88addsubsassd 28111 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
110108, 109eqtrd 2777 . . . . . . . 8 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
11199, 106, 1103eqtr4rd 2788 . . . . . . 7 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))
112111eqeq2d 2748 . . . . . 6 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))))
1131122rexbidva 3220 . . . . 5 (𝜑 → (∃𝑡𝐿𝑢𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑡𝐿𝑢𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))))
114113abbidv 2808 . . . 4 (𝜑 → {𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} = {𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))})
11545sselda 3983 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝑅) → 𝑣 No )
116115adantrr 717 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → 𝑣 No )
1179adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → 𝐵 No )
118116, 117mulscld 28161 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝑣 ·s 𝐵) ∈ No )
11920sselda 3983 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑀) → 𝑤 No )
120119adantrl 716 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → 𝑤 No )
121116, 120mulscld 28161 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝑣 ·s 𝑤) ∈ No )
122118, 121subscld 28093 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) ∈ No )
12310adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝐴 ·s 𝐵) ∈ No )
1247adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → 𝐴 No )
125124, 120mulscld 28161 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝐴 ·s 𝑤) ∈ No )
126122, 123, 125subsubs2d 28125 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s ((𝐴 ·s 𝑤) -s (𝐴 ·s 𝐵))))
127122, 125, 123addsubsassd 28111 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵)) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s ((𝐴 ·s 𝑤) -s (𝐴 ·s 𝐵))))
128126, 127eqtr4d 2780 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))) = ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵)))
129128oveq2d 7447 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝐴 ·s 𝐵) +s (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))) = ((𝐴 ·s 𝐵) +s ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵))))
130122, 125addscld 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 𝑤)))
132123, 130, 131syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝐴 ·s 𝐵) +s ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)))
133129, 132eqtrd 2777 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝐴 ·s 𝐵) +s (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)))
134117, 120subscld 28093 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝐵 -s 𝑤) ∈ No )
135116, 124, 134subsdird 28185 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)) = ((𝑣 ·s (𝐵 -s 𝑤)) -s (𝐴 ·s (𝐵 -s 𝑤))))
136116, 117, 120subsdid 28184 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝑣 ·s (𝐵 -s 𝑤)) = ((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)))
137124, 117, 120subsdid 28184 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝐴 ·s (𝐵 -s 𝑤)) = ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))
138136, 137oveq12d 7449 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝑣 ·s (𝐵 -s 𝑤)) -s (𝐴 ·s (𝐵 -s 𝑤))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))))
139135, 138eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))))
140139oveq2d 7447 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤))) = ((𝐴 ·s 𝐵) +s (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))))
141118, 125, 121addsubsd 28112 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)))
142133, 140, 1413eqtr4rd 2788 . . . . . . 7 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤))))
143142eqeq2d 2748 . . . . . 6 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))))
1441432rexbidva 3220 . . . . 5 (𝜑 → (∃𝑣𝑅𝑤𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑣𝑅𝑤𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))))
145144abbidv 2808 . . . 4 (𝜑 → {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))} = {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))})
146114, 145uneq12d 4169 . . 3 (𝜑 → ({𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = ({𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))}))
14779, 146oveq12d 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 𝑤)))})))
1485, 147eqtrd 2777 1 (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))} ∪ {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))}) |s ({𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  {cab 2714  wrex 3070  cun 3949  wss 3951   class class class wbr 5143  (class class class)co 7431   No csur 27684   <<s csslt 27825   |s cscut 27827   +s cadds 27992   -s csubs 28052   ·s cmuls 28132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-1o 8506  df-2o 8507  df-nadd 8704  df-no 27687  df-slt 27688  df-bday 27689  df-sle 27790  df-sslt 27826  df-scut 27828  df-0s 27869  df-made 27886  df-old 27887  df-left 27889  df-right 27890  df-norec 27971  df-norec2 27982  df-adds 27993  df-negs 28053  df-subs 28054  df-muls 28133
This theorem is referenced by:  mulsunif2  28196
  Copyright terms: Public domain W3C validator