Metamath Proof Explorer

Theorem mulsval

Description: The value of surreal multiplication. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion mulsval ⊢ A ∈ No ∧ B ∈ No → A ⋅ s B = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w

Proof

Step Hyp Ref Expression
1 df-muls ⊢ ⋅ s = norec2 s #A# z ∈ V , m ∈ V ⟼ ⦋ 1 st ⁡ z / x⦌ ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w
2 1 norec2ov ⊢ A ∈ No ∧ B ∈ No → A ⋅ s B = A B z ∈ V , m ∈ V ⟼ ⦋ 1 st ⁡ z / x⦌ ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
3 opex ⊢ A B ∈ V
4 mulsfn ⊢ ⋅ s Fn No × No
5 fnfun ⊢ ⋅ s Fn No × No → Fun ⁡ ⋅ s
6 4 5 ax-mp ⊢ Fun ⁡ ⋅ s
7 fvex ⊢ L ⁡ A ∈ V
8 fvex ⊢ R ⁡ A ∈ V
9 7 8 unex ⊢ L ⁡ A ∪ R ⁡ A ∈ V
10 snex ⊢ A ∈ V
11 9 10 unex ⊢ L ⁡ A ∪ R ⁡ A ∪ A ∈ V
12 fvex ⊢ L ⁡ B ∈ V
13 fvex ⊢ R ⁡ B ∈ V
14 12 13 unex ⊢ L ⁡ B ∪ R ⁡ B ∈ V
15 snex ⊢ B ∈ V
16 14 15 unex ⊢ L ⁡ B ∪ R ⁡ B ∪ B ∈ V
17 11 16 xpex ⊢ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∈ V
18 17 difexi ⊢ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ∈ V
19 resfunexg ⊢ Fun ⁡ ⋅ s ∧ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ∈ V → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ∈ V
20 6 18 19 mp2an ⊢ ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ∈ V
21 fveq2 ⊢ z = A B → 1 st ⁡ z = 1 st ⁡ A B
22 fveq2 ⊢ z = A B → 2 nd ⁡ z = 2 nd ⁡ A B
23 22 csbeq1d ⊢ z = A B → ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w = ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w
24 21 23 csbeq12dv ⊢ z = A B → ⦋ 1 st ⁡ z / x⦌ ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w = ⦋ 1 st ⁡ A B / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w
25 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → p m y = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y
26 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → x m q = x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
27 25 26 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → p m y + s x m q = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
28 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → p m q = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
29 27 28 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → p m y + s x m q - s p m q = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
30 29 eqeq2d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → a = p m y + s x m q - s p m q ↔ a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
31 30 2rexbidv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ↔ ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
32 31 abbidv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q = a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
33 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → r m y = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y
34 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → x m s = x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
35 33 34 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → r m y + s x m s = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
36 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → r m s = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
37 35 36 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → r m y + s x m s - s r m s = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
38 37 eqeq2d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → b = r m y + s x m s - s r m s ↔ b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
39 38 2rexbidv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s ↔ ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
40 39 abbidv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s = b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
41 32 40 uneq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s = a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
42 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → t m y = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y
43 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → x m u = x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
44 42 43 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → t m y + s x m u = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
45 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → t m u = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
46 44 45 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → t m y + s x m u - s t m u = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
47 46 eqeq2d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → c = t m y + s x m u - s t m u ↔ c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
48 47 2rexbidv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ↔ ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
49 48 abbidv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u = c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
50 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → v m y = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y
51 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → x m w = x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
52 50 51 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → v m y + s x m w = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
53 oveq ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → v m w = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
54 52 53 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → v m y + s x m w - s v m w = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
55 54 eqeq2d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → d = v m y + s x m w - s v m w ↔ d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
56 55 2rexbidv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w ↔ ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
57 56 abbidv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w = d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
58 49 57 uneq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w = c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
59 41 58 oveq12d ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w = a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
60 59 csbeq2dv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w = ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
61 60 csbeq2dv ⊢ m = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B → ⦋ 1 st ⁡ A B / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w = ⦋ 1 st ⁡ A B / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
62 eqid ⊢ z ∈ V , m ∈ V ⟼ ⦋ 1 st ⁡ z / x⦌ ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w = z ∈ V , m ∈ V ⟼ ⦋ 1 st ⁡ z / x⦌ ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w
63 ovex ⊢ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ∈ V
64 63 csbex ⊢ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ∈ V
65 64 csbex ⊢ ⦋ 1 st ⁡ A B / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ∈ V
66 24 61 62 65 ovmpo ⊢ A B ∈ V ∧ ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ∈ V → A B z ∈ V , m ∈ V ⟼ ⦋ 1 st ⁡ z / x⦌ ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B = ⦋ 1 st ⁡ A B / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
67 3 20 66 mp2an ⊢ A B z ∈ V , m ∈ V ⟼ ⦋ 1 st ⁡ z / x⦌ ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B = ⦋ 1 st ⁡ A B / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
68 op1stg ⊢ A ∈ No ∧ B ∈ No → 1 st ⁡ A B = A
69 68 csbeq1d ⊢ A ∈ No ∧ B ∈ No → ⦋ 1 st ⁡ A B / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = ⦋ A / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
70 op2ndg ⊢ A ∈ No ∧ B ∈ No → 2 nd ⁡ A B = B
71 70 csbeq1d ⊢ A ∈ No ∧ B ∈ No → ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = ⦋ B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
72 71 csbeq2dv ⊢ A ∈ No ∧ B ∈ No → ⦋ A / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = ⦋ A / x⦌ ⦋ B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
73 simpl ⊢ A ∈ No ∧ B ∈ No → A ∈ No
74 fveq2 ⊢ x = A → L ⁡ x = L ⁡ A
75 oveq1 ⊢ x = A → x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
76 75 oveq2d ⊢ x = A → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
77 76 oveq1d ⊢ x = A → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
78 77 eqeq2d ⊢ x = A → a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ↔ a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
79 78 rexbidv ⊢ x = A → ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ↔ ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
80 74 79 rexeqbidv ⊢ x = A → ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
81 80 abbidv ⊢ x = A → a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
82 fveq2 ⊢ x = A → R ⁡ x = R ⁡ A
83 oveq1 ⊢ x = A → x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
84 83 oveq2d ⊢ x = A → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
85 84 oveq1d ⊢ x = A → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
86 85 eqeq2d ⊢ x = A → b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s ↔ b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
87 86 rexbidv ⊢ x = A → ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s ↔ ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
88 82 87 rexeqbidv ⊢ x = A → ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s ↔ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
89 88 abbidv ⊢ x = A → b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
90 81 89 uneq12d ⊢ x = A → a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
91 oveq1 ⊢ x = A → x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
92 91 oveq2d ⊢ x = A → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
93 92 oveq1d ⊢ x = A → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
94 93 eqeq2d ⊢ x = A → c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ↔ c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
95 94 rexbidv ⊢ x = A → ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ↔ ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
96 74 95 rexeqbidv ⊢ x = A → ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
97 96 abbidv ⊢ x = A → c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
98 oveq1 ⊢ x = A → x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
99 98 oveq2d ⊢ x = A → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
100 99 oveq1d ⊢ x = A → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
101 100 eqeq2d ⊢ x = A → d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ↔ d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
102 101 rexbidv ⊢ x = A → ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ↔ ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
103 82 102 rexeqbidv ⊢ x = A → ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ↔ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
104 103 abbidv ⊢ x = A → d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
105 97 104 uneq12d ⊢ x = A → c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
106 90 105 oveq12d ⊢ x = A → a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
107 106 csbeq2dv ⊢ x = A → ⦋ B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = ⦋ B / y⦌ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
108 107 adantl ⊢ A ∈ No ∧ B ∈ No ∧ x = A → ⦋ B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = ⦋ B / y⦌ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
109 73 108 csbied ⊢ A ∈ No ∧ B ∈ No → ⦋ A / x⦌ ⦋ B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = ⦋ B / y⦌ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
110 simpr ⊢ A ∈ No ∧ B ∈ No → B ∈ No
111 fveq2 ⊢ y = B → L ⁡ y = L ⁡ B
112 oveq2 ⊢ y = B → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B
113 112 oveq1d ⊢ y = B → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
114 113 oveq1d ⊢ y = B → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
115 114 eqeq2d ⊢ y = B → a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ↔ a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
116 111 115 rexeqbidv ⊢ y = B → ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ↔ ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
117 116 rexbidv ⊢ y = B → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
118 117 abbidv ⊢ y = B → a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q
119 fveq2 ⊢ y = B → R ⁡ y = R ⁡ B
120 oveq2 ⊢ y = B → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B
121 120 oveq1d ⊢ y = B → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
122 121 oveq1d ⊢ y = B → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
123 122 eqeq2d ⊢ y = B → b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s ↔ b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
124 119 123 rexeqbidv ⊢ y = B → ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s ↔ ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
125 124 rexbidv ⊢ y = B → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s ↔ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
126 125 abbidv ⊢ y = B → b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
127 118 126 uneq12d ⊢ y = B → a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s
128 oveq2 ⊢ y = B → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B
129 128 oveq1d ⊢ y = B → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
130 129 oveq1d ⊢ y = B → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
131 130 eqeq2d ⊢ y = B → c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ↔ c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
132 119 131 rexeqbidv ⊢ y = B → ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ↔ ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
133 132 rexbidv ⊢ y = B → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
134 133 abbidv ⊢ y = B → c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u
135 oveq2 ⊢ y = B → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B
136 135 oveq1d ⊢ y = B → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
137 136 oveq1d ⊢ y = B → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
138 137 eqeq2d ⊢ y = B → d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ↔ d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
139 111 138 rexeqbidv ⊢ y = B → ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ↔ ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
140 139 rexbidv ⊢ y = B → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ↔ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
141 140 abbidv ⊢ y = B → d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
142 134 141 uneq12d ⊢ y = B → c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
143 127 142 oveq12d ⊢ y = B → a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
144 143 adantl ⊢ A ∈ No ∧ B ∈ No ∧ y = B → a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
145 110 144 csbied ⊢ A ∈ No ∧ B ∈ No → ⦋ B / y⦌ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w
146 elun1 ⊢ p ∈ L ⁡ A → p ∈ L ⁡ A ∪ R ⁡ A
147 146 ad2antrl ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ∈ L ⁡ A ∪ R ⁡ A
148 elun1 ⊢ p ∈ L ⁡ A ∪ R ⁡ A → p ∈ L ⁡ A ∪ R ⁡ A ∪ A
149 147 148 syl ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ∈ L ⁡ A ∪ R ⁡ A ∪ A
150 snidg ⊢ B ∈ No → B ∈ B
151 150 adantl ⊢ A ∈ No ∧ B ∈ No → B ∈ B
152 elun2 ⊢ B ∈ B → B ∈ L ⁡ B ∪ R ⁡ B ∪ B
153 151 152 syl ⊢ A ∈ No ∧ B ∈ No → B ∈ L ⁡ B ∪ R ⁡ B ∪ B
154 153 adantr ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → B ∈ L ⁡ B ∪ R ⁡ B ∪ B
155 149 154 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p B ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
156 leftirr ⊢ ¬ A ∈ L ⁡ A
157 eleq1 ⊢ p = A → p ∈ L ⁡ A ↔ A ∈ L ⁡ A
158 156 157 mtbiri ⊢ p = A → ¬ p ∈ L ⁡ A
159 158 necon2ai ⊢ p ∈ L ⁡ A → p ≠ A
160 159 ad2antrl ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ≠ A
161 160 orcd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ≠ A ∨ B ≠ B
162 vex ⊢ p ∈ V
163 opthneg ⊢ p ∈ V ∧ B ∈ No → p B ≠ A B ↔ p ≠ A ∨ B ≠ B
164 162 163 mpan ⊢ B ∈ No → p B ≠ A B ↔ p ≠ A ∨ B ≠ B
165 164 ad2antlr ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p B ≠ A B ↔ p ≠ A ∨ B ≠ B
166 161 165 mpbird ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p B ≠ A B
167 opex ⊢ p B ∈ V
168 167 elsn ⊢ p B ∈ A B ↔ p B = A B
169 168 necon3bbii ⊢ ¬ p B ∈ A B ↔ p B ≠ A B
170 166 169 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ¬ p B ∈ A B
171 155 170 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p B ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
172 171 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ p B = ⋅ s ⁡ p B
173 df-ov ⊢ p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ p B
174 df-ov ⊢ p ⋅ s B = ⋅ s ⁡ p B
175 172 173 174 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B = p ⋅ s B
176 snidg ⊢ A ∈ No → A ∈ A
177 176 adantr ⊢ A ∈ No ∧ B ∈ No → A ∈ A
178 elun2 ⊢ A ∈ A → A ∈ L ⁡ A ∪ R ⁡ A ∪ A
179 177 178 syl ⊢ A ∈ No ∧ B ∈ No → A ∈ L ⁡ A ∪ R ⁡ A ∪ A
180 179 adantr ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A ∈ L ⁡ A ∪ R ⁡ A ∪ A
181 elun1 ⊢ q ∈ L ⁡ B → q ∈ L ⁡ B ∪ R ⁡ B
182 181 ad2antll ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → q ∈ L ⁡ B ∪ R ⁡ B
183 elun1 ⊢ q ∈ L ⁡ B ∪ R ⁡ B → q ∈ L ⁡ B ∪ R ⁡ B ∪ B
184 182 183 syl ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → q ∈ L ⁡ B ∪ R ⁡ B ∪ B
185 180 184 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A q ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
186 leftirr ⊢ ¬ B ∈ L ⁡ B
187 eleq1 ⊢ q = B → q ∈ L ⁡ B ↔ B ∈ L ⁡ B
188 186 187 mtbiri ⊢ q = B → ¬ q ∈ L ⁡ B
189 188 necon2ai ⊢ q ∈ L ⁡ B → q ≠ B
190 189 ad2antll ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → q ≠ B
191 190 olcd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A ≠ A ∨ q ≠ B
192 opthneg ⊢ A ∈ No ∧ q ∈ V → A q ≠ A B ↔ A ≠ A ∨ q ≠ B
193 192 elvd ⊢ A ∈ No → A q ≠ A B ↔ A ≠ A ∨ q ≠ B
194 193 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A q ≠ A B ↔ A ≠ A ∨ q ≠ B
195 191 194 mpbird ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A q ≠ A B
196 opex ⊢ A q ∈ V
197 196 elsn ⊢ A q ∈ A B ↔ A q = A B
198 197 necon3bbii ⊢ ¬ A q ∈ A B ↔ A q ≠ A B
199 195 198 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ¬ A q ∈ A B
200 185 199 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A q ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
201 200 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ A q = ⋅ s ⁡ A q
202 df-ov ⊢ A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ A q
203 df-ov ⊢ A ⋅ s q = ⋅ s ⁡ A q
204 201 202 203 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = A ⋅ s q
205 175 204 oveq12d ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = p ⋅ s B + s A ⋅ s q
206 149 184 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p q ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
207 190 olcd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ≠ A ∨ q ≠ B
208 vex ⊢ q ∈ V
209 162 208 opthne ⊢ p q ≠ A B ↔ p ≠ A ∨ q ≠ B
210 207 209 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p q ≠ A B
211 opex ⊢ p q ∈ V
212 211 elsn ⊢ p q ∈ A B ↔ p q = A B
213 212 necon3bbii ⊢ ¬ p q ∈ A B ↔ p q ≠ A B
214 210 213 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ¬ p q ∈ A B
215 206 214 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p q ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
216 215 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ p q = ⋅ s ⁡ p q
217 df-ov ⊢ p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ p q
218 df-ov ⊢ p ⋅ s q = ⋅ s ⁡ p q
219 216 217 218 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = p ⋅ s q
220 205 219 oveq12d ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = p ⋅ s B + s A ⋅ s q - s p ⋅ s q
221 220 eqeq2d ⊢ A ∈ No ∧ B ∈ No ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ↔ a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q
222 221 2rexbidva ⊢ A ∈ No ∧ B ∈ No → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q
223 222 abbidv ⊢ A ∈ No ∧ B ∈ No → a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q
224 elun2 ⊢ r ∈ R ⁡ A → r ∈ L ⁡ A ∪ R ⁡ A
225 224 ad2antrl ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ∈ L ⁡ A ∪ R ⁡ A
226 elun1 ⊢ r ∈ L ⁡ A ∪ R ⁡ A → r ∈ L ⁡ A ∪ R ⁡ A ∪ A
227 225 226 syl ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ∈ L ⁡ A ∪ R ⁡ A ∪ A
228 153 adantr ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → B ∈ L ⁡ B ∪ R ⁡ B ∪ B
229 227 228 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r B ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
230 rightirr ⊢ ¬ A ∈ R ⁡ A
231 eleq1 ⊢ r = A → r ∈ R ⁡ A ↔ A ∈ R ⁡ A
232 230 231 mtbiri ⊢ r = A → ¬ r ∈ R ⁡ A
233 232 necon2ai ⊢ r ∈ R ⁡ A → r ≠ A
234 233 ad2antrl ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ≠ A
235 234 orcd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ≠ A ∨ B ≠ B
236 vex ⊢ r ∈ V
237 opthneg ⊢ r ∈ V ∧ B ∈ No → r B ≠ A B ↔ r ≠ A ∨ B ≠ B
238 236 237 mpan ⊢ B ∈ No → r B ≠ A B ↔ r ≠ A ∨ B ≠ B
239 238 ad2antlr ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r B ≠ A B ↔ r ≠ A ∨ B ≠ B
240 235 239 mpbird ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r B ≠ A B
241 opex ⊢ r B ∈ V
242 241 elsn ⊢ r B ∈ A B ↔ r B = A B
243 242 necon3bbii ⊢ ¬ r B ∈ A B ↔ r B ≠ A B
244 240 243 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ¬ r B ∈ A B
245 229 244 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r B ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
246 245 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ r B = ⋅ s ⁡ r B
247 df-ov ⊢ r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ r B
248 df-ov ⊢ r ⋅ s B = ⋅ s ⁡ r B
249 246 247 248 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B = r ⋅ s B
250 179 adantr ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A ∈ L ⁡ A ∪ R ⁡ A ∪ A
251 elun2 ⊢ s ∈ R ⁡ B → s ∈ L ⁡ B ∪ R ⁡ B
252 251 ad2antll ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → s ∈ L ⁡ B ∪ R ⁡ B
253 elun1 ⊢ s ∈ L ⁡ B ∪ R ⁡ B → s ∈ L ⁡ B ∪ R ⁡ B ∪ B
254 252 253 syl ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → s ∈ L ⁡ B ∪ R ⁡ B ∪ B
255 250 254 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A s ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
256 rightirr ⊢ ¬ B ∈ R ⁡ B
257 eleq1 ⊢ s = B → s ∈ R ⁡ B ↔ B ∈ R ⁡ B
258 256 257 mtbiri ⊢ s = B → ¬ s ∈ R ⁡ B
259 258 necon2ai ⊢ s ∈ R ⁡ B → s ≠ B
260 259 ad2antll ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → s ≠ B
261 260 olcd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A ≠ A ∨ s ≠ B
262 opthneg ⊢ A ∈ No ∧ s ∈ V → A s ≠ A B ↔ A ≠ A ∨ s ≠ B
263 262 elvd ⊢ A ∈ No → A s ≠ A B ↔ A ≠ A ∨ s ≠ B
264 263 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A s ≠ A B ↔ A ≠ A ∨ s ≠ B
265 261 264 mpbird ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A s ≠ A B
266 opex ⊢ A s ∈ V
267 266 elsn ⊢ A s ∈ A B ↔ A s = A B
268 267 necon3bbii ⊢ ¬ A s ∈ A B ↔ A s ≠ A B
269 265 268 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ¬ A s ∈ A B
270 255 269 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A s ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
271 270 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ A s = ⋅ s ⁡ A s
272 df-ov ⊢ A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ A s
273 df-ov ⊢ A ⋅ s s = ⋅ s ⁡ A s
274 271 272 273 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = A ⋅ s s
275 249 274 oveq12d ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = r ⋅ s B + s A ⋅ s s
276 227 254 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r s ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
277 260 olcd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ≠ A ∨ s ≠ B
278 vex ⊢ s ∈ V
279 236 278 opthne ⊢ r s ≠ A B ↔ r ≠ A ∨ s ≠ B
280 277 279 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r s ≠ A B
281 opex ⊢ r s ∈ V
282 281 elsn ⊢ r s ∈ A B ↔ r s = A B
283 282 necon3bbii ⊢ ¬ r s ∈ A B ↔ r s ≠ A B
284 280 283 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ¬ r s ∈ A B
285 276 284 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r s ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
286 285 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ r s = ⋅ s ⁡ r s
287 df-ov ⊢ r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ r s
288 df-ov ⊢ r ⋅ s s = ⋅ s ⁡ r s
289 286 287 288 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = r ⋅ s s
290 275 289 oveq12d ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
291 290 eqeq2d ⊢ A ∈ No ∧ B ∈ No ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s ↔ b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
292 291 2rexbidva ⊢ A ∈ No ∧ B ∈ No → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s ↔ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
293 292 abbidv ⊢ A ∈ No ∧ B ∈ No → b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
294 223 293 uneq12d ⊢ A ∈ No ∧ B ∈ No → a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
295 elun1 ⊢ t ∈ L ⁡ A → t ∈ L ⁡ A ∪ R ⁡ A
296 295 ad2antrl ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ L ⁡ A ∪ R ⁡ A
297 elun1 ⊢ t ∈ L ⁡ A ∪ R ⁡ A → t ∈ L ⁡ A ∪ R ⁡ A ∪ A
298 296 297 syl ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ L ⁡ A ∪ R ⁡ A ∪ A
299 153 adantr ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → B ∈ L ⁡ B ∪ R ⁡ B ∪ B
300 298 299 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t B ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
301 eleq1 ⊢ t = A → t ∈ L ⁡ A ↔ A ∈ L ⁡ A
302 156 301 mtbiri ⊢ t = A → ¬ t ∈ L ⁡ A
303 302 necon2ai ⊢ t ∈ L ⁡ A → t ≠ A
304 303 ad2antrl ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ≠ A
305 304 orcd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ≠ A ∨ B ≠ B
306 vex ⊢ t ∈ V
307 opthneg ⊢ t ∈ V ∧ B ∈ No → t B ≠ A B ↔ t ≠ A ∨ B ≠ B
308 306 307 mpan ⊢ B ∈ No → t B ≠ A B ↔ t ≠ A ∨ B ≠ B
309 308 ad2antlr ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t B ≠ A B ↔ t ≠ A ∨ B ≠ B
310 305 309 mpbird ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t B ≠ A B
311 opex ⊢ t B ∈ V
312 311 elsn ⊢ t B ∈ A B ↔ t B = A B
313 312 necon3bbii ⊢ ¬ t B ∈ A B ↔ t B ≠ A B
314 310 313 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ¬ t B ∈ A B
315 300 314 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t B ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
316 315 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ t B = ⋅ s ⁡ t B
317 df-ov ⊢ t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ t B
318 df-ov ⊢ t ⋅ s B = ⋅ s ⁡ t B
319 316 317 318 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B = t ⋅ s B
320 179 adantr ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ∈ L ⁡ A ∪ R ⁡ A ∪ A
321 elun2 ⊢ u ∈ R ⁡ B → u ∈ L ⁡ B ∪ R ⁡ B
322 321 ad2antll ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ L ⁡ B ∪ R ⁡ B
323 elun1 ⊢ u ∈ L ⁡ B ∪ R ⁡ B → u ∈ L ⁡ B ∪ R ⁡ B ∪ B
324 322 323 syl ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ L ⁡ B ∪ R ⁡ B ∪ B
325 320 324 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A u ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
326 eleq1 ⊢ u = B → u ∈ R ⁡ B ↔ B ∈ R ⁡ B
327 256 326 mtbiri ⊢ u = B → ¬ u ∈ R ⁡ B
328 327 necon2ai ⊢ u ∈ R ⁡ B → u ≠ B
329 328 ad2antll ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ≠ B
330 329 olcd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ≠ A ∨ u ≠ B
331 opthneg ⊢ A ∈ No ∧ u ∈ V → A u ≠ A B ↔ A ≠ A ∨ u ≠ B
332 331 elvd ⊢ A ∈ No → A u ≠ A B ↔ A ≠ A ∨ u ≠ B
333 332 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A u ≠ A B ↔ A ≠ A ∨ u ≠ B
334 330 333 mpbird ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A u ≠ A B
335 opex ⊢ A u ∈ V
336 335 elsn ⊢ A u ∈ A B ↔ A u = A B
337 336 necon3bbii ⊢ ¬ A u ∈ A B ↔ A u ≠ A B
338 334 337 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ¬ A u ∈ A B
339 325 338 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A u ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
340 339 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ A u = ⋅ s ⁡ A u
341 df-ov ⊢ A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ A u
342 df-ov ⊢ A ⋅ s u = ⋅ s ⁡ A u
343 340 341 342 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = A ⋅ s u
344 319 343 oveq12d ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = t ⋅ s B + s A ⋅ s u
345 298 324 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t u ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
346 329 olcd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ≠ A ∨ u ≠ B
347 vex ⊢ u ∈ V
348 306 347 opthne ⊢ t u ≠ A B ↔ t ≠ A ∨ u ≠ B
349 346 348 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t u ≠ A B
350 opex ⊢ t u ∈ V
351 350 elsn ⊢ t u ∈ A B ↔ t u = A B
352 351 necon3bbii ⊢ ¬ t u ∈ A B ↔ t u ≠ A B
353 349 352 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ¬ t u ∈ A B
354 345 353 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t u ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
355 354 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ t u = ⋅ s ⁡ t u
356 df-ov ⊢ t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ t u
357 df-ov ⊢ t ⋅ s u = ⋅ s ⁡ t u
358 355 356 357 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = t ⋅ s u
359 344 358 oveq12d ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = t ⋅ s B + s A ⋅ s u - s t ⋅ s u
360 359 eqeq2d ⊢ A ∈ No ∧ B ∈ No ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ↔ c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u
361 360 2rexbidva ⊢ A ∈ No ∧ B ∈ No → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u
362 361 abbidv ⊢ A ∈ No ∧ B ∈ No → c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u = c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u
363 elun2 ⊢ v ∈ R ⁡ A → v ∈ L ⁡ A ∪ R ⁡ A
364 363 ad2antrl ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ L ⁡ A ∪ R ⁡ A
365 elun1 ⊢ v ∈ L ⁡ A ∪ R ⁡ A → v ∈ L ⁡ A ∪ R ⁡ A ∪ A
366 364 365 syl ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ L ⁡ A ∪ R ⁡ A ∪ A
367 153 adantr ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → B ∈ L ⁡ B ∪ R ⁡ B ∪ B
368 366 367 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v B ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
369 eleq1 ⊢ v = A → v ∈ R ⁡ A ↔ A ∈ R ⁡ A
370 230 369 mtbiri ⊢ v = A → ¬ v ∈ R ⁡ A
371 370 necon2ai ⊢ v ∈ R ⁡ A → v ≠ A
372 371 ad2antrl ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ≠ A
373 372 orcd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ≠ A ∨ B ≠ B
374 vex ⊢ v ∈ V
375 opthneg ⊢ v ∈ V ∧ B ∈ No → v B ≠ A B ↔ v ≠ A ∨ B ≠ B
376 374 375 mpan ⊢ B ∈ No → v B ≠ A B ↔ v ≠ A ∨ B ≠ B
377 376 ad2antlr ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v B ≠ A B ↔ v ≠ A ∨ B ≠ B
378 373 377 mpbird ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v B ≠ A B
379 opex ⊢ v B ∈ V
380 379 elsn ⊢ v B ∈ A B ↔ v B = A B
381 380 necon3bbii ⊢ ¬ v B ∈ A B ↔ v B ≠ A B
382 378 381 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ¬ v B ∈ A B
383 368 382 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v B ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
384 383 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ v B = ⋅ s ⁡ v B
385 df-ov ⊢ v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ v B
386 df-ov ⊢ v ⋅ s B = ⋅ s ⁡ v B
387 384 385 386 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B = v ⋅ s B
388 179 adantr ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ∈ L ⁡ A ∪ R ⁡ A ∪ A
389 elun1 ⊢ w ∈ L ⁡ B → w ∈ L ⁡ B ∪ R ⁡ B
390 389 ad2antll ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ L ⁡ B ∪ R ⁡ B
391 elun1 ⊢ w ∈ L ⁡ B ∪ R ⁡ B → w ∈ L ⁡ B ∪ R ⁡ B ∪ B
392 390 391 syl ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ L ⁡ B ∪ R ⁡ B ∪ B
393 388 392 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A w ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
394 eleq1 ⊢ w = B → w ∈ L ⁡ B ↔ B ∈ L ⁡ B
395 186 394 mtbiri ⊢ w = B → ¬ w ∈ L ⁡ B
396 395 necon2ai ⊢ w ∈ L ⁡ B → w ≠ B
397 396 ad2antll ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ≠ B
398 397 olcd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ≠ A ∨ w ≠ B
399 opthneg ⊢ A ∈ No ∧ w ∈ V → A w ≠ A B ↔ A ≠ A ∨ w ≠ B
400 399 elvd ⊢ A ∈ No → A w ≠ A B ↔ A ≠ A ∨ w ≠ B
401 400 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A w ≠ A B ↔ A ≠ A ∨ w ≠ B
402 398 401 mpbird ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A w ≠ A B
403 opex ⊢ A w ∈ V
404 403 elsn ⊢ A w ∈ A B ↔ A w = A B
405 404 necon3bbii ⊢ ¬ A w ∈ A B ↔ A w ≠ A B
406 402 405 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ¬ A w ∈ A B
407 393 406 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A w ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
408 407 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ A w = ⋅ s ⁡ A w
409 df-ov ⊢ A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ A w
410 df-ov ⊢ A ⋅ s w = ⋅ s ⁡ A w
411 408 409 410 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = A ⋅ s w
412 387 411 oveq12d ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = v ⋅ s B + s A ⋅ s w
413 366 392 opelxpd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v w ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
414 397 olcd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ≠ A ∨ w ≠ B
415 vex ⊢ w ∈ V
416 374 415 opthne ⊢ v w ≠ A B ↔ v ≠ A ∨ w ≠ B
417 414 416 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v w ≠ A B
418 opex ⊢ v w ∈ V
419 418 elsn ⊢ v w ∈ A B ↔ v w = A B
420 419 necon3bbii ⊢ ¬ v w ∈ A B ↔ v w ≠ A B
421 417 420 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ¬ v w ∈ A B
422 413 421 eldifd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v w ∈ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
423 422 fvresd ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ v w = ⋅ s ⁡ v w
424 df-ov ⊢ v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B ⁡ v w
425 df-ov ⊢ v ⋅ s w = ⋅ s ⁡ v w
426 423 424 425 3eqtr4g ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = v ⋅ s w
427 412 426 oveq12d ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
428 427 eqeq2d ⊢ A ∈ No ∧ B ∈ No ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ↔ d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
429 428 2rexbidva ⊢ A ∈ No ∧ B ∈ No → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w ↔ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
430 429 abbidv ⊢ A ∈ No ∧ B ∈ No → d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
431 362 430 uneq12d ⊢ A ∈ No ∧ B ∈ No → c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
432 294 431 oveq12d ⊢ A ∈ No ∧ B ∈ No → a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B B + s A ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
433 109 145 432 3eqtrd ⊢ A ∈ No ∧ B ∈ No → ⦋ A / x⦌ ⦋ B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
434 69 72 433 3eqtrd ⊢ A ∈ No ∧ B ∈ No → ⦋ 1 st ⁡ A B / x⦌ ⦋ 2 nd ⁡ A B / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q - s p ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s - s r ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u - s t ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B y + s x ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w - s v ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B w = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
435 67 434 eqtrid ⊢ A ∈ No ∧ B ∈ No → A B z ∈ V , m ∈ V ⟼ ⦋ 1 st ⁡ z / x⦌ ⦋ 2 nd ⁡ z / y⦌ a | ∃ p ∈ L ⁡ x ∃ q ∈ L ⁡ y a = p m y + s x m q - s p m q ∪ b | ∃ r ∈ R ⁡ x ∃ s ∈ R ⁡ y b = r m y + s x m s - s r m s | s c | ∃ t ∈ L ⁡ x ∃ u ∈ R ⁡ y c = t m y + s x m u - s t m u ∪ d | ∃ v ∈ R ⁡ x ∃ w ∈ L ⁡ y d = v m y + s x m w - s v m w ⋅ s ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
436 2 435 eqtrd ⊢ A ∈ No ∧ B ∈ No → A ⋅ s B = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w