Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rloccring Structured version   Visualization version   GIF version

Theorem rloccring 33060
Description: The ring localization 𝐿 of a commutative ring 𝑅 by a multiplicatively closed set 𝑆 is itself a commutative ring. (Contributed by Thierry Arnoux, 4-May-2025.)
Hypotheses
Ref Expression
rlocaddval.1 𝐵 = (Base‘𝑅)
rlocaddval.2 · = (.r𝑅)
rlocaddval.3 + = (+g𝑅)
rlocaddval.4 𝐿 = (𝑅 RLocal 𝑆)
rlocaddval.5 = (𝑅 ~RL 𝑆)
rlocaddval.r (𝜑𝑅 ∈ CRing)
rlocaddval.s (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
Assertion
Ref Expression
rloccring (𝜑𝐿 ∈ CRing)

Proof of Theorem rloccring
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑥 𝑦 𝑧 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rlocaddval.1 . . 3 𝐵 = (Base‘𝑅)
2 eqid 2725 . . 3 (0g𝑅) = (0g𝑅)
3 rlocaddval.2 . . 3 · = (.r𝑅)
4 eqid 2725 . . 3 (-g𝑅) = (-g𝑅)
5 eqid 2725 . . 3 (𝐵 × 𝑆) = (𝐵 × 𝑆)
6 rlocaddval.4 . . 3 𝐿 = (𝑅 RLocal 𝑆)
7 rlocaddval.5 . . 3 = (𝑅 ~RL 𝑆)
8 rlocaddval.r . . 3 (𝜑𝑅 ∈ CRing)
9 rlocaddval.s . . . 4 (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
10 eqid 2725 . . . . . 6 (mulGrp‘𝑅) = (mulGrp‘𝑅)
1110, 1mgpbas 20092 . . . . 5 𝐵 = (Base‘(mulGrp‘𝑅))
1211submss 18769 . . . 4 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆𝐵)
139, 12syl 17 . . 3 (𝜑𝑆𝐵)
141, 2, 3, 4, 5, 6, 7, 8, 13rlocbas 33057 . 2 (𝜑 → ((𝐵 × 𝑆) / ) = (Base‘𝐿))
15 eqidd 2726 . 2 (𝜑 → (+g𝐿) = (+g𝐿))
16 eqidd 2726 . 2 (𝜑 → (.r𝐿) = (.r𝐿))
17 eqid 2725 . . . 4 (Base‘𝐿) = (Base‘𝐿)
18 eqid 2725 . . . 4 (0g𝐿) = (0g𝐿)
19 eqid 2725 . . . 4 (+g𝐿) = (+g𝐿)
208crngringd 20198 . . . . . . . 8 (𝜑𝑅 ∈ Ring)
211, 2ring0cl 20215 . . . . . . . 8 (𝑅 ∈ Ring → (0g𝑅) ∈ 𝐵)
2220, 21syl 17 . . . . . . 7 (𝜑 → (0g𝑅) ∈ 𝐵)
23 eqid 2725 . . . . . . . . . 10 (1r𝑅) = (1r𝑅)
2410, 23ringidval 20135 . . . . . . . . 9 (1r𝑅) = (0g‘(mulGrp‘𝑅))
2524subm0cl 18771 . . . . . . . 8 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → (1r𝑅) ∈ 𝑆)
269, 25syl 17 . . . . . . 7 (𝜑 → (1r𝑅) ∈ 𝑆)
2722, 26opelxpd 5717 . . . . . 6 (𝜑 → ⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
287ovexi 7453 . . . . . . 7 ∈ V
2928ecelqsi 8792 . . . . . 6 (⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3027, 29syl 17 . . . . 5 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3130, 14eleqtrd 2827 . . . 4 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ (Base‘𝐿))
3214eleq2d 2811 . . . . . 6 (𝜑 → (𝑥 ∈ ((𝐵 × 𝑆) / ) ↔ 𝑥 ∈ (Base‘𝐿)))
3332biimpar 476 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐿)) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
34 simpr 483 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
3534oveq2d 7435 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
3620ad4antr 730 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Ring)
379ad4antr 730 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
3837, 12syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆𝐵)
39 simplr 767 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝑆)
4038, 39sseldd 3977 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝐵)
411, 3, 2, 36, 40ringlzd 20243 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · 𝑏) = (0g𝑅))
42 simpllr 774 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎𝐵)
431, 3, 23, 36, 42ringridmd 20221 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 · (1r𝑅)) = 𝑎)
4441, 43oveq12d 7437 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = ((0g𝑅)(+g𝑅)𝑎))
45 eqid 2725 . . . . . . . . . . . 12 (+g𝑅) = (+g𝑅)
4636ringgrpd 20194 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Grp)
471, 45, 2, 46, 42grplidd 18934 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(+g𝑅)𝑎) = 𝑎)
4844, 47eqtrd 2765 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = 𝑎)
491, 3, 23, 36, 40ringlidmd 20220 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑏) = 𝑏)
5048, 49opeq12d 4883 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
5150eceq1d 8764 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
528ad4antr 730 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ CRing)
5322ad4antr 730 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (0g𝑅) ∈ 𝐵)
5437, 25syl 17 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝑆)
551, 3, 45, 6, 7, 52, 37, 53, 42, 54, 39, 19rlocaddval 33058 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] )
5651, 55, 343eqtr4d 2775 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
5735, 56eqtrd 2765 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
58 simpr 483 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
5958elrlocbasi 33056 . . . . . 6 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
6057, 59r19.29vva 3203 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
6133, 60syldan 589 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
62 rlocaddval.3 . . . . . . . 8 + = (+g𝑅)
631, 3, 62, 6, 7, 52, 37, 42, 53, 39, 54, 19rlocaddval 33058 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
6434oveq1d 7434 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ))
6543, 41oveq12d 7437 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)) = (𝑎 + (0g𝑅)))
661, 62, 2, 46, 42grpridd 18935 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 + (0g𝑅)) = 𝑎)
6765, 66eqtr2d 2766 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)))
681, 3, 23, 36, 40ringridmd 20221 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · (1r𝑅)) = 𝑏)
6968eqcomd 2731 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏 = (𝑏 · (1r𝑅)))
7067, 69opeq12d 4883 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩)
7170eceq1d 8764 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7234, 71eqtrd 2765 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7363, 64, 723eqtr4d 2775 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7473, 59r19.29vva 3203 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7533, 74syldan 589 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7617, 18, 19, 31, 61, 75ismgmid2 18631 . . 3 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] = (0g𝐿))
77 simp-4r 782 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
78 simpr 483 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
7977, 78oveq12d 7437 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
808ad8antr 738 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ CRing)
819ad8antr 738 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
82 simp-6r 786 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑎𝐵)
83 simpllr 774 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑐𝐵)
84 simp-5r 784 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝑆)
85 simplr 767 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝑆)
861, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 19rlocaddval 33058 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
8780crnggrpd 20199 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Grp)
8820ad8antr 738 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Ring)
8981, 12syl 17 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆𝐵)
9089, 85sseldd 3977 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝐵)
911, 3, 88, 82, 90ringcld 20211 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
9289, 84sseldd 3977 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝐵)
931, 3, 88, 83, 92ringcld 20211 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
941, 62, 87, 91, 93grpcld 18912 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
9510, 3mgpplusg 20090 . . . . . . . . . . . 12 · = (+g‘(mulGrp‘𝑅))
9695, 81, 84, 85submcld 32844 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
9794, 96opelxpd 5717 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
9828ecelqsi 8792 . . . . . . . . . 10 (⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
9997, 98syl 17 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
10086, 99eqeltrd 2825 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
10179, 100eqeltrd 2825 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
102 simp-4r 782 . . . . . . . 8 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
103102elrlocbasi 33056 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
104101, 103r19.29vva 3203 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
105 simplr 767 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
106105elrlocbasi 33056 . . . . . 6 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
107104, 106r19.29vva 3203 . . . . 5 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1081073impa 1107 . . . 4 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1098ad10antr 742 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ CRing)
110109crnggrpd 20199 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Grp)
11120ad10antr 742 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Ring)
112 simp-9r 792 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑎𝐵)
1139ad10antr 742 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
114113, 12syl 17 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆𝐵)
115 simp-5r 784 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝑆)
116114, 115sseldd 3977 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝐵)
1171, 3, 111, 112, 116ringcld 20211 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
118 simplr 767 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝑆)
119114, 118sseldd 3977 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝐵)
1201, 3, 111, 117, 119ringcld 20211 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) ∈ 𝐵)
121 simp-6r 786 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑐𝐵)
122 simp-8r 790 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝑆)
123114, 122sseldd 3977 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝐵)
1241, 3, 111, 121, 123ringcld 20211 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
1251, 3, 111, 124, 119ringcld 20211 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) ∈ 𝐵)
126 simpllr 774 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑒𝐵)
1271, 3, 111, 123, 116ringcld 20211 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝐵)
1281, 3, 111, 126, 127ringcld 20211 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) ∈ 𝐵)
1291, 62, 110, 120, 125, 128grpassd 18910 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))))
1301, 3, 111, 112, 116, 119ringassd 20209 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) = (𝑎 · (𝑑 · 𝑓)))
1311, 3, 109, 121, 123, 119cringmul32d 33028 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) = ((𝑐 · 𝑓) · 𝑏))
1321, 3, 109, 126, 123, 116crng12d 20210 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = (𝑏 · (𝑒 · 𝑑)))
1331, 3, 111, 126, 116ringcld 20211 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · 𝑑) ∈ 𝐵)
1341, 3, 109, 123, 133crngcomd 20207 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑒 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
135132, 134eqtrd 2765 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
136131, 135oveq12d 7437 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
137130, 136oveq12d 7437 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
138129, 137eqtrd 2765 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
1391, 62, 3, 111, 117, 124, 119ringdird 33030 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) = (((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)))
140139oveq1d 7434 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))))
1411, 3, 111, 121, 119ringcld 20211 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑓) ∈ 𝐵)
1421, 62, 3, 111, 141, 133, 123ringdird 33030 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
143142oveq2d 7435 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
144138, 140, 1433eqtr4d 2775 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)))
1451, 3, 111, 123, 116, 119ringassd 20209 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑏 · (𝑑 · 𝑓)))
146144, 145opeq12d 4883 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩)
147146eceq1d 8764 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
1481, 62, 110, 117, 124grpcld 18912 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
14995, 113, 122, 115submcld 32844 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
1501, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 19rlocaddval 33058 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] )
1511, 62, 110, 141, 133grpcld 18912 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑓) + (𝑒 · 𝑑)) ∈ 𝐵)
15295, 113, 115, 118submcld 32844 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑑 · 𝑓) ∈ 𝑆)
1531, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 19rlocaddval 33058 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
154147, 150, 1533eqtr4d 2775 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
1551, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 19rlocaddval 33058 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
156155oveq1d 7434 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
1571, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 19rlocaddval 33058 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] )
158157oveq2d 7435 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
159154, 156, 1583eqtr4d 2775 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
160 simp-7r 788 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
161 simp-4r 782 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
162160, 161oveq12d 7437 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
163 simpr 483 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑧 = [⟨𝑒, 𝑓⟩] )
164162, 163oveq12d 7437 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ))
165161, 163oveq12d 7437 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(+g𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
166160, 165oveq12d 7437 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
167159, 164, 1663eqtr4d 2775 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
168 simpr3 1193 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
169168ad6antr 734 . . . . . . . 8 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
170169elrlocbasi 33056 . . . . . . 7 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ∃𝑒𝐵𝑓𝑆 𝑧 = [⟨𝑒, 𝑓⟩] )
171167, 170r19.29vva 3203 . . . . . 6 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
172 simpr2 1192 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
173172ad5ant12 754 . . . . . . 7 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
174173elrlocbasi 33056 . . . . . 6 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
175171, 174r19.29vva 3203 . . . . 5 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
176 simpr1 1191 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
177176elrlocbasi 33056 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
178175, 177r19.29vva 3203 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
17914, 15, 108, 178, 30, 60, 74ismndd 18719 . . 3 (𝜑𝐿 ∈ Mnd)
180 eqid 2725 . . . . . . . 8 (invg𝑅) = (invg𝑅)
1811, 180, 46, 42grpinvcld 18953 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((invg𝑅)‘𝑎) ∈ 𝐵)
182181, 39opelxpd 5717 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆))
18328ecelqsi 8792 . . . . . 6 (⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
184182, 183syl 17 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
185 simpr 483 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] )
186 simplr 767 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
187185, 186oveq12d 7437 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → (𝑢(+g𝐿)𝑥) = ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
188187eqeq1d 2727 . . . . 5 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → ((𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] ↔ ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] ))
1891, 3, 62, 6, 7, 52, 37, 181, 42, 39, 39, 19rlocaddval 33058 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] )
1901, 62, 2, 180, 46, 42grplinvd 18959 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((invg𝑅)‘𝑎) + 𝑎) = (0g𝑅))
191190oveq1d 7434 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((0g𝑅) · 𝑏))
1921, 62, 3, 36, 181, 42, 40ringdird 33030 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)))
193191, 192, 413eqtr3d 2773 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)) = (0g𝑅))
194193opeq1d 4881 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
195194eceq1d 8764 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (𝑏 · 𝑏)⟩] )
1961, 2, 23, 3, 4, 5, 7, 8, 9erler 33055 . . . . . . . 8 (𝜑 Er (𝐵 × 𝑆))
197196ad4antr 730 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → Er (𝐵 × 𝑆))
198 eqidd 2726 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
199 eqidd 2726 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (1r𝑅)⟩ = ⟨(0g𝑅), (1r𝑅)⟩)
20095, 37, 39, 39submcld 32844 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝑆)
2011, 3, 23, 36, 53ringridmd 20221 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (1r𝑅)) = (0g𝑅))
20238, 200sseldd 3977 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝐵)
2031, 3, 2, 36, 202ringlzd 20243 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (𝑏 · 𝑏)) = (0g𝑅))
204201, 203oveq12d 7437 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = ((0g𝑅)(-g𝑅)(0g𝑅)))
2051, 2, 4grpsubid 18988 . . . . . . . . . . . 12 ((𝑅 ∈ Grp ∧ (0g𝑅) ∈ 𝐵) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
20646, 53, 205syl2anc 582 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
207204, 206eqtrd 2765 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = (0g𝑅))
208207oveq2d 7435 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = ((𝑏 · 𝑏) · (0g𝑅)))
2091, 3, 2, 36, 202ringrzd 20244 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (0g𝑅)) = (0g𝑅))
210208, 209eqtrd 2765 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = (0g𝑅))
2111, 7, 38, 2, 3, 4, 198, 199, 53, 53, 200, 54, 200, 210erlbrd 33053 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ ⟨(0g𝑅), (1r𝑅)⟩)
212197, 211erthi 8777 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(0g𝑅), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (1r𝑅)⟩] )
213189, 195, 2123eqtrd 2769 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] )
214184, 188, 213rspcedvd 3608 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
215214, 59r19.29vva 3203 . . 3 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
21614, 15, 76, 179, 215isgrpd2e 18920 . 2 (𝜑𝐿 ∈ Grp)
21777, 78oveq12d 7437 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
218 eqid 2725 . . . . . . . 8 (.r𝐿) = (.r𝐿)
2191, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 218rlocmulval 33059 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
2201, 3, 88, 82, 83ringcld 20211 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
221220, 96opelxpd 5717 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
22228ecelqsi 8792 . . . . . . . 8 (⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
223221, 222syl 17 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
224219, 223eqeltrd 2825 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
225217, 224eqeltrd 2825 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
226225, 103r19.29vva 3203 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
227226, 106r19.29vva 3203 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2282273impa 1107 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2291, 3, 111, 112, 121, 126ringassd 20209 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · 𝑒) = (𝑎 · (𝑐 · 𝑒)))
230229, 145opeq12d 4883 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩)
231230eceq1d 8764 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
2321, 3, 111, 112, 121ringcld 20211 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
2331, 3, 62, 6, 7, 109, 113, 232, 126, 149, 118, 218rlocmulval 33059 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
2341, 3, 111, 121, 126ringcld 20211 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑒) ∈ 𝐵)
2351, 3, 62, 6, 7, 109, 113, 112, 234, 122, 152, 218rlocmulval 33059 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
236231, 233, 2353eqtr4d 2775 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
2371, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 218rlocmulval 33059 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
238237oveq1d 7434 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
2391, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 218rlocmulval 33059 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] )
240239oveq2d 7435 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
241236, 238, 2403eqtr4d 2775 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
242160, 161oveq12d 7437 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
243242, 163oveq12d 7437 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
244161, 163oveq12d 7437 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(.r𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
245160, 244oveq12d 7437 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
246241, 243, 2453eqtr4d 2775 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
247246, 170r19.29vva 3203 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
248247, 174r19.29vva 3203 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
249248, 177r19.29vva 3203 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
250196ad10antr 742 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → Er (𝐵 × 𝑆))
251 eqidd 2726 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ = ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩)
2521, 3, 111, 112, 123ringcld 20211 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑏) ∈ 𝐵)
2531, 62, 3, 111, 252, 141, 133ringdid 33029 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2541, 3, 111, 112, 123, 151ringassd 20209 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
255253, 254eqtr3d 2767 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
25610crngmgp 20193 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
2578, 256syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
258257ad10antr 742 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (mulGrp‘𝑅) ∈ CMnd)
25911, 95, 258, 112, 121, 123, 119cmn4d 32841 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · (𝑏 · 𝑓)) = ((𝑎 · 𝑏) · (𝑐 · 𝑓)))
26011, 95, 258, 112, 126, 123, 116cmn4d 32841 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑏 · 𝑑)) = ((𝑎 · 𝑏) · (𝑒 · 𝑑)))
261259, 260oveq12d 7437 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2621, 3, 109, 123, 112, 151crng12d 20210 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
263255, 261, 2623eqtr4d 2775 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
2641, 3, 109, 127, 123, 119crng12d 20210 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · ((𝑏 · 𝑑) · 𝑓)))
265145oveq2d 7435 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · ((𝑏 · 𝑑) · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
266264, 265eqtrd 2765 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
267263, 266opeq12d 4883 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩ = ⟨(𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))), (𝑏 · (𝑏 · (𝑑 · 𝑓)))⟩)
2681, 3, 111, 112, 151ringcld 20211 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) ∈ 𝐵)
2691, 3, 111, 123, 268ringcld 20211 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) ∈ 𝐵)
27095, 113, 122, 152submcld 32844 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑑 · 𝑓)) ∈ 𝑆)
27195, 113, 122, 270submcld 32844 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) ∈ 𝑆)
272 eqidd 2726 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
273 eqidd 2726 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
2741, 7, 109, 113, 3, 251, 267, 268, 269, 270, 271, 122, 272, 273erlbr2d 33054 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩)
275250, 274erthi 8777 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
2761, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 218rlocmulval 33059 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] )
2771, 3, 111, 112, 126ringcld 20211 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑒) ∈ 𝐵)
27895, 113, 122, 118submcld 32844 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝑆)
2791, 3, 62, 6, 7, 109, 113, 232, 277, 149, 278, 19rlocaddval 33058 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
280275, 276, 2793eqtr4d 2775 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
281157oveq2d 7435 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
2821, 3, 62, 6, 7, 109, 113, 112, 126, 122, 118, 218rlocmulval 33059 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] )
283237, 282oveq12d 7437 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
284280, 281, 2833eqtr4d 2775 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
285160, 165oveq12d 7437 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
286160, 163oveq12d 7437 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑧) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
287242, 286oveq12d 7437 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
288284, 285, 2873eqtr4d 2775 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
289288, 170r19.29vva 3203 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
290289, 174r19.29vva 3203 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
291290, 177r19.29vva 3203 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
2921, 62, 3, 111, 117, 124, 126ringdird 33030 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒) = (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)))
293292opeq1d 4881 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)), ((𝑏 · 𝑑) · 𝑓)⟩)
2941, 3, 111, 117, 126, 119ringassd 20209 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) · 𝑓) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
2951, 3, 111, 117, 126ringcld 20211 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑒) ∈ 𝐵)
2961, 3, 109, 119, 295crngcomd 20207 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑎 · 𝑑) · 𝑒)) = (((𝑎 · 𝑑) · 𝑒) · 𝑓))
29711, 95, 258, 112, 126, 116, 119cmn4d 32841 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
298294, 296, 2973eqtr4rd 2776 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = (𝑓 · ((𝑎 · 𝑑) · 𝑒)))
2991, 3, 111, 124, 126, 119ringassd 20209 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑒) · 𝑓) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
3001, 3, 111, 124, 126ringcld 20211 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑒) ∈ 𝐵)
3011, 3, 109, 119, 300crngcomd 20207 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑐 · 𝑏) · 𝑒)) = (((𝑐 · 𝑏) · 𝑒) · 𝑓))
30211, 95, 258, 121, 126, 123, 119cmn4d 32841 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
303299, 301, 3023eqtr4rd 2776 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = (𝑓 · ((𝑐 · 𝑏) · 𝑒)))
304298, 303oveq12d 7437 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
3051, 62, 3, 111, 119, 295, 300ringdid 33029 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
306304, 305eqtr4d 2768 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
307114, 278sseldd 3977 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝐵)
3081, 3, 111, 116, 307, 119ringassd 20209 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · (𝑏 · 𝑓)) · 𝑓) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
3091, 3, 109, 123, 116crngcomd 20207 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
310309oveq1d 7434 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = ((𝑑 · 𝑏) · 𝑓))
3111, 3, 111, 116, 123, 119ringassd 20209 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · 𝑏) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
312310, 311eqtrd 2765 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
313312oveq1d 7434 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = ((𝑑 · (𝑏 · 𝑓)) · 𝑓))
3141, 3, 109, 307, 116, 119crng12d 20210 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
315308, 313, 3143eqtr4rd 2776 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (((𝑏 · 𝑑) · 𝑓) · 𝑓))
316306, 315opeq12d 4883 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩ = ⟨(𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))), (((𝑏 · 𝑑) · 𝑓) · 𝑓)⟩)
3171, 62, 110, 295, 300grpcld 18912 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)) ∈ 𝐵)
3181, 3, 111, 119, 317ringcld 20211 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) ∈ 𝐵)
319145, 270eqeltrd 2825 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝑆)
32095, 113, 319, 118submcld 32844 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) ∈ 𝑆)
321 eqidd 2726 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
322114, 319sseldd 3977 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝐵)
3231, 3, 109, 322, 119crngcomd 20207 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = (𝑓 · ((𝑏 · 𝑑) · 𝑓)))
3241, 7, 109, 113, 3, 293, 316, 317, 318, 319, 320, 118, 321, 323erlbr2d 33054 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩)
325250, 324erthi 8777 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
3261, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 218rlocmulval 33059 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
3271, 3, 62, 6, 7, 109, 113, 277, 234, 278, 152, 19rlocaddval 33058 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
328325, 326, 3273eqtr4d 2775 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
329155oveq1d 7434 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
330282, 239oveq12d 7437 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
331328, 329, 3303eqtr4d 2775 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
332162, 163oveq12d 7437 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
333286, 244oveq12d 7437 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
334331, 332, 3333eqtr4d 2775 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
335334, 170r19.29vva 3203 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
336335, 174r19.29vva 3203 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
337336, 177r19.29vva 3203 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
33813, 26sseldd 3977 . . . 4 (𝜑 → (1r𝑅) ∈ 𝐵)
339338, 26opelxpd 5717 . . 3 (𝜑 → ⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
34028ecelqsi 8792 . . 3 (⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
341339, 340syl 17 . 2 (𝜑 → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
34234oveq2d 7435 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
3431, 3, 23, 36, 42ringlidmd 20220 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑎) = 𝑎)
344343, 49opeq12d 4883 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
345344eceq1d 8764 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
34638, 54sseldd 3977 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝐵)
3471, 3, 62, 6, 7, 52, 37, 346, 42, 54, 39, 218rlocmulval 33059 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] )
348345, 347, 343eqtr4d 2775 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
349342, 348eqtrd 2765 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
350349, 59r19.29vva 3203 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
3511, 3, 62, 6, 7, 52, 37, 42, 346, 39, 54, 218rlocmulval 33059 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
35234oveq1d 7434 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ))
35343eqcomd 2731 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = (𝑎 · (1r𝑅)))
354353, 69opeq12d 4883 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩)
355354eceq1d 8764 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
356351, 352, 3553eqtr4d 2775 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨𝑎, 𝑏⟩] )
357356, 34eqtr4d 2768 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
358357, 59r19.29vva 3203 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
3591, 3, 80, 82, 83crngcomd 20207 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) = (𝑐 · 𝑎))
3601, 3, 80, 92, 90crngcomd 20207 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
361359, 360opeq12d 4883 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ = ⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩)
362361eceq1d 8764 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
3631, 3, 62, 6, 7, 80, 81, 83, 82, 85, 84, 218rlocmulval 33059 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
364362, 219, 3633eqtr4d 2775 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
36578, 77oveq12d 7437 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑦(.r𝐿)𝑥) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
366364, 217, 3653eqtr4d 2775 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
367366, 103r19.29vva 3203 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
368367, 106r19.29vva 3203 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
3693683impa 1107 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
37014, 15, 16, 216, 228, 249, 291, 337, 341, 350, 358, 369iscrngd 20240 1 (𝜑𝐿 ∈ CRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wrex 3059  wss 3944  cop 4636   × cxp 5676  cfv 6549  (class class class)co 7419   Er wer 8722  [cec 8723   / cqs 8724  Basecbs 17183  +gcplusg 17236  .rcmulr 17237  0gc0g 17424  SubMndcsubmnd 18742  Grpcgrp 18898  invgcminusg 18899  -gcsg 18900  CMndccmn 19747  mulGrpcmgp 20086  1rcur 20133  Ringcrg 20185  CRingccrg 20186   ~RL cerl 33043   RLocal crloc 33044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-ec 8727  df-qs 8731  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9467  df-inf 9468  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12506  df-z 12592  df-dec 12711  df-uz 12856  df-fz 13520  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-mulr 17250  df-sca 17252  df-vsca 17253  df-ip 17254  df-tset 17255  df-ple 17256  df-ds 17258  df-0g 17426  df-imas 17493  df-qus 17494  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-submnd 18744  df-grp 18901  df-minusg 18902  df-sbg 18903  df-cmn 19749  df-abl 19750  df-mgp 20087  df-rng 20105  df-ur 20134  df-ring 20187  df-cring 20188  df-erl 33045  df-rloc 33046
This theorem is referenced by:  rloc0g  33061  rloc1r  33062  rlocf1  33063  fracfld  33094
  Copyright terms: Public domain W3C validator