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

Theorem mulsunif2lem 28210
Description: Lemma for mulsunif2 28211. 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 28191 . 2 (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
61scutcld 27863 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 |s 𝑅) ∈ No )
73, 6eqeltrd 2839 . . . . . . . . . . . . 13 (𝜑𝐴 No )
82scutcld 27863 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 |s 𝑆) ∈ No )
94, 8eqeltrd 2839 . . . . . . . . . . . . 13 (𝜑𝐵 No )
107, 9mulscld 28176 . . . . . . . . . . . 12 (𝜑 → (𝐴 ·s 𝐵) ∈ No )
1110adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝐴 ·s 𝐵) ∈ No )
12 ssltss1 27848 . . . . . . . . . . . . . . 15 (𝐿 <<s 𝑅𝐿 No )
131, 12syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿 No )
1413sselda 3995 . . . . . . . . . . . . 13 ((𝜑𝑝𝐿) → 𝑝 No )
1514adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → 𝑝 No )
169adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → 𝐵 No )
1715, 16mulscld 28176 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝑝 ·s 𝐵) ∈ No )
187adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → 𝐴 No )
19 ssltss1 27848 . . . . . . . . . . . . . . . 16 (𝑀 <<s 𝑆𝑀 No )
202, 19syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑀 No )
2120sselda 3995 . . . . . . . . . . . . . 14 ((𝜑𝑞𝑀) → 𝑞 No )
2221adantrl 716 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → 𝑞 No )
2318, 22mulscld 28176 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝐴 ·s 𝑞) ∈ No )
2415, 22mulscld 28176 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝑝 ·s 𝑞) ∈ No )
2523, 24subscld 28108 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)) ∈ No )
2611, 17, 25subsubs4d 28139 . . . . . . . . . 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 28028 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))) ∈ No )
2911, 28nncansd 28141 . . . . . . . . 9 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 ·s 𝐵) -s ((𝐴 ·s 𝐵) -s ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3027, 29eqtrd 2775 . . . . . . . 8 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 ·s 𝐵) -s (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3118, 15subscld 28108 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝐴 -s 𝑝) ∈ No )
3231, 16, 22subsdid 28199 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)) = (((𝐴 -s 𝑝) ·s 𝐵) -s ((𝐴 -s 𝑝) ·s 𝑞)))
3318, 15, 16subsdird 28200 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 -s 𝑝) ·s 𝐵) = ((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)))
3418, 15, 22subsdird 28200 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → ((𝐴 -s 𝑝) ·s 𝑞) = ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞)))
3533, 34oveq12d 7449 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (((𝐴 -s 𝑝) ·s 𝐵) -s ((𝐴 -s 𝑝) ·s 𝑞)) = (((𝐴 ·s 𝐵) -s (𝑝 ·s 𝐵)) -s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3632, 35eqtrd 2775 . . . . . . . . 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 28126 . . . . . . . 8 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = ((𝑝 ·s 𝐵) +s ((𝐴 ·s 𝑞) -s (𝑝 ·s 𝑞))))
3930, 37, 383eqtr4rd 2786 . . . . . . 7 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞))))
4039eqeq2d 2746 . . . . . 6 ((𝜑 ∧ (𝑝𝐿𝑞𝑀)) → (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))))
41402rexbidva 3218 . . . . 5 (𝜑 → (∃𝑝𝐿𝑞𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝𝐿𝑞𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))))
4241abbidv 2806 . . . 4 (𝜑 → {𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} = {𝑎 ∣ ∃𝑝𝐿𝑞𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))})
4310adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝐴 ·s 𝐵) ∈ No )
44 ssltss2 27849 . . . . . . . . . . . . . . 15 (𝐿 <<s 𝑅𝑅 No )
451, 44syl 17 . . . . . . . . . . . . . 14 (𝜑𝑅 No )
4645sselda 3995 . . . . . . . . . . . . 13 ((𝜑𝑟𝑅) → 𝑟 No )
4746adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → 𝑟 No )
48 ssltss2 27849 . . . . . . . . . . . . . . 15 (𝑀 <<s 𝑆𝑆 No )
492, 48syl 17 . . . . . . . . . . . . . 14 (𝜑𝑆 No )
5049sselda 3995 . . . . . . . . . . . . 13 ((𝜑𝑠𝑆) → 𝑠 No )
5150adantrl 716 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → 𝑠 No )
5247, 51mulscld 28176 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝑟 ·s 𝑠) ∈ No )
537adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → 𝐴 No )
5453, 51mulscld 28176 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝐴 ·s 𝑠) ∈ No )
5552, 54subscld 28108 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) ∈ No )
569adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → 𝐵 No )
5747, 56mulscld 28176 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝑟 ·s 𝐵) ∈ No )
5857, 43subscld 28108 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)) ∈ No )
5943, 55, 58subsubs2d 28140 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝐴 ·s 𝐵) -s (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))) = ((𝐴 ·s 𝐵) +s (((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)))))
6043, 58, 55addsubsassd 28126 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝐴 ·s 𝐵) +s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))) = ((𝐴 ·s 𝐵) +s (((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)))))
61 pncan3s 28118 . . . . . . . . . . 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 2781 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝐴 ·s 𝐵) -s (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))) = ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))))
6547, 53subscld 28108 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝑟 -s 𝐴) ∈ No )
6665, 51, 56subsdid 28199 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)) = (((𝑟 -s 𝐴) ·s 𝑠) -s ((𝑟 -s 𝐴) ·s 𝐵)))
6747, 53, 51subsdird 28200 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 -s 𝐴) ·s 𝑠) = ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)))
6847, 53, 56subsdird 28200 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 -s 𝐴) ·s 𝐵) = ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵)))
6967, 68oveq12d 7449 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝑟 -s 𝐴) ·s 𝑠) -s ((𝑟 -s 𝐴) ·s 𝐵)) = (((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠)) -s ((𝑟 ·s 𝐵) -s (𝐴 ·s 𝐵))))
7066, 69eqtrd 2775 . . . . . . . . 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 28126 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝑟 ·s 𝐵) +s ((𝐴 ·s 𝑠) -s (𝑟 ·s 𝑠))))
7357, 52, 54subsubs2d 28140 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))) = ((𝑟 ·s 𝐵) +s ((𝐴 ·s 𝑠) -s (𝑟 ·s 𝑠))))
7472, 73eqtr4d 2778 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝑟 ·s 𝐵) -s ((𝑟 ·s 𝑠) -s (𝐴 ·s 𝑠))))
7564, 71, 743eqtr4rd 2786 . . . . . . 7 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵))))
7675eqeq2d 2746 . . . . . 6 ((𝜑 ∧ (𝑟𝑅𝑠𝑆)) → (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))))
77762rexbidva 3218 . . . . 5 (𝜑 → (∃𝑟𝑅𝑠𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑟𝑅𝑠𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))))
7877abbidv 2806 . . . 4 (𝜑 → {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} = {𝑏 ∣ ∃𝑟𝑅𝑠𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))})
7942, 78uneq12d 4179 . . 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 3995 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑆) → 𝑢 No )
8281adantrl 716 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → 𝑢 No )
8380, 82mulscld 28176 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝐴 ·s 𝑢) ∈ No )
8410adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝐴 ·s 𝐵) ∈ No )
8583, 84subscld 28108 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) ∈ No )
8613sselda 3995 . . . . . . . . . . . . . 14 ((𝜑𝑡𝐿) → 𝑡 No )
8786adantrr 717 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → 𝑡 No )
8887, 82mulscld 28176 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑡 ·s 𝑢) ∈ No )
899adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → 𝐵 No )
9087, 89mulscld 28176 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑡 ·s 𝐵) ∈ No )
9185, 88, 90subsubs2d 28140 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
9290, 88subscld 28108 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢)) ∈ No )
9383, 92, 84addsubsd 28127 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) -s (𝐴 ·s 𝐵)) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
9491, 93eqtr4d 2778 . . . . . . . . . 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 28028 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))) ∈ No )
97 pncan3s 28118 . . . . . . . . . 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 2775 . . . . . . . 8 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s 𝐵) +s (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
10082, 89subscld 28108 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑢 -s 𝐵) ∈ No )
10180, 87, 100subsdird 28200 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)) = ((𝐴 ·s (𝑢 -s 𝐵)) -s (𝑡 ·s (𝑢 -s 𝐵))))
10280, 82, 89subsdid 28199 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝐴 ·s (𝑢 -s 𝐵)) = ((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)))
10387, 82, 89subsdid 28199 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑡 ·s (𝑢 -s 𝐵)) = ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵)))
104102, 103oveq12d 7449 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝐴 ·s (𝑢 -s 𝐵)) -s (𝑡 ·s (𝑢 -s 𝐵))) = (((𝐴 ·s 𝑢) -s (𝐴 ·s 𝐵)) -s ((𝑡 ·s 𝑢) -s (𝑡 ·s 𝐵))))
105101, 104eqtrd 2775 . . . . . . . . 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 28015 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → ((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵)))
108107oveq1d 7446 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵)) -s (𝑡 ·s 𝑢)))
10983, 90, 88addsubsassd 28126 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝐴 ·s 𝑢) +s (𝑡 ·s 𝐵)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
110108, 109eqtrd 2775 . . . . . . . 8 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝑢) +s ((𝑡 ·s 𝐵) -s (𝑡 ·s 𝑢))))
11199, 106, 1103eqtr4rd 2786 . . . . . . 7 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))
112111eqeq2d 2746 . . . . . 6 ((𝜑 ∧ (𝑡𝐿𝑢𝑆)) → (𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))))
1131122rexbidva 3218 . . . . 5 (𝜑 → (∃𝑡𝐿𝑢𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑡𝐿𝑢𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))))
114113abbidv 2806 . . . 4 (𝜑 → {𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} = {𝑐 ∣ ∃𝑡𝐿𝑢𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))})
11545sselda 3995 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝑅) → 𝑣 No )
116115adantrr 717 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → 𝑣 No )
1179adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → 𝐵 No )
118116, 117mulscld 28176 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝑣 ·s 𝐵) ∈ No )
11920sselda 3995 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑀) → 𝑤 No )
120119adantrl 716 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → 𝑤 No )
121116, 120mulscld 28176 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝑣 ·s 𝑤) ∈ No )
122118, 121subscld 28108 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) ∈ No )
12310adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝐴 ·s 𝐵) ∈ No )
1247adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → 𝐴 No )
125124, 120mulscld 28176 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝐴 ·s 𝑤) ∈ No )
126122, 123, 125subsubs2d 28140 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s ((𝐴 ·s 𝑤) -s (𝐴 ·s 𝐵))))
127122, 125, 123addsubsassd 28126 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) -s (𝐴 ·s 𝐵)) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s ((𝐴 ·s 𝑤) -s (𝐴 ·s 𝐵))))
128126, 127eqtr4d 2778 . . . . . . . . . 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 28028 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)) ∈ No )
131 pncan3s 28118 . . . . . . . . . 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 2775 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝐴 ·s 𝐵) +s (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)))
134117, 120subscld 28108 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝐵 -s 𝑤) ∈ No )
135116, 124, 134subsdird 28200 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)) = ((𝑣 ·s (𝐵 -s 𝑤)) -s (𝐴 ·s (𝐵 -s 𝑤))))
136116, 117, 120subsdid 28199 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝑣 ·s (𝐵 -s 𝑤)) = ((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)))
137124, 117, 120subsdid 28199 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝐴 ·s (𝐵 -s 𝑤)) = ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤)))
138136, 137oveq12d 7449 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → ((𝑣 ·s (𝐵 -s 𝑤)) -s (𝐴 ·s (𝐵 -s 𝑤))) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) -s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑤))))
139135, 138eqtrd 2775 . . . . . . . . 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 28127 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝑣 ·s 𝐵) -s (𝑣 ·s 𝑤)) +s (𝐴 ·s 𝑤)))
142133, 140, 1413eqtr4rd 2786 . . . . . . 7 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤))))
143142eqeq2d 2746 . . . . . 6 ((𝜑 ∧ (𝑣𝑅𝑤𝑀)) → (𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))))
1441432rexbidva 3218 . . . . 5 (𝜑 → (∃𝑣𝑅𝑤𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑣𝑅𝑤𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))))
145144abbidv 2806 . . . 4 (𝜑 → {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))} = {𝑑 ∣ ∃𝑣𝑅𝑤𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))})
146114, 145uneq12d 4179 . . 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 2775 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 1537  wcel 2106  {cab 2712  wrex 3068  cun 3961  wss 3963   class class class wbr 5148  (class class class)co 7431   No csur 27699   <<s csslt 27840   |s cscut 27842   +s cadds 28007   -s csubs 28067   ·s cmuls 28147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-ot 4640  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-1o 8505  df-2o 8506  df-nadd 8703  df-no 27702  df-slt 27703  df-bday 27704  df-sle 27805  df-sslt 27841  df-scut 27843  df-0s 27884  df-made 27901  df-old 27902  df-left 27904  df-right 27905  df-norec 27986  df-norec2 27997  df-adds 28008  df-negs 28068  df-subs 28069  df-muls 28148
This theorem is referenced by:  mulsunif2  28211
  Copyright terms: Public domain W3C validator