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 33622
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 2766 . . 3 (0g𝑅) = (0g𝑅)
3 rlocaddval.2 . . 3 · = (.r𝑅)
4 eqid 2766 . . 3 (-g𝑅) = (-g𝑅)
5 eqid 2766 . . 3 (𝐵 × 𝑆) = (𝐵 × 𝑆)
6 rlocaddval.4 . . 3 𝐿 = (𝑅 RLocal 𝑆)
7 rlocaddval.5 . . 3 = (𝑅 ~RL 𝑆)
8 rlocaddval.r . . 3 (𝜑𝑅 ∈ CRing)
9 rlocaddval.s . . . 4 (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
10 eqid 2766 . . . . . 6 (mulGrp‘𝑅) = (mulGrp‘𝑅)
1110, 1mgpbas 20252 . . . . 5 𝐵 = (Base‘(mulGrp‘𝑅))
1211submss 18898 . . . 4 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆𝐵)
139, 12syl 18 . . 3 (𝜑𝑆𝐵)
141, 2, 3, 4, 5, 6, 7, 8, 13rlocbas 33619 . 2 (𝜑 → ((𝐵 × 𝑆) / ) = (Base‘𝐿))
15 eqidd 2767 . 2 (𝜑 → (+g𝐿) = (+g𝐿))
16 eqidd 2767 . 2 (𝜑 → (.r𝐿) = (.r𝐿))
17 eqid 2766 . . . 4 (Base‘𝐿) = (Base‘𝐿)
18 eqid 2766 . . . 4 (0g𝐿) = (0g𝐿)
19 eqid 2766 . . . 4 (+g𝐿) = (+g𝐿)
208crngringd 20359 . . . . . . . 8 (𝜑𝑅 ∈ Ring)
211, 2ring0cl 20382 . . . . . . . 8 (𝑅 ∈ Ring → (0g𝑅) ∈ 𝐵)
2220, 21syl 18 . . . . . . 7 (𝜑 → (0g𝑅) ∈ 𝐵)
23 eqid 2766 . . . . . . . . . 10 (1r𝑅) = (1r𝑅)
2410, 23ringidval 20296 . . . . . . . . 9 (1r𝑅) = (0g‘(mulGrp‘𝑅))
2524subm0cl 18900 . . . . . . . 8 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → (1r𝑅) ∈ 𝑆)
269, 25syl 18 . . . . . . 7 (𝜑 → (1r𝑅) ∈ 𝑆)
2722, 26opelxpd 5705 . . . . . 6 (𝜑 → ⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
287ovexi 7457 . . . . . . 7 ∈ V
2928ecelqsi 8776 . . . . . 6 (⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3027, 29syl 18 . . . . 5 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3130, 14eleqtrd 2868 . . . 4 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ (Base‘𝐿))
3214eleq2d 2852 . . . . . 6 (𝜑 → (𝑥 ∈ ((𝐵 × 𝑆) / ) ↔ 𝑥 ∈ (Base‘𝐿)))
3332biimpar 483 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐿)) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
34 simpr 490 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
3534oveq2d 7439 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
3620ad4antr 745 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Ring)
379ad4antr 745 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
3837, 12syl 18 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆𝐵)
39 simplr 781 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝑆)
4038, 39sseldd 3941 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝐵)
411, 3, 2, 36, 40ringlzd 20411 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · 𝑏) = (0g𝑅))
42 simpllr 788 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎𝐵)
431, 3, 23, 36, 42ringridmd 20388 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 · (1r𝑅)) = 𝑎)
4441, 43oveq12d 7441 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = ((0g𝑅)(+g𝑅)𝑎))
45 eqid 2766 . . . . . . . . . . . 12 (+g𝑅) = (+g𝑅)
4636ringgrpd 20355 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Grp)
471, 45, 2, 46, 42grplidd 19067 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(+g𝑅)𝑎) = 𝑎)
4844, 47eqtrd 2801 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = 𝑎)
491, 3, 23, 36, 40ringlidmd 20387 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑏) = 𝑏)
5048, 49opeq12d 4851 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
5150eceq1d 8744 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
528ad4antr 745 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ CRing)
5322ad4antr 745 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (0g𝑅) ∈ 𝐵)
5437, 25syl 18 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝑆)
551, 3, 45, 6, 7, 52, 37, 53, 42, 54, 39, 19rlocaddval 33620 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] )
5651, 55, 343eqtr4d 2811 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
5735, 56eqtrd 2801 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
58 simpr 490 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
5958elrlocbasi 33618 . . . . . 6 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
6057, 59r19.29vva 3228 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
6133, 60syldan 603 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
62 rlocaddval.3 . . . . . . . 8 + = (+g𝑅)
631, 3, 62, 6, 7, 52, 37, 42, 53, 39, 54, 19rlocaddval 33620 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
6434oveq1d 7438 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ))
6543, 41oveq12d 7441 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)) = (𝑎 + (0g𝑅)))
661, 62, 2, 46, 42grpridd 19068 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 + (0g𝑅)) = 𝑎)
6765, 66eqtr2d 2802 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)))
681, 3, 23, 36, 40ringridmd 20388 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · (1r𝑅)) = 𝑏)
6968eqcomd 2772 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏 = (𝑏 · (1r𝑅)))
7067, 69opeq12d 4851 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩)
7170eceq1d 8744 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7234, 71eqtrd 2801 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7363, 64, 723eqtr4d 2811 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7473, 59r19.29vva 3228 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7533, 74syldan 603 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7617, 18, 19, 31, 61, 75ismgmid2 18752 . . 3 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] = (0g𝐿))
77 simp-4r 796 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
78 simpr 490 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
7977, 78oveq12d 7441 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
808ad8antr 753 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ CRing)
819ad8antr 753 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
82 simp-6r 800 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑎𝐵)
83 simpllr 788 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑐𝐵)
84 simp-5r 798 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝑆)
85 simplr 781 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝑆)
861, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 19rlocaddval 33620 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
8780crnggrpd 20360 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Grp)
8820ad8antr 753 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Ring)
8981, 12syl 18 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆𝐵)
9089, 85sseldd 3941 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝐵)
911, 3, 88, 82, 90ringcld 20370 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
9289, 84sseldd 3941 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝐵)
931, 3, 88, 83, 92ringcld 20370 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
941, 62, 87, 91, 93grpcld 19045 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
9510, 3mgpplusg 20251 . . . . . . . . . . . 12 · = (+g‘(mulGrp‘𝑅))
9695, 81, 84, 85submcld 18902 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
9794, 96opelxpd 5705 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
9828ecelqsi 8776 . . . . . . . . . 10 (⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
9997, 98syl 18 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
10086, 99eqeltrd 2866 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
10179, 100eqeltrd 2866 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
102 simp-4r 796 . . . . . . . 8 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
103102elrlocbasi 33618 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
104101, 103r19.29vva 3228 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
105 simplr 781 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
106105elrlocbasi 33618 . . . . . 6 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
107104, 106r19.29vva 3228 . . . . 5 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1081073impa 1127 . . . 4 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1098ad10antr 757 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ CRing)
110109crnggrpd 20360 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Grp)
11120ad10antr 757 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Ring)
112 simp-9r 806 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑎𝐵)
1139ad10antr 757 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
114113, 12syl 18 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆𝐵)
115 simp-5r 798 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝑆)
116114, 115sseldd 3941 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝐵)
1171, 3, 111, 112, 116ringcld 20370 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
118 simplr 781 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝑆)
119114, 118sseldd 3941 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝐵)
1201, 3, 111, 117, 119ringcld 20370 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) ∈ 𝐵)
121 simp-6r 800 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑐𝐵)
122 simp-8r 804 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝑆)
123114, 122sseldd 3941 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝐵)
1241, 3, 111, 121, 123ringcld 20370 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
1251, 3, 111, 124, 119ringcld 20370 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) ∈ 𝐵)
126 simpllr 788 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑒𝐵)
1271, 3, 111, 123, 116ringcld 20370 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝐵)
1281, 3, 111, 126, 127ringcld 20370 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) ∈ 𝐵)
1291, 62, 110, 120, 125, 128grpassd 19043 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))))
1301, 3, 111, 112, 116, 119ringassd 20371 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) = (𝑎 · (𝑑 · 𝑓)))
1311, 3, 109, 121, 123, 119crng32d 20373 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) = ((𝑐 · 𝑓) · 𝑏))
1321, 3, 109, 126, 123, 116crng12d 20372 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = (𝑏 · (𝑒 · 𝑑)))
1331, 3, 111, 126, 116ringcld 20370 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · 𝑑) ∈ 𝐵)
1341, 3, 109, 123, 133crngcomd 20368 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑒 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
135132, 134eqtrd 2801 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
136131, 135oveq12d 7441 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
137130, 136oveq12d 7441 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
138129, 137eqtrd 2801 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
1391, 62, 3, 111, 117, 124, 119ringdird 20378 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) = (((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)))
140139oveq1d 7438 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))))
1411, 3, 111, 121, 119ringcld 20370 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑓) ∈ 𝐵)
1421, 62, 3, 111, 141, 133, 123ringdird 20378 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
143142oveq2d 7439 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
144138, 140, 1433eqtr4d 2811 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)))
1451, 3, 111, 123, 116, 119ringassd 20371 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑏 · (𝑑 · 𝑓)))
146144, 145opeq12d 4851 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩)
147146eceq1d 8744 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
1481, 62, 110, 117, 124grpcld 19045 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
14995, 113, 122, 115submcld 18902 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
1501, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 19rlocaddval 33620 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] )
1511, 62, 110, 141, 133grpcld 19045 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑓) + (𝑒 · 𝑑)) ∈ 𝐵)
15295, 113, 115, 118submcld 18902 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑑 · 𝑓) ∈ 𝑆)
1531, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 19rlocaddval 33620 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
154147, 150, 1533eqtr4d 2811 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
1551, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 19rlocaddval 33620 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
156155oveq1d 7438 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
1571, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 19rlocaddval 33620 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] )
158157oveq2d 7439 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
159154, 156, 1583eqtr4d 2811 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
160 simp-7r 802 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
161 simp-4r 796 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
162160, 161oveq12d 7441 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
163 simpr 490 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑧 = [⟨𝑒, 𝑓⟩] )
164162, 163oveq12d 7441 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ))
165161, 163oveq12d 7441 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(+g𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
166160, 165oveq12d 7441 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
167159, 164, 1663eqtr4d 2811 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
168 simpr3 1215 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
169168ad6antr 749 . . . . . . . 8 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
170169elrlocbasi 33618 . . . . . . 7 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ∃𝑒𝐵𝑓𝑆 𝑧 = [⟨𝑒, 𝑓⟩] )
171167, 170r19.29vva 3228 . . . . . 6 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
172 simpr2 1214 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
173172ad3antrrr 743 . . . . . . 7 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
174173elrlocbasi 33618 . . . . . 6 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
175171, 174r19.29vva 3228 . . . . 5 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
176 simpr1 1213 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
177176elrlocbasi 33618 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
178175, 177r19.29vva 3228 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
17914, 15, 108, 178, 30, 60, 74ismndd 18843 . . 3 (𝜑𝐿 ∈ Mnd)
180 eqid 2766 . . . . . . . 8 (invg𝑅) = (invg𝑅)
1811, 180, 46, 42grpinvcld 19086 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((invg𝑅)‘𝑎) ∈ 𝐵)
182181, 39opelxpd 5705 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆))
18328ecelqsi 8776 . . . . . 6 (⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
184182, 183syl 18 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
185 simpr 490 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] )
186 simplr 781 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
187185, 186oveq12d 7441 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → (𝑢(+g𝐿)𝑥) = ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
188187eqeq1d 2768 . . . . 5 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → ((𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] ↔ ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] ))
1891, 3, 62, 6, 7, 52, 37, 181, 42, 39, 39, 19rlocaddval 33620 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] )
1901, 62, 2, 180, 46, 42grplinvd 19092 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((invg𝑅)‘𝑎) + 𝑎) = (0g𝑅))
191190oveq1d 7438 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((0g𝑅) · 𝑏))
1921, 62, 3, 36, 181, 42, 40ringdird 20378 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)))
193191, 192, 413eqtr3d 2809 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)) = (0g𝑅))
194193opeq1d 4849 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
195194eceq1d 8744 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (𝑏 · 𝑏)⟩] )
1961, 2, 23, 3, 4, 5, 7, 8, 9erler 33616 . . . . . . . 8 (𝜑 Er (𝐵 × 𝑆))
197196ad4antr 745 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → Er (𝐵 × 𝑆))
198 eqidd 2767 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
199 eqidd 2767 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (1r𝑅)⟩ = ⟨(0g𝑅), (1r𝑅)⟩)
20095, 37, 39, 39submcld 18902 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝑆)
2011, 3, 23, 36, 53ringridmd 20388 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (1r𝑅)) = (0g𝑅))
20238, 200sseldd 3941 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝐵)
2031, 3, 2, 36, 202ringlzd 20411 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (𝑏 · 𝑏)) = (0g𝑅))
204201, 203oveq12d 7441 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = ((0g𝑅)(-g𝑅)(0g𝑅)))
2051, 2, 4grpsubid 19121 . . . . . . . . . . . 12 ((𝑅 ∈ Grp ∧ (0g𝑅) ∈ 𝐵) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
20646, 53, 205syl2anc 596 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
207204, 206eqtrd 2801 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = (0g𝑅))
208207oveq2d 7439 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = ((𝑏 · 𝑏) · (0g𝑅)))
2091, 3, 2, 36, 202ringrzd 20412 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (0g𝑅)) = (0g𝑅))
210208, 209eqtrd 2801 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = (0g𝑅))
2111, 7, 38, 2, 3, 4, 198, 199, 53, 53, 200, 54, 200, 210erlbrd 33614 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ ⟨(0g𝑅), (1r𝑅)⟩)
212197, 211erthi 8760 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(0g𝑅), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (1r𝑅)⟩] )
213189, 195, 2123eqtrd 2805 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] )
214184, 188, 213rspcedvd 3586 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
215214, 59r19.29vva 3228 . . 3 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
21614, 15, 76, 179, 215isgrpd2e 19053 . 2 (𝜑𝐿 ∈ Grp)
21777, 78oveq12d 7441 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
218 eqid 2766 . . . . . . . 8 (.r𝐿) = (.r𝐿)
2191, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 218rlocmulval 33621 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
2201, 3, 88, 82, 83ringcld 20370 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
221220, 96opelxpd 5705 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
22228ecelqsi 8776 . . . . . . . 8 (⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
223221, 222syl 18 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
224219, 223eqeltrd 2866 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
225217, 224eqeltrd 2866 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
226225, 103r19.29vva 3228 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
227226, 106r19.29vva 3228 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2282273impa 1127 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2291, 3, 111, 112, 121, 126ringassd 20371 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · 𝑒) = (𝑎 · (𝑐 · 𝑒)))
230229, 145opeq12d 4851 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩)
231230eceq1d 8744 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
2321, 3, 111, 112, 121ringcld 20370 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
2331, 3, 62, 6, 7, 109, 113, 232, 126, 149, 118, 218rlocmulval 33621 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
2341, 3, 111, 121, 126ringcld 20370 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑒) ∈ 𝐵)
2351, 3, 62, 6, 7, 109, 113, 112, 234, 122, 152, 218rlocmulval 33621 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
236231, 233, 2353eqtr4d 2811 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
2371, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 218rlocmulval 33621 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
238237oveq1d 7438 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
2391, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 218rlocmulval 33621 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] )
240239oveq2d 7439 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
241236, 238, 2403eqtr4d 2811 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
242160, 161oveq12d 7441 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
243242, 163oveq12d 7441 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
244161, 163oveq12d 7441 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(.r𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
245160, 244oveq12d 7441 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
246241, 243, 2453eqtr4d 2811 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
247246, 170r19.29vva 3228 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
248247, 174r19.29vva 3228 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
249248, 177r19.29vva 3228 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
250196ad10antr 757 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → Er (𝐵 × 𝑆))
251 eqidd 2767 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ = ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩)
2521, 3, 111, 112, 123ringcld 20370 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑏) ∈ 𝐵)
2531, 62, 3, 111, 252, 141, 133ringdid 20377 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2541, 3, 111, 112, 123, 151ringassd 20371 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
255253, 254eqtr3d 2803 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
25610crngmgp 20354 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
2578, 256syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
258257ad10antr 757 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (mulGrp‘𝑅) ∈ CMnd)
25911, 95, 258, 112, 121, 123, 119cmn4d 33383 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · (𝑏 · 𝑓)) = ((𝑎 · 𝑏) · (𝑐 · 𝑓)))
26011, 95, 258, 112, 126, 123, 116cmn4d 33383 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑏 · 𝑑)) = ((𝑎 · 𝑏) · (𝑒 · 𝑑)))
261259, 260oveq12d 7441 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2621, 3, 109, 123, 112, 151crng12d 20372 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
263255, 261, 2623eqtr4d 2811 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
2641, 3, 109, 127, 123, 119crng12d 20372 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · ((𝑏 · 𝑑) · 𝑓)))
265145oveq2d 7439 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · ((𝑏 · 𝑑) · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
266264, 265eqtrd 2801 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
267263, 266opeq12d 4851 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩ = ⟨(𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))), (𝑏 · (𝑏 · (𝑑 · 𝑓)))⟩)
2681, 3, 111, 112, 151ringcld 20370 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) ∈ 𝐵)
2691, 3, 111, 123, 268ringcld 20370 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) ∈ 𝐵)
27095, 113, 122, 152submcld 18902 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑑 · 𝑓)) ∈ 𝑆)
27195, 113, 122, 270submcld 18902 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) ∈ 𝑆)
272 eqidd 2767 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
273 eqidd 2767 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
2741, 7, 109, 113, 3, 251, 267, 268, 269, 270, 271, 122, 272, 273erlbr2d 33615 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩)
275250, 274erthi 8760 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
2761, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 218rlocmulval 33621 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] )
2771, 3, 111, 112, 126ringcld 20370 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑒) ∈ 𝐵)
27895, 113, 122, 118submcld 18902 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝑆)
2791, 3, 62, 6, 7, 109, 113, 232, 277, 149, 278, 19rlocaddval 33620 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
280275, 276, 2793eqtr4d 2811 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
281157oveq2d 7439 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
2821, 3, 62, 6, 7, 109, 113, 112, 126, 122, 118, 218rlocmulval 33621 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] )
283237, 282oveq12d 7441 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
284280, 281, 2833eqtr4d 2811 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
285160, 165oveq12d 7441 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
286160, 163oveq12d 7441 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑧) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
287242, 286oveq12d 7441 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
288284, 285, 2873eqtr4d 2811 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
289288, 170r19.29vva 3228 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
290289, 174r19.29vva 3228 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
291290, 177r19.29vva 3228 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
2921, 62, 3, 111, 117, 124, 126ringdird 20378 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒) = (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)))
293292opeq1d 4849 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)), ((𝑏 · 𝑑) · 𝑓)⟩)
2941, 3, 111, 117, 126, 119ringassd 20371 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) · 𝑓) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
2951, 3, 111, 117, 126ringcld 20370 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑒) ∈ 𝐵)
2961, 3, 109, 119, 295crngcomd 20368 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑎 · 𝑑) · 𝑒)) = (((𝑎 · 𝑑) · 𝑒) · 𝑓))
29711, 95, 258, 112, 126, 116, 119cmn4d 33383 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
298294, 296, 2973eqtr4rd 2812 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = (𝑓 · ((𝑎 · 𝑑) · 𝑒)))
2991, 3, 111, 124, 126, 119ringassd 20371 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑒) · 𝑓) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
3001, 3, 111, 124, 126ringcld 20370 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑒) ∈ 𝐵)
3011, 3, 109, 119, 300crngcomd 20368 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑐 · 𝑏) · 𝑒)) = (((𝑐 · 𝑏) · 𝑒) · 𝑓))
30211, 95, 258, 121, 126, 123, 119cmn4d 33383 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
303299, 301, 3023eqtr4rd 2812 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = (𝑓 · ((𝑐 · 𝑏) · 𝑒)))
304298, 303oveq12d 7441 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
3051, 62, 3, 111, 119, 295, 300ringdid 20377 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
306304, 305eqtr4d 2804 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
307114, 278sseldd 3941 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝐵)
3081, 3, 111, 116, 307, 119ringassd 20371 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · (𝑏 · 𝑓)) · 𝑓) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
3091, 3, 109, 123, 116crngcomd 20368 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
310309oveq1d 7438 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = ((𝑑 · 𝑏) · 𝑓))
3111, 3, 111, 116, 123, 119ringassd 20371 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · 𝑏) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
312310, 311eqtrd 2801 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
313312oveq1d 7438 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = ((𝑑 · (𝑏 · 𝑓)) · 𝑓))
3141, 3, 109, 307, 116, 119crng12d 20372 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
315308, 313, 3143eqtr4rd 2812 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (((𝑏 · 𝑑) · 𝑓) · 𝑓))
316306, 315opeq12d 4851 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩ = ⟨(𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))), (((𝑏 · 𝑑) · 𝑓) · 𝑓)⟩)
3171, 62, 110, 295, 300grpcld 19045 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)) ∈ 𝐵)
3181, 3, 111, 119, 317ringcld 20370 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) ∈ 𝐵)
319145, 270eqeltrd 2866 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝑆)
32095, 113, 319, 118submcld 18902 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) ∈ 𝑆)
321 eqidd 2767 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
322114, 319sseldd 3941 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝐵)
3231, 3, 109, 322, 119crngcomd 20368 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = (𝑓 · ((𝑏 · 𝑑) · 𝑓)))
3241, 7, 109, 113, 3, 293, 316, 317, 318, 319, 320, 118, 321, 323erlbr2d 33615 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩)
325250, 324erthi 8760 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
3261, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 218rlocmulval 33621 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
3271, 3, 62, 6, 7, 109, 113, 277, 234, 278, 152, 19rlocaddval 33620 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
328325, 326, 3273eqtr4d 2811 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
329155oveq1d 7438 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
330282, 239oveq12d 7441 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
331328, 329, 3303eqtr4d 2811 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
332162, 163oveq12d 7441 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
333286, 244oveq12d 7441 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
334331, 332, 3333eqtr4d 2811 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
335334, 170r19.29vva 3228 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
336335, 174r19.29vva 3228 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
337336, 177r19.29vva 3228 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
33813, 26sseldd 3941 . . . 4 (𝜑 → (1r𝑅) ∈ 𝐵)
339338, 26opelxpd 5705 . . 3 (𝜑 → ⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
34028ecelqsi 8776 . . 3 (⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
341339, 340syl 18 . 2 (𝜑 → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
34234oveq2d 7439 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
3431, 3, 23, 36, 42ringlidmd 20387 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑎) = 𝑎)
344343, 49opeq12d 4851 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
345344eceq1d 8744 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
34638, 54sseldd 3941 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝐵)
3471, 3, 62, 6, 7, 52, 37, 346, 42, 54, 39, 218rlocmulval 33621 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] )
348345, 347, 343eqtr4d 2811 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
349342, 348eqtrd 2801 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
350349, 59r19.29vva 3228 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
3511, 3, 62, 6, 7, 52, 37, 42, 346, 39, 54, 218rlocmulval 33621 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
35234oveq1d 7438 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ))
35343eqcomd 2772 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = (𝑎 · (1r𝑅)))
354353, 69opeq12d 4851 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩)
355354eceq1d 8744 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
356351, 352, 3553eqtr4d 2811 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨𝑎, 𝑏⟩] )
357356, 34eqtr4d 2804 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
358357, 59r19.29vva 3228 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
3591, 3, 80, 82, 83crngcomd 20368 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) = (𝑐 · 𝑎))
3601, 3, 80, 92, 90crngcomd 20368 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
361359, 360opeq12d 4851 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ = ⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩)
362361eceq1d 8744 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
3631, 3, 62, 6, 7, 80, 81, 83, 82, 85, 84, 218rlocmulval 33621 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
364362, 219, 3633eqtr4d 2811 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
36578, 77oveq12d 7441 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑦(.r𝐿)𝑥) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
366364, 217, 3653eqtr4d 2811 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
367366, 103r19.29vva 3228 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
368367, 106r19.29vva 3228 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
3693683impa 1127 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
37014, 15, 16, 216, 228, 249, 291, 337, 341, 350, 358, 369iscrngd 20408 1 (𝜑𝐿 ∈ CRing)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wa 401  w3a 1103   = wceq 1570  wcel 2146  wrex 3092  wss 3908  cop 4600   × cxp 5664  cfv 6543  (class class class)co 7423   Er wer 8700  [cec 8701   / cqs 8702  Basecbs 17294  +gcplusg 17335  .rcmulr 17336  0gc0g 17517  SubMndcsubmnd 18871  Grpcgrp 19031  invgcminusg 19032  -gcsg 19033  CMndccmn 19881  mulGrpcmgp 20247  1rcur 20294  Ringcrg 20346  CRingccrg 20347   ~RL cerl 33604   RLocal crloc 33605
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8703  df-ec 8705  df-qs 8709  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-sup 9412  df-inf 9413  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-nn 12252  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12523  df-z 12610  df-dec 12730  df-uz 12881  df-fz 13554  df-struct 17232  df-sets 17249  df-slot 17267  df-ndx 17279  df-base 17295  df-ress 17316  df-plusg 17348  df-mulr 17349  df-sca 17351  df-vsca 17352  df-ip 17353  df-tset 17354  df-ple 17355  df-ds 17357  df-0g 17519  df-imas 17587  df-qus 17588  df-mgm 18723  df-sgrp 18806  df-mnd 18822  df-submnd 18873  df-grp 19034  df-minusg 19035  df-sbg 19036  df-cmn 19883  df-abl 19884  df-mgp 20248  df-rng 20262  df-ur 20295  df-ring 20348  df-cring 20349  df-erl 33606  df-rloc 33607
This theorem is used by:  rloc0g  33623  rloc1r  33624  rlocf1  33625  rlocinvunit  33626  rlocisunit  33627  fracfld  33660
  Copyright terms: Public domain W3C validator