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 33274
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 2737 . . 3 (0g𝑅) = (0g𝑅)
3 rlocaddval.2 . . 3 · = (.r𝑅)
4 eqid 2737 . . 3 (-g𝑅) = (-g𝑅)
5 eqid 2737 . . 3 (𝐵 × 𝑆) = (𝐵 × 𝑆)
6 rlocaddval.4 . . 3 𝐿 = (𝑅 RLocal 𝑆)
7 rlocaddval.5 . . 3 = (𝑅 ~RL 𝑆)
8 rlocaddval.r . . 3 (𝜑𝑅 ∈ CRing)
9 rlocaddval.s . . . 4 (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
10 eqid 2737 . . . . . 6 (mulGrp‘𝑅) = (mulGrp‘𝑅)
1110, 1mgpbas 20142 . . . . 5 𝐵 = (Base‘(mulGrp‘𝑅))
1211submss 18822 . . . 4 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆𝐵)
139, 12syl 17 . . 3 (𝜑𝑆𝐵)
141, 2, 3, 4, 5, 6, 7, 8, 13rlocbas 33271 . 2 (𝜑 → ((𝐵 × 𝑆) / ) = (Base‘𝐿))
15 eqidd 2738 . 2 (𝜑 → (+g𝐿) = (+g𝐿))
16 eqidd 2738 . 2 (𝜑 → (.r𝐿) = (.r𝐿))
17 eqid 2737 . . . 4 (Base‘𝐿) = (Base‘𝐿)
18 eqid 2737 . . . 4 (0g𝐿) = (0g𝐿)
19 eqid 2737 . . . 4 (+g𝐿) = (+g𝐿)
208crngringd 20243 . . . . . . . 8 (𝜑𝑅 ∈ Ring)
211, 2ring0cl 20264 . . . . . . . 8 (𝑅 ∈ Ring → (0g𝑅) ∈ 𝐵)
2220, 21syl 17 . . . . . . 7 (𝜑 → (0g𝑅) ∈ 𝐵)
23 eqid 2737 . . . . . . . . . 10 (1r𝑅) = (1r𝑅)
2410, 23ringidval 20180 . . . . . . . . 9 (1r𝑅) = (0g‘(mulGrp‘𝑅))
2524subm0cl 18824 . . . . . . . 8 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → (1r𝑅) ∈ 𝑆)
269, 25syl 17 . . . . . . 7 (𝜑 → (1r𝑅) ∈ 𝑆)
2722, 26opelxpd 5724 . . . . . 6 (𝜑 → ⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
287ovexi 7465 . . . . . . 7 ∈ V
2928ecelqsi 8813 . . . . . 6 (⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3027, 29syl 17 . . . . 5 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3130, 14eleqtrd 2843 . . . 4 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ (Base‘𝐿))
3214eleq2d 2827 . . . . . 6 (𝜑 → (𝑥 ∈ ((𝐵 × 𝑆) / ) ↔ 𝑥 ∈ (Base‘𝐿)))
3332biimpar 477 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐿)) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
34 simpr 484 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
3534oveq2d 7447 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
3620ad4antr 732 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Ring)
379ad4antr 732 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
3837, 12syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆𝐵)
39 simplr 769 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝑆)
4038, 39sseldd 3984 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝐵)
411, 3, 2, 36, 40ringlzd 20292 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · 𝑏) = (0g𝑅))
42 simpllr 776 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎𝐵)
431, 3, 23, 36, 42ringridmd 20270 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 · (1r𝑅)) = 𝑎)
4441, 43oveq12d 7449 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = ((0g𝑅)(+g𝑅)𝑎))
45 eqid 2737 . . . . . . . . . . . 12 (+g𝑅) = (+g𝑅)
4636ringgrpd 20239 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Grp)
471, 45, 2, 46, 42grplidd 18987 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(+g𝑅)𝑎) = 𝑎)
4844, 47eqtrd 2777 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = 𝑎)
491, 3, 23, 36, 40ringlidmd 20269 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑏) = 𝑏)
5048, 49opeq12d 4881 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
5150eceq1d 8785 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
528ad4antr 732 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ CRing)
5322ad4antr 732 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (0g𝑅) ∈ 𝐵)
5437, 25syl 17 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝑆)
551, 3, 45, 6, 7, 52, 37, 53, 42, 54, 39, 19rlocaddval 33272 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] )
5651, 55, 343eqtr4d 2787 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
5735, 56eqtrd 2777 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
58 simpr 484 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
5958elrlocbasi 33270 . . . . . 6 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
6057, 59r19.29vva 3216 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
6133, 60syldan 591 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
62 rlocaddval.3 . . . . . . . 8 + = (+g𝑅)
631, 3, 62, 6, 7, 52, 37, 42, 53, 39, 54, 19rlocaddval 33272 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
6434oveq1d 7446 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ))
6543, 41oveq12d 7449 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)) = (𝑎 + (0g𝑅)))
661, 62, 2, 46, 42grpridd 18988 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 + (0g𝑅)) = 𝑎)
6765, 66eqtr2d 2778 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)))
681, 3, 23, 36, 40ringridmd 20270 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · (1r𝑅)) = 𝑏)
6968eqcomd 2743 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏 = (𝑏 · (1r𝑅)))
7067, 69opeq12d 4881 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩)
7170eceq1d 8785 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7234, 71eqtrd 2777 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7363, 64, 723eqtr4d 2787 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7473, 59r19.29vva 3216 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7533, 74syldan 591 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7617, 18, 19, 31, 61, 75ismgmid2 18681 . . 3 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] = (0g𝐿))
77 simp-4r 784 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
78 simpr 484 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
7977, 78oveq12d 7449 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
808ad8antr 740 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ CRing)
819ad8antr 740 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
82 simp-6r 788 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑎𝐵)
83 simpllr 776 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑐𝐵)
84 simp-5r 786 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝑆)
85 simplr 769 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝑆)
861, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 19rlocaddval 33272 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
8780crnggrpd 20244 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Grp)
8820ad8antr 740 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Ring)
8981, 12syl 17 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆𝐵)
9089, 85sseldd 3984 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝐵)
911, 3, 88, 82, 90ringcld 20257 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
9289, 84sseldd 3984 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝐵)
931, 3, 88, 83, 92ringcld 20257 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
941, 62, 87, 91, 93grpcld 18965 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
9510, 3mgpplusg 20141 . . . . . . . . . . . 12 · = (+g‘(mulGrp‘𝑅))
9695, 81, 84, 85submcld 33040 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
9794, 96opelxpd 5724 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
9828ecelqsi 8813 . . . . . . . . . 10 (⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
9997, 98syl 17 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
10086, 99eqeltrd 2841 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
10179, 100eqeltrd 2841 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
102 simp-4r 784 . . . . . . . 8 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
103102elrlocbasi 33270 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
104101, 103r19.29vva 3216 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
105 simplr 769 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
106105elrlocbasi 33270 . . . . . 6 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
107104, 106r19.29vva 3216 . . . . 5 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1081073impa 1110 . . . 4 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1098ad10antr 744 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ CRing)
110109crnggrpd 20244 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Grp)
11120ad10antr 744 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Ring)
112 simp-9r 794 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑎𝐵)
1139ad10antr 744 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
114113, 12syl 17 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆𝐵)
115 simp-5r 786 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝑆)
116114, 115sseldd 3984 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝐵)
1171, 3, 111, 112, 116ringcld 20257 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
118 simplr 769 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝑆)
119114, 118sseldd 3984 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝐵)
1201, 3, 111, 117, 119ringcld 20257 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) ∈ 𝐵)
121 simp-6r 788 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑐𝐵)
122 simp-8r 792 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝑆)
123114, 122sseldd 3984 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝐵)
1241, 3, 111, 121, 123ringcld 20257 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
1251, 3, 111, 124, 119ringcld 20257 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) ∈ 𝐵)
126 simpllr 776 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑒𝐵)
1271, 3, 111, 123, 116ringcld 20257 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝐵)
1281, 3, 111, 126, 127ringcld 20257 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) ∈ 𝐵)
1291, 62, 110, 120, 125, 128grpassd 18963 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))))
1301, 3, 111, 112, 116, 119ringassd 20254 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) = (𝑎 · (𝑑 · 𝑓)))
1311, 3, 109, 121, 123, 119crng32d 20256 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) = ((𝑐 · 𝑓) · 𝑏))
1321, 3, 109, 126, 123, 116crng12d 20255 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = (𝑏 · (𝑒 · 𝑑)))
1331, 3, 111, 126, 116ringcld 20257 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · 𝑑) ∈ 𝐵)
1341, 3, 109, 123, 133crngcomd 20252 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑒 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
135132, 134eqtrd 2777 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
136131, 135oveq12d 7449 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
137130, 136oveq12d 7449 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
138129, 137eqtrd 2777 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
1391, 62, 3, 111, 117, 124, 119ringdird 20261 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) = (((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)))
140139oveq1d 7446 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))))
1411, 3, 111, 121, 119ringcld 20257 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑓) ∈ 𝐵)
1421, 62, 3, 111, 141, 133, 123ringdird 20261 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
143142oveq2d 7447 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
144138, 140, 1433eqtr4d 2787 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)))
1451, 3, 111, 123, 116, 119ringassd 20254 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑏 · (𝑑 · 𝑓)))
146144, 145opeq12d 4881 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩)
147146eceq1d 8785 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
1481, 62, 110, 117, 124grpcld 18965 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
14995, 113, 122, 115submcld 33040 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
1501, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 19rlocaddval 33272 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] )
1511, 62, 110, 141, 133grpcld 18965 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑓) + (𝑒 · 𝑑)) ∈ 𝐵)
15295, 113, 115, 118submcld 33040 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑑 · 𝑓) ∈ 𝑆)
1531, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 19rlocaddval 33272 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
154147, 150, 1533eqtr4d 2787 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
1551, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 19rlocaddval 33272 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
156155oveq1d 7446 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
1571, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 19rlocaddval 33272 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] )
158157oveq2d 7447 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
159154, 156, 1583eqtr4d 2787 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
160 simp-7r 790 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
161 simp-4r 784 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
162160, 161oveq12d 7449 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
163 simpr 484 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑧 = [⟨𝑒, 𝑓⟩] )
164162, 163oveq12d 7449 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ))
165161, 163oveq12d 7449 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(+g𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
166160, 165oveq12d 7449 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
167159, 164, 1663eqtr4d 2787 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
168 simpr3 1197 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
169168ad6antr 736 . . . . . . . 8 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
170169elrlocbasi 33270 . . . . . . 7 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ∃𝑒𝐵𝑓𝑆 𝑧 = [⟨𝑒, 𝑓⟩] )
171167, 170r19.29vva 3216 . . . . . 6 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
172 simpr2 1196 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
173172ad5ant12 756 . . . . . . 7 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
174173elrlocbasi 33270 . . . . . 6 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
175171, 174r19.29vva 3216 . . . . 5 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
176 simpr1 1195 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
177176elrlocbasi 33270 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
178175, 177r19.29vva 3216 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
17914, 15, 108, 178, 30, 60, 74ismndd 18769 . . 3 (𝜑𝐿 ∈ Mnd)
180 eqid 2737 . . . . . . . 8 (invg𝑅) = (invg𝑅)
1811, 180, 46, 42grpinvcld 19006 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((invg𝑅)‘𝑎) ∈ 𝐵)
182181, 39opelxpd 5724 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆))
18328ecelqsi 8813 . . . . . 6 (⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
184182, 183syl 17 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
185 simpr 484 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] )
186 simplr 769 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
187185, 186oveq12d 7449 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → (𝑢(+g𝐿)𝑥) = ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
188187eqeq1d 2739 . . . . 5 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → ((𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] ↔ ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] ))
1891, 3, 62, 6, 7, 52, 37, 181, 42, 39, 39, 19rlocaddval 33272 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] )
1901, 62, 2, 180, 46, 42grplinvd 19012 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((invg𝑅)‘𝑎) + 𝑎) = (0g𝑅))
191190oveq1d 7446 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((0g𝑅) · 𝑏))
1921, 62, 3, 36, 181, 42, 40ringdird 20261 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)))
193191, 192, 413eqtr3d 2785 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)) = (0g𝑅))
194193opeq1d 4879 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
195194eceq1d 8785 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (𝑏 · 𝑏)⟩] )
1961, 2, 23, 3, 4, 5, 7, 8, 9erler 33269 . . . . . . . 8 (𝜑 Er (𝐵 × 𝑆))
197196ad4antr 732 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → Er (𝐵 × 𝑆))
198 eqidd 2738 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
199 eqidd 2738 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (1r𝑅)⟩ = ⟨(0g𝑅), (1r𝑅)⟩)
20095, 37, 39, 39submcld 33040 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝑆)
2011, 3, 23, 36, 53ringridmd 20270 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (1r𝑅)) = (0g𝑅))
20238, 200sseldd 3984 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝐵)
2031, 3, 2, 36, 202ringlzd 20292 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (𝑏 · 𝑏)) = (0g𝑅))
204201, 203oveq12d 7449 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = ((0g𝑅)(-g𝑅)(0g𝑅)))
2051, 2, 4grpsubid 19042 . . . . . . . . . . . 12 ((𝑅 ∈ Grp ∧ (0g𝑅) ∈ 𝐵) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
20646, 53, 205syl2anc 584 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
207204, 206eqtrd 2777 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = (0g𝑅))
208207oveq2d 7447 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = ((𝑏 · 𝑏) · (0g𝑅)))
2091, 3, 2, 36, 202ringrzd 20293 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (0g𝑅)) = (0g𝑅))
210208, 209eqtrd 2777 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = (0g𝑅))
2111, 7, 38, 2, 3, 4, 198, 199, 53, 53, 200, 54, 200, 210erlbrd 33267 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ ⟨(0g𝑅), (1r𝑅)⟩)
212197, 211erthi 8798 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(0g𝑅), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (1r𝑅)⟩] )
213189, 195, 2123eqtrd 2781 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] )
214184, 188, 213rspcedvd 3624 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
215214, 59r19.29vva 3216 . . 3 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
21614, 15, 76, 179, 215isgrpd2e 18973 . 2 (𝜑𝐿 ∈ Grp)
21777, 78oveq12d 7449 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
218 eqid 2737 . . . . . . . 8 (.r𝐿) = (.r𝐿)
2191, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 218rlocmulval 33273 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
2201, 3, 88, 82, 83ringcld 20257 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
221220, 96opelxpd 5724 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
22228ecelqsi 8813 . . . . . . . 8 (⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
223221, 222syl 17 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
224219, 223eqeltrd 2841 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
225217, 224eqeltrd 2841 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
226225, 103r19.29vva 3216 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
227226, 106r19.29vva 3216 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2282273impa 1110 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2291, 3, 111, 112, 121, 126ringassd 20254 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · 𝑒) = (𝑎 · (𝑐 · 𝑒)))
230229, 145opeq12d 4881 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩)
231230eceq1d 8785 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
2321, 3, 111, 112, 121ringcld 20257 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
2331, 3, 62, 6, 7, 109, 113, 232, 126, 149, 118, 218rlocmulval 33273 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
2341, 3, 111, 121, 126ringcld 20257 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑒) ∈ 𝐵)
2351, 3, 62, 6, 7, 109, 113, 112, 234, 122, 152, 218rlocmulval 33273 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
236231, 233, 2353eqtr4d 2787 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
2371, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 218rlocmulval 33273 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
238237oveq1d 7446 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
2391, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 218rlocmulval 33273 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] )
240239oveq2d 7447 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
241236, 238, 2403eqtr4d 2787 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
242160, 161oveq12d 7449 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
243242, 163oveq12d 7449 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
244161, 163oveq12d 7449 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(.r𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
245160, 244oveq12d 7449 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
246241, 243, 2453eqtr4d 2787 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
247246, 170r19.29vva 3216 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
248247, 174r19.29vva 3216 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
249248, 177r19.29vva 3216 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
250196ad10antr 744 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → Er (𝐵 × 𝑆))
251 eqidd 2738 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ = ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩)
2521, 3, 111, 112, 123ringcld 20257 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑏) ∈ 𝐵)
2531, 62, 3, 111, 252, 141, 133ringdid 20260 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2541, 3, 111, 112, 123, 151ringassd 20254 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
255253, 254eqtr3d 2779 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
25610crngmgp 20238 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
2578, 256syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
258257ad10antr 744 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (mulGrp‘𝑅) ∈ CMnd)
25911, 95, 258, 112, 121, 123, 119cmn4d 33037 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · (𝑏 · 𝑓)) = ((𝑎 · 𝑏) · (𝑐 · 𝑓)))
26011, 95, 258, 112, 126, 123, 116cmn4d 33037 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑏 · 𝑑)) = ((𝑎 · 𝑏) · (𝑒 · 𝑑)))
261259, 260oveq12d 7449 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2621, 3, 109, 123, 112, 151crng12d 20255 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
263255, 261, 2623eqtr4d 2787 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
2641, 3, 109, 127, 123, 119crng12d 20255 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · ((𝑏 · 𝑑) · 𝑓)))
265145oveq2d 7447 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · ((𝑏 · 𝑑) · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
266264, 265eqtrd 2777 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
267263, 266opeq12d 4881 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩ = ⟨(𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))), (𝑏 · (𝑏 · (𝑑 · 𝑓)))⟩)
2681, 3, 111, 112, 151ringcld 20257 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) ∈ 𝐵)
2691, 3, 111, 123, 268ringcld 20257 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) ∈ 𝐵)
27095, 113, 122, 152submcld 33040 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑑 · 𝑓)) ∈ 𝑆)
27195, 113, 122, 270submcld 33040 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) ∈ 𝑆)
272 eqidd 2738 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
273 eqidd 2738 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
2741, 7, 109, 113, 3, 251, 267, 268, 269, 270, 271, 122, 272, 273erlbr2d 33268 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩)
275250, 274erthi 8798 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
2761, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 218rlocmulval 33273 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] )
2771, 3, 111, 112, 126ringcld 20257 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑒) ∈ 𝐵)
27895, 113, 122, 118submcld 33040 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝑆)
2791, 3, 62, 6, 7, 109, 113, 232, 277, 149, 278, 19rlocaddval 33272 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
280275, 276, 2793eqtr4d 2787 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
281157oveq2d 7447 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
2821, 3, 62, 6, 7, 109, 113, 112, 126, 122, 118, 218rlocmulval 33273 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] )
283237, 282oveq12d 7449 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
284280, 281, 2833eqtr4d 2787 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
285160, 165oveq12d 7449 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
286160, 163oveq12d 7449 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑧) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
287242, 286oveq12d 7449 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
288284, 285, 2873eqtr4d 2787 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
289288, 170r19.29vva 3216 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
290289, 174r19.29vva 3216 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
291290, 177r19.29vva 3216 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
2921, 62, 3, 111, 117, 124, 126ringdird 20261 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒) = (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)))
293292opeq1d 4879 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)), ((𝑏 · 𝑑) · 𝑓)⟩)
2941, 3, 111, 117, 126, 119ringassd 20254 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) · 𝑓) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
2951, 3, 111, 117, 126ringcld 20257 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑒) ∈ 𝐵)
2961, 3, 109, 119, 295crngcomd 20252 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑎 · 𝑑) · 𝑒)) = (((𝑎 · 𝑑) · 𝑒) · 𝑓))
29711, 95, 258, 112, 126, 116, 119cmn4d 33037 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
298294, 296, 2973eqtr4rd 2788 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = (𝑓 · ((𝑎 · 𝑑) · 𝑒)))
2991, 3, 111, 124, 126, 119ringassd 20254 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑒) · 𝑓) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
3001, 3, 111, 124, 126ringcld 20257 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑒) ∈ 𝐵)
3011, 3, 109, 119, 300crngcomd 20252 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑐 · 𝑏) · 𝑒)) = (((𝑐 · 𝑏) · 𝑒) · 𝑓))
30211, 95, 258, 121, 126, 123, 119cmn4d 33037 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
303299, 301, 3023eqtr4rd 2788 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = (𝑓 · ((𝑐 · 𝑏) · 𝑒)))
304298, 303oveq12d 7449 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
3051, 62, 3, 111, 119, 295, 300ringdid 20260 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
306304, 305eqtr4d 2780 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
307114, 278sseldd 3984 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝐵)
3081, 3, 111, 116, 307, 119ringassd 20254 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · (𝑏 · 𝑓)) · 𝑓) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
3091, 3, 109, 123, 116crngcomd 20252 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
310309oveq1d 7446 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = ((𝑑 · 𝑏) · 𝑓))
3111, 3, 111, 116, 123, 119ringassd 20254 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · 𝑏) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
312310, 311eqtrd 2777 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
313312oveq1d 7446 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = ((𝑑 · (𝑏 · 𝑓)) · 𝑓))
3141, 3, 109, 307, 116, 119crng12d 20255 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
315308, 313, 3143eqtr4rd 2788 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (((𝑏 · 𝑑) · 𝑓) · 𝑓))
316306, 315opeq12d 4881 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩ = ⟨(𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))), (((𝑏 · 𝑑) · 𝑓) · 𝑓)⟩)
3171, 62, 110, 295, 300grpcld 18965 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)) ∈ 𝐵)
3181, 3, 111, 119, 317ringcld 20257 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) ∈ 𝐵)
319145, 270eqeltrd 2841 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝑆)
32095, 113, 319, 118submcld 33040 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) ∈ 𝑆)
321 eqidd 2738 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
322114, 319sseldd 3984 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝐵)
3231, 3, 109, 322, 119crngcomd 20252 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = (𝑓 · ((𝑏 · 𝑑) · 𝑓)))
3241, 7, 109, 113, 3, 293, 316, 317, 318, 319, 320, 118, 321, 323erlbr2d 33268 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩)
325250, 324erthi 8798 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
3261, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 218rlocmulval 33273 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
3271, 3, 62, 6, 7, 109, 113, 277, 234, 278, 152, 19rlocaddval 33272 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
328325, 326, 3273eqtr4d 2787 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
329155oveq1d 7446 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
330282, 239oveq12d 7449 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
331328, 329, 3303eqtr4d 2787 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
332162, 163oveq12d 7449 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
333286, 244oveq12d 7449 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
334331, 332, 3333eqtr4d 2787 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
335334, 170r19.29vva 3216 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
336335, 174r19.29vva 3216 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
337336, 177r19.29vva 3216 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
33813, 26sseldd 3984 . . . 4 (𝜑 → (1r𝑅) ∈ 𝐵)
339338, 26opelxpd 5724 . . 3 (𝜑 → ⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
34028ecelqsi 8813 . . 3 (⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
341339, 340syl 17 . 2 (𝜑 → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
34234oveq2d 7447 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
3431, 3, 23, 36, 42ringlidmd 20269 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑎) = 𝑎)
344343, 49opeq12d 4881 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
345344eceq1d 8785 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
34638, 54sseldd 3984 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝐵)
3471, 3, 62, 6, 7, 52, 37, 346, 42, 54, 39, 218rlocmulval 33273 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] )
348345, 347, 343eqtr4d 2787 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
349342, 348eqtrd 2777 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
350349, 59r19.29vva 3216 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
3511, 3, 62, 6, 7, 52, 37, 42, 346, 39, 54, 218rlocmulval 33273 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
35234oveq1d 7446 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ))
35343eqcomd 2743 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = (𝑎 · (1r𝑅)))
354353, 69opeq12d 4881 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩)
355354eceq1d 8785 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
356351, 352, 3553eqtr4d 2787 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨𝑎, 𝑏⟩] )
357356, 34eqtr4d 2780 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
358357, 59r19.29vva 3216 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
3591, 3, 80, 82, 83crngcomd 20252 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) = (𝑐 · 𝑎))
3601, 3, 80, 92, 90crngcomd 20252 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
361359, 360opeq12d 4881 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ = ⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩)
362361eceq1d 8785 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
3631, 3, 62, 6, 7, 80, 81, 83, 82, 85, 84, 218rlocmulval 33273 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
364362, 219, 3633eqtr4d 2787 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
36578, 77oveq12d 7449 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑦(.r𝐿)𝑥) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
366364, 217, 3653eqtr4d 2787 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
367366, 103r19.29vva 3216 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
368367, 106r19.29vva 3216 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
3693683impa 1110 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
37014, 15, 16, 216, 228, 249, 291, 337, 341, 350, 358, 369iscrngd 20289 1 (𝜑𝐿 ∈ CRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wrex 3070  wss 3951  cop 4632   × cxp 5683  cfv 6561  (class class class)co 7431   Er wer 8742  [cec 8743   / cqs 8744  Basecbs 17247  +gcplusg 17297  .rcmulr 17298  0gc0g 17484  SubMndcsubmnd 18795  Grpcgrp 18951  invgcminusg 18952  -gcsg 18953  CMndccmn 19798  mulGrpcmgp 20137  1rcur 20178  Ringcrg 20230  CRingccrg 20231   ~RL cerl 33257   RLocal crloc 33258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-ec 8747  df-qs 8751  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-fz 13548  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-0g 17486  df-imas 17553  df-qus 17554  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-grp 18954  df-minusg 18955  df-sbg 18956  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-cring 20233  df-erl 33259  df-rloc 33260
This theorem is referenced by:  rloc0g  33275  rloc1r  33276  rlocf1  33277  fracfld  33310
  Copyright terms: Public domain W3C validator