Metamath Proof Explorer


Theorem rlocaddval

Description: Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses rlocaddval.1 ⊢ B = Base R
rlocaddval.2 ⊢ · ˙ = ⋅ R
rlocaddval.3 ⊢ + ˙ = + R
rlocaddval.4 ⊢ L = R RLocal S
rlocaddval.5 ⊢ ∼ ˙ = R ~RL S
rlocaddval.r ⊢ φ → R ∈ CRing
rlocaddval.s ⊢ φ → S ∈ SubMnd ⁡ mulGrp R
rlocaddval.6 ⊢ φ → E ∈ B
rlocaddval.7 ⊢ φ → F ∈ B
rlocaddval.8 ⊢ φ → G ∈ S
rlocaddval.9 ⊢ φ → H ∈ S
rlocaddval.10 ⊢ ⊕ ˙ = + L
Assertion rlocaddval ⊢ φ → E G ∼ ˙ ⊕ ˙ F H ∼ ˙ = E · ˙ H + ˙ F · ˙ G G · ˙ H ∼ ˙

Proof

Step Hyp Ref Expression
1 rlocaddval.1 ⊢ B = Base R
2 rlocaddval.2 ⊢ · ˙ = ⋅ R
3 rlocaddval.3 ⊢ + ˙ = + R
4 rlocaddval.4 ⊢ L = R RLocal S
5 rlocaddval.5 ⊢ ∼ ˙ = R ~RL S
6 rlocaddval.r ⊢ φ → R ∈ CRing
7 rlocaddval.s ⊢ φ → S ∈ SubMnd ⁡ mulGrp R
8 rlocaddval.6 ⊢ φ → E ∈ B
9 rlocaddval.7 ⊢ φ → F ∈ B
10 rlocaddval.8 ⊢ φ → G ∈ S
11 rlocaddval.9 ⊢ φ → H ∈ S
12 rlocaddval.10 ⊢ ⊕ ˙ = + L
13 8 10 opelxpd ⊢ φ → E G ∈ B × S
14 9 11 opelxpd ⊢ φ → F H ∈ B × S
15 eqid ⊢ 0 R = 0 R
16 eqid ⊢ - R = - R
17 eqid ⊢ ≤ R = ≤ R
18 eqid ⊢ Scalar ⁡ R = Scalar ⁡ R
19 eqid ⊢ Base Scalar ⁡ R = Base Scalar ⁡ R
20 eqid ⊢ ⋅ R = ⋅ R
21 eqid ⊢ B × S = B × S
22 eqid ⊢ TopSet ⁡ R = TopSet ⁡ R
23 eqid ⊢ dist ⁡ R = dist ⁡ R
24 eqid ⊢ a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b = a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b
25 eqid ⊢ a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b = a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b
26 eqid ⊢ k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a = k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a
27 eqid ⊢ a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a = a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a
28 eqid ⊢ a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a = a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
29 eqid ⊢ mulGrp R = mulGrp R
30 29 1 mgpbas ⊢ B = Base mulGrp R
31 30 submss ⊢ S ∈ SubMnd ⁡ mulGrp R → S ⊆ B
32 7 31 syl ⊢ φ → S ⊆ B
33 1 15 2 16 3 17 18 19 20 21 5 22 23 24 25 26 27 28 6 32 rlocval ⊢ φ → R RLocal S = Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a / 𝑠 ∼ ˙
34 4 33 eqtrid ⊢ φ → L = Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a / 𝑠 ∼ ˙
35 eqidd ⊢ φ → Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a = Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
36 eqid ⊢ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a = Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
37 36 imasvalstr ⊢ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a Struct 1 12
38 baseid ⊢ Base = Slot Base ndx
39 snsstp1 ⊢ Base ndx B × S ⊆ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b
40 ssun1 ⊢ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ⊆ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅
41 ssun1 ⊢ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ⊆ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
42 40 41 sstri ⊢ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ⊆ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
43 39 42 sstri ⊢ Base ndx B × S ⊆ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
44 1 fvexi ⊢ B ∈ V
45 44 a1i ⊢ φ → B ∈ V
46 45 7 xpexd ⊢ φ → B × S ∈ V
47 eqid ⊢ Base Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a = Base Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
48 35 37 38 43 46 47 strfv3 ⊢ φ → Base Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a = B × S
49 48 eqcomd ⊢ φ → B × S = Base Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
50 eqid ⊢ 1 R = 1 R
51 1 15 50 2 16 21 5 6 7 erler ⊢ φ → ∼ ˙ Er B × S
52 tpex ⊢ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∈ V
53 tpex ⊢ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∈ V
54 52 53 unex ⊢ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∈ V
55 tpex ⊢ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a ∈ V
56 54 55 unex ⊢ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a ∈ V
57 56 a1i ⊢ φ → Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a ∈ V
58 32 ad2antrr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → S ⊆ B
59 58 ad2antrr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R → S ⊆ B
60 59 ad2antrr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → S ⊆ B
61 eqidd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v = 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v
62 eqidd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q = 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
63 6 crnggrpd ⊢ φ → R ∈ Grp
64 63 ad6antr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → R ∈ Grp
65 6 crngringd ⊢ φ → R ∈ Ring
66 65 ad6antr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → R ∈ Ring
67 simplr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → u ∼ ˙ p
68 1 5 58 67 erlcl1 ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → u ∈ B × S
69 68 ad4antr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → u ∈ B × S
70 xp1st ⊢ u ∈ B × S → 1 st ⁡ u ∈ B
71 69 70 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u ∈ B
72 simpr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → v ∼ ˙ q
73 1 5 58 72 erlcl1 ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → v ∈ B × S
74 73 ad4antr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → v ∈ B × S
75 xp2nd ⊢ v ∈ B × S → 2 nd ⁡ v ∈ S
76 74 75 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ v ∈ S
77 60 76 sseldd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ v ∈ B
78 1 2 66 71 77 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v ∈ B
79 xp1st ⊢ v ∈ B × S → 1 st ⁡ v ∈ B
80 74 79 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ v ∈ B
81 xp2nd ⊢ u ∈ B × S → 2 nd ⁡ u ∈ S
82 69 81 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ u ∈ S
83 60 82 sseldd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ u ∈ B
84 1 2 66 80 83 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ v · ˙ 2 nd ⁡ u ∈ B
85 1 3 64 78 84 grpcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u ∈ B
86 1 5 58 67 erlcl2 ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → p ∈ B × S
87 86 ad4antr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → p ∈ B × S
88 xp1st ⊢ p ∈ B × S → 1 st ⁡ p ∈ B
89 87 88 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ p ∈ B
90 1 5 58 72 erlcl2 ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → q ∈ B × S
91 90 ad4antr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → q ∈ B × S
92 xp2nd ⊢ q ∈ B × S → 2 nd ⁡ q ∈ S
93 91 92 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ q ∈ S
94 60 93 sseldd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ q ∈ B
95 1 2 66 89 94 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ p · ˙ 2 nd ⁡ q ∈ B
96 xp1st ⊢ q ∈ B × S → 1 st ⁡ q ∈ B
97 91 96 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ q ∈ B
98 xp2nd ⊢ p ∈ B × S → 2 nd ⁡ p ∈ S
99 87 98 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ p ∈ S
100 60 99 sseldd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ p ∈ B
101 1 2 66 97 100 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ q · ˙ 2 nd ⁡ p ∈ B
102 1 3 64 95 101 grpcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p ∈ B
103 7 ad6antr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → S ∈ SubMnd ⁡ mulGrp R
104 29 2 mgpplusg ⊢ · ˙ = + mulGrp R
105 104 submcl ⊢ S ∈ SubMnd ⁡ mulGrp R ∧ 2 nd ⁡ u ∈ S ∧ 2 nd ⁡ v ∈ S → 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ S
106 103 82 76 105 syl3anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ S
107 104 submcl ⊢ S ∈ SubMnd ⁡ mulGrp R ∧ 2 nd ⁡ p ∈ S ∧ 2 nd ⁡ q ∈ S → 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ S
108 103 99 93 107 syl3anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ S
109 simp-4r ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f ∈ S
110 simplr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g ∈ S
111 104 submcl ⊢ S ∈ SubMnd ⁡ mulGrp R ∧ f ∈ S ∧ g ∈ S → f · ˙ g ∈ S
112 103 109 110 111 syl3anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g ∈ S
113 60 108 sseldd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B
114 1 3 2 ringdir ⊢ R ∈ Ring ∧ 1 st ⁡ u · ˙ 2 nd ⁡ v ∈ B ∧ 1 st ⁡ v · ˙ 2 nd ⁡ u ∈ B ∧ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q = 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q
115 66 78 84 113 114 syl13anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q = 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q
116 60 106 sseldd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B
117 1 3 2 ringdir ⊢ R ∈ Ring ∧ 1 st ⁡ p · ˙ 2 nd ⁡ q ∈ B ∧ 1 st ⁡ q · ˙ 2 nd ⁡ p ∈ B ∧ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B → 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
118 66 95 101 116 117 syl13anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
119 115 118 oveq12d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
120 119 oveq2d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
121 60 109 sseldd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f ∈ B
122 60 110 sseldd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g ∈ B
123 1 2 66 121 122 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g ∈ B
124 1 2 66 78 113 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B
125 1 2 66 84 113 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B
126 1 3 64 124 125 grpcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B
127 1 2 66 95 116 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B
128 1 2 66 101 116 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B
129 1 3 64 127 128 grpcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B
130 1 2 16 66 123 126 129 ringsubdi ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
131 1 3 2 ringdi ⊢ R ∈ Ring ∧ f · ˙ g ∈ B ∧ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B ∧ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q = f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q
132 66 123 124 125 131 syl13anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q = f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q
133 1 3 2 ringdi ⊢ R ∈ Ring ∧ f · ˙ g ∈ B ∧ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B ∧ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B → f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
134 66 123 127 128 133 syl13anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
135 132 134 oveq12d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
136 66 ringabld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → R ∈ Abel
137 1 2 66 123 124 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B
138 1 2 66 123 125 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B
139 1 2 66 123 127 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B
140 1 2 66 123 128 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B
141 1 3 16 ablsub4 ⊢ R ∈ Abel ∧ f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B ∧ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B ∧ f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B ∧ f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ B → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
142 136 137 138 139 140 141 syl122anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v
143 29 crngmgp ⊢ R ∈ CRing → mulGrp R ∈ CMnd
144 6 143 syl ⊢ φ → mulGrp R ∈ CMnd
145 144 ad6antr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → mulGrp R ∈ CMnd
146 30 104 145 121 122 71 77 100 94 cmn246135 ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q = g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p
147 30 104 145 121 122 89 94 83 77 cmn246135 ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = g · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ v · ˙ f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u
148 30 104 cmncom ⊢ mulGrp R ∈ CMnd ∧ 2 nd ⁡ v ∈ B ∧ 2 nd ⁡ q ∈ B → 2 nd ⁡ v · ˙ 2 nd ⁡ q = 2 nd ⁡ q · ˙ 2 nd ⁡ v
149 145 77 94 148 syl3anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ v · ˙ 2 nd ⁡ q = 2 nd ⁡ q · ˙ 2 nd ⁡ v
150 149 oveq2d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q = g · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ v
151 150 oveq1d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u = g · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ v · ˙ f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u
152 147 151 eqtr4d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u
153 146 152 oveq12d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u
154 1 2 66 71 100 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ p ∈ B
155 1 2 66 89 83 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ p · ˙ 2 nd ⁡ u ∈ B
156 1 2 16 66 121 154 155 ringsubdi ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u
157 simpllr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R
158 156 157 eqtr3d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R
159 158 oveq2d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u = g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ 0 R
160 1 2 66 77 94 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ v · ˙ 2 nd ⁡ q ∈ B
161 1 2 66 122 160 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q ∈ B
162 1 2 66 121 154 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p ∈ B
163 1 2 66 121 155 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u ∈ B
164 1 2 16 66 161 162 163 ringsubdi ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u = g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u
165 1 2 15 66 161 ringrzd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ 0 R = 0 R
166 159 164 165 3eqtr3d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R g · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ q · ˙ f · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R
167 153 166 eqtrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 0 R
168 30 104 145 121 122 80 83 100 94 cmn145236 ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q = f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q
169 30 104 145 121 122 97 100 83 77 cmn145236 ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v
170 30 104 cmncom ⊢ mulGrp R ∈ CMnd ∧ 2 nd ⁡ p ∈ B ∧ 2 nd ⁡ u ∈ B → 2 nd ⁡ p · ˙ 2 nd ⁡ u = 2 nd ⁡ u · ˙ 2 nd ⁡ p
171 145 100 83 170 syl3anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ p · ˙ 2 nd ⁡ u = 2 nd ⁡ u · ˙ 2 nd ⁡ p
172 171 oveq2d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u = f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p
173 172 oveq1d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v = f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v
174 169 173 eqtrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v
175 168 174 oveq12d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v
176 1 2 66 80 94 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ v · ˙ 2 nd ⁡ q ∈ B
177 1 2 66 97 77 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ q · ˙ 2 nd ⁡ v ∈ B
178 1 2 16 66 122 176 177 ringsubdi ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v
179 simpr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R
180 178 179 eqtr3d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R
181 180 oveq2d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v = f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 0 R
182 1 2 66 83 100 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 2 nd ⁡ u · ˙ 2 nd ⁡ p ∈ B
183 1 2 66 121 182 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p ∈ B
184 1 2 66 122 176 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q ∈ B
185 1 2 66 122 177 ringcld ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v ∈ B
186 1 2 16 66 183 184 185 ringsubdi ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v = f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v
187 1 2 15 66 183 ringrzd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 0 R = 0 R
188 181 186 187 3eqtr3d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R f · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R
189 175 188 eqtrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 0 R
190 167 189 oveq12d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 0 R + ˙ 0 R
191 1 15 grpidcl ⊢ R ∈ Grp → 0 R ∈ B
192 64 191 syl ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 0 R ∈ B
193 1 3 15 64 192 grplidd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 0 R + ˙ 0 R = 0 R
194 190 193 eqtrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ f · ˙ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 0 R
195 135 142 194 3eqtrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R f · ˙ g · ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 0 R
196 120 130 195 3eqtrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → f · ˙ g · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ q - R 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p · ˙ 2 nd ⁡ u · ˙ 2 nd ⁡ v = 0 R
197 1 5 60 15 2 16 61 62 85 102 106 108 112 196 erlbrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R ∧ g ∈ S ∧ g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v ∼ ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
198 72 ad2antrr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R → v ∼ ˙ q
199 1 5 59 15 2 16 198 erldi ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R → ∃ g ∈ S g · ˙ 1 st ⁡ v · ˙ 2 nd ⁡ q - R 1 st ⁡ q · ˙ 2 nd ⁡ v = 0 R
200 197 199 r19.29a ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q ∧ f ∈ S ∧ f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v ∼ ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
201 1 5 58 15 2 16 67 erldi ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → ∃ f ∈ S f · ˙ 1 st ⁡ u · ˙ 2 nd ⁡ p - R 1 st ⁡ p · ˙ 2 nd ⁡ u = 0 R
202 200 201 r19.29a ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v ∼ ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
203 plusgid ⊢ + 𝑔 = Slot + ndx
204 snsstp2 ⊢ + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⊆ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b
205 204 42 sstri ⊢ + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⊆ Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
206 24 mpoexg ⊢ B × S ∈ V ∧ B × S ∈ V → a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ∈ V
207 46 46 206 syl2anc ⊢ φ → a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ∈ V
208 eqid ⊢ + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a = + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a
209 35 37 203 205 207 208 strfv3 ⊢ φ → + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a = a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b
210 209 ad2antrr ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a = a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b
211 210 oveqd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → u + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a v = u a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b v
212 opex ⊢ 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ V
213 212 a1i ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ V
214 simpl ⊢ a = u ∧ b = v → a = u
215 214 fveq2d ⊢ a = u ∧ b = v → 1 st ⁡ a = 1 st ⁡ u
216 simpr ⊢ a = u ∧ b = v → b = v
217 216 fveq2d ⊢ a = u ∧ b = v → 2 nd ⁡ b = 2 nd ⁡ v
218 215 217 oveq12d ⊢ a = u ∧ b = v → 1 st ⁡ a · ˙ 2 nd ⁡ b = 1 st ⁡ u · ˙ 2 nd ⁡ v
219 216 fveq2d ⊢ a = u ∧ b = v → 1 st ⁡ b = 1 st ⁡ v
220 214 fveq2d ⊢ a = u ∧ b = v → 2 nd ⁡ a = 2 nd ⁡ u
221 219 220 oveq12d ⊢ a = u ∧ b = v → 1 st ⁡ b · ˙ 2 nd ⁡ a = 1 st ⁡ v · ˙ 2 nd ⁡ u
222 218 221 oveq12d ⊢ a = u ∧ b = v → 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a = 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u
223 220 217 oveq12d ⊢ a = u ∧ b = v → 2 nd ⁡ a · ˙ 2 nd ⁡ b = 2 nd ⁡ u · ˙ 2 nd ⁡ v
224 222 223 opeq12d ⊢ a = u ∧ b = v → 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b = 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v
225 224 24 ovmpoga ⊢ u ∈ B × S ∧ v ∈ B × S ∧ 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v ∈ V → u a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b v = 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v
226 68 73 213 225 syl3anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → u a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b v = 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v
227 211 226 eqtrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → u + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a v = 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v
228 210 oveqd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q = p a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b q
229 opex ⊢ 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ V
230 229 a1i ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ V
231 simpl ⊢ a = p ∧ b = q → a = p
232 231 fveq2d ⊢ a = p ∧ b = q → 1 st ⁡ a = 1 st ⁡ p
233 simpr ⊢ a = p ∧ b = q → b = q
234 233 fveq2d ⊢ a = p ∧ b = q → 2 nd ⁡ b = 2 nd ⁡ q
235 232 234 oveq12d ⊢ a = p ∧ b = q → 1 st ⁡ a · ˙ 2 nd ⁡ b = 1 st ⁡ p · ˙ 2 nd ⁡ q
236 233 fveq2d ⊢ a = p ∧ b = q → 1 st ⁡ b = 1 st ⁡ q
237 231 fveq2d ⊢ a = p ∧ b = q → 2 nd ⁡ a = 2 nd ⁡ p
238 236 237 oveq12d ⊢ a = p ∧ b = q → 1 st ⁡ b · ˙ 2 nd ⁡ a = 1 st ⁡ q · ˙ 2 nd ⁡ p
239 235 238 oveq12d ⊢ a = p ∧ b = q → 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a = 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p
240 237 234 oveq12d ⊢ a = p ∧ b = q → 2 nd ⁡ a · ˙ 2 nd ⁡ b = 2 nd ⁡ p · ˙ 2 nd ⁡ q
241 239 240 opeq12d ⊢ a = p ∧ b = q → 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b = 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
242 241 24 ovmpoga ⊢ p ∈ B × S ∧ q ∈ B × S ∧ 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ V → p a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b q = 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
243 86 90 230 242 syl3anc ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → p a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b q = 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
244 228 243 eqtrd ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q = 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
245 227 244 breq12d ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → u + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a v ∼ ˙ p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q ↔ 1 st ⁡ u · ˙ 2 nd ⁡ v + ˙ 1 st ⁡ v · ˙ 2 nd ⁡ u 2 nd ⁡ u · ˙ 2 nd ⁡ v ∼ ˙ 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
246 202 245 mpbird ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → u + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a v ∼ ˙ p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q
247 246 anasss ⊢ φ ∧ u ∼ ˙ p ∧ v ∼ ˙ q → u + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a v ∼ ˙ p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q
248 247 ex ⊢ φ → u ∼ ˙ p ∧ v ∼ ˙ q → u + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a v ∼ ˙ p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q
249 209 oveqd ⊢ φ → p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q = p a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b q
250 249 ad2antrr ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q = p a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b q
251 simplr ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → p ∈ B × S
252 simpr ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → q ∈ B × S
253 229 a1i ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ V
254 251 252 253 242 syl3anc ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → p a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b q = 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q
255 63 ad2antrr ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → R ∈ Grp
256 65 ad2antrr ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → R ∈ Ring
257 251 88 syl ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 1 st ⁡ p ∈ B
258 32 ad2antrr ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → S ⊆ B
259 252 92 syl ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 2 nd ⁡ q ∈ S
260 258 259 sseldd ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 2 nd ⁡ q ∈ B
261 1 2 256 257 260 ringcld ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 1 st ⁡ p · ˙ 2 nd ⁡ q ∈ B
262 252 96 syl ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 1 st ⁡ q ∈ B
263 251 98 syl ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 2 nd ⁡ p ∈ S
264 258 263 sseldd ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 2 nd ⁡ p ∈ B
265 1 2 256 262 264 ringcld ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 1 st ⁡ q · ˙ 2 nd ⁡ p ∈ B
266 1 3 255 261 265 grpcld ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p ∈ B
267 7 ad2antrr ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → S ∈ SubMnd ⁡ mulGrp R
268 267 263 259 107 syl3anc ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ S
269 266 268 opelxpd ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → 1 st ⁡ p · ˙ 2 nd ⁡ q + ˙ 1 st ⁡ q · ˙ 2 nd ⁡ p 2 nd ⁡ p · ˙ 2 nd ⁡ q ∈ B × S
270 254 269 eqeltrd ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → p a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b q ∈ B × S
271 250 270 eqeltrd ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q ∈ B × S
272 271 anasss ⊢ φ ∧ p ∈ B × S ∧ q ∈ B × S → p + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a q ∈ B × S
273 34 49 51 57 248 272 208 12 qusaddval ⊢ φ ∧ E G ∈ B × S ∧ F H ∈ B × S → E G ∼ ˙ ⊕ ˙ F H ∼ ˙ = E G + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a F H ∼ ˙
274 13 14 273 mpd3an23 ⊢ φ → E G ∼ ˙ ⊕ ˙ F H ∼ ˙ = E G + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a F H ∼ ˙
275 209 oveqd ⊢ φ → E G + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a F H = E G a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b F H
276 24 a1i ⊢ φ → a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b = a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b
277 simprl ⊢ φ ∧ a = E G ∧ b = F H → a = E G
278 277 fveq2d ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ a = 1 st ⁡ E G
279 8 adantr ⊢ φ ∧ a = E G ∧ b = F H → E ∈ B
280 10 adantr ⊢ φ ∧ a = E G ∧ b = F H → G ∈ S
281 op1stg ⊢ E ∈ B ∧ G ∈ S → 1 st ⁡ E G = E
282 279 280 281 syl2anc ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ E G = E
283 278 282 eqtrd ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ a = E
284 simprr ⊢ φ ∧ a = E G ∧ b = F H → b = F H
285 284 fveq2d ⊢ φ ∧ a = E G ∧ b = F H → 2 nd ⁡ b = 2 nd ⁡ F H
286 9 adantr ⊢ φ ∧ a = E G ∧ b = F H → F ∈ B
287 11 adantr ⊢ φ ∧ a = E G ∧ b = F H → H ∈ S
288 op2ndg ⊢ F ∈ B ∧ H ∈ S → 2 nd ⁡ F H = H
289 286 287 288 syl2anc ⊢ φ ∧ a = E G ∧ b = F H → 2 nd ⁡ F H = H
290 285 289 eqtrd ⊢ φ ∧ a = E G ∧ b = F H → 2 nd ⁡ b = H
291 283 290 oveq12d ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ a · ˙ 2 nd ⁡ b = E · ˙ H
292 284 fveq2d ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ b = 1 st ⁡ F H
293 op1stg ⊢ F ∈ B ∧ H ∈ S → 1 st ⁡ F H = F
294 286 287 293 syl2anc ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ F H = F
295 292 294 eqtrd ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ b = F
296 277 fveq2d ⊢ φ ∧ a = E G ∧ b = F H → 2 nd ⁡ a = 2 nd ⁡ E G
297 op2ndg ⊢ E ∈ B ∧ G ∈ S → 2 nd ⁡ E G = G
298 279 280 297 syl2anc ⊢ φ ∧ a = E G ∧ b = F H → 2 nd ⁡ E G = G
299 296 298 eqtrd ⊢ φ ∧ a = E G ∧ b = F H → 2 nd ⁡ a = G
300 295 299 oveq12d ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ b · ˙ 2 nd ⁡ a = F · ˙ G
301 291 300 oveq12d ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a = E · ˙ H + ˙ F · ˙ G
302 299 290 oveq12d ⊢ φ ∧ a = E G ∧ b = F H → 2 nd ⁡ a · ˙ 2 nd ⁡ b = G · ˙ H
303 301 302 opeq12d ⊢ φ ∧ a = E G ∧ b = F H → 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b = E · ˙ H + ˙ F · ˙ G G · ˙ H
304 opex ⊢ E · ˙ H + ˙ F · ˙ G G · ˙ H ∈ V
305 304 a1i ⊢ φ → E · ˙ H + ˙ F · ˙ G G · ˙ H ∈ V
306 276 303 13 14 305 ovmpod ⊢ φ → E G a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b F H = E · ˙ H + ˙ F · ˙ G G · ˙ H
307 275 306 eqtrd ⊢ φ → E G + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a F H = E · ˙ H + ˙ F · ˙ G G · ˙ H
308 307 eceq1d ⊢ φ → E G + Base ndx B × S + ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b + ˙ 1 st ⁡ b · ˙ 2 nd ⁡ a 2 nd ⁡ a · ˙ 2 nd ⁡ b ⋅ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 1 st ⁡ b 2 nd ⁡ a · ˙ 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ R ⋅ ndx k ∈ Base Scalar ⁡ R , a ∈ B × S ⟼ k ⋅ R 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ R × t TopSet ⁡ R ↾ 𝑡 S ≤ ndx a b | a ∈ B × S ∧ b ∈ B × S ∧ 1 st ⁡ a · ˙ 2 nd ⁡ b ≤ R 1 st ⁡ b · ˙ 2 nd ⁡ a dist ⁡ ndx a ∈ B × S , b ∈ B × S ⟼ 1 st ⁡ a · ˙ 2 nd ⁡ b dist ⁡ R 1 st ⁡ b · ˙ 2 nd ⁡ a F H ∼ ˙ = E · ˙ H + ˙ F · ˙ G G · ˙ H ∼ ˙
309 274 308 eqtrd ⊢ φ → E G ∼ ˙ ⊕ ˙ F H ∼ ˙ = E · ˙ H + ˙ F · ˙ G G · ˙ H ∼ ˙