Metamath Proof Explorer

Theorem mulsunif2lem

Description: Lemma for mulsunif2 . State the theorem with extra disjoint variable conditions. (Contributed by Scott Fenton, 16-Mar-2025)

Ref Expression
Hypotheses mulsunif2.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
mulsunif2.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
mulsunif2.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
mulsunif2.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
Assertion mulsunif2lem ( 𝜑 → ( 𝐴 ·s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( 𝐴 ·s 𝐵 ) -s ( ( 𝐴 -s 𝑝 ) ·s ( 𝐵 -s 𝑞 ) ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( 𝐴 ·s 𝐵 ) -s ( ( 𝑟 -s 𝐴 ) ·s ( 𝑠 -s 𝐵 ) ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( 𝐴 ·s 𝐵 ) +s ( ( 𝐴 -s 𝑡 ) ·s ( 𝑢 -s 𝐵 ) ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( 𝐴 ·s 𝐵 ) +s ( ( 𝑣 -s 𝐴 ) ·s ( 𝐵 -s 𝑤 ) ) ) } ) ) )

Proof

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