Metamath Proof Explorer


Theorem islmod

Description: The predicate "is a left module". (Contributed by NM, 4-Nov-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses islmod.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
islmod.a โŠข + = ( +g โ€˜ ๐‘Š )
islmod.s โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
islmod.f โŠข ๐น = ( Scalar โ€˜ ๐‘Š )
islmod.k โŠข ๐พ = ( Base โ€˜ ๐น )
islmod.p โŠข โจฃ = ( +g โ€˜ ๐น )
islmod.t โŠข ร— = ( .r โ€˜ ๐น )
islmod.u โŠข 1 = ( 1r โ€˜ ๐น )
Assertion islmod ( ๐‘Š โˆˆ LMod โ†” ( ๐‘Š โˆˆ Grp โˆง ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) )

Proof

Step Hyp Ref Expression
1 islmod.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
2 islmod.a โŠข + = ( +g โ€˜ ๐‘Š )
3 islmod.s โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
4 islmod.f โŠข ๐น = ( Scalar โ€˜ ๐‘Š )
5 islmod.k โŠข ๐พ = ( Base โ€˜ ๐น )
6 islmod.p โŠข โจฃ = ( +g โ€˜ ๐น )
7 islmod.t โŠข ร— = ( .r โ€˜ ๐น )
8 islmod.u โŠข 1 = ( 1r โ€˜ ๐น )
9 fveq2 โŠข ( ๐‘” = ๐‘Š โ†’ ( Base โ€˜ ๐‘” ) = ( Base โ€˜ ๐‘Š ) )
10 9 1 eqtr4di โŠข ( ๐‘” = ๐‘Š โ†’ ( Base โ€˜ ๐‘” ) = ๐‘‰ )
11 fveq2 โŠข ( ๐‘” = ๐‘Š โ†’ ( +g โ€˜ ๐‘” ) = ( +g โ€˜ ๐‘Š ) )
12 11 2 eqtr4di โŠข ( ๐‘” = ๐‘Š โ†’ ( +g โ€˜ ๐‘” ) = + )
13 fveq2 โŠข ( ๐‘” = ๐‘Š โ†’ ( Scalar โ€˜ ๐‘” ) = ( Scalar โ€˜ ๐‘Š ) )
14 13 4 eqtr4di โŠข ( ๐‘” = ๐‘Š โ†’ ( Scalar โ€˜ ๐‘” ) = ๐น )
15 fveq2 โŠข ( ๐‘” = ๐‘Š โ†’ ( ยท๐‘  โ€˜ ๐‘” ) = ( ยท๐‘  โ€˜ ๐‘Š ) )
16 15 3 eqtr4di โŠข ( ๐‘” = ๐‘Š โ†’ ( ยท๐‘  โ€˜ ๐‘” ) = ยท )
17 16 sbceq1d โŠข ( ๐‘” = ๐‘Š โ†’ ( [ ( ยท๐‘  โ€˜ ๐‘” ) / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ ยท / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
18 14 17 sbceqbid โŠข ( ๐‘” = ๐‘Š โ†’ ( [ ( Scalar โ€˜ ๐‘” ) / ๐‘“ ] [ ( ยท๐‘  โ€˜ ๐‘” ) / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ ๐น / ๐‘“ ] [ ยท / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
19 12 18 sbceqbid โŠข ( ๐‘” = ๐‘Š โ†’ ( [ ( +g โ€˜ ๐‘” ) / ๐‘Ž ] [ ( Scalar โ€˜ ๐‘” ) / ๐‘“ ] [ ( ยท๐‘  โ€˜ ๐‘” ) / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ + / ๐‘Ž ] [ ๐น / ๐‘“ ] [ ยท / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
20 10 19 sbceqbid โŠข ( ๐‘” = ๐‘Š โ†’ ( [ ( Base โ€˜ ๐‘” ) / ๐‘ฃ ] [ ( +g โ€˜ ๐‘” ) / ๐‘Ž ] [ ( Scalar โ€˜ ๐‘” ) / ๐‘“ ] [ ( ยท๐‘  โ€˜ ๐‘” ) / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ ๐‘‰ / ๐‘ฃ ] [ + / ๐‘Ž ] [ ๐น / ๐‘“ ] [ ยท / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
21 1 fvexi โŠข ๐‘‰ โˆˆ V
22 2 fvexi โŠข + โˆˆ V
23 4 fvexi โŠข ๐น โˆˆ V
24 simp3 โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ๐‘“ = ๐น )
25 24 fveq2d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( Base โ€˜ ๐‘“ ) = ( Base โ€˜ ๐น ) )
26 25 5 eqtr4di โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( Base โ€˜ ๐‘“ ) = ๐พ )
27 24 fveq2d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( +g โ€˜ ๐‘“ ) = ( +g โ€˜ ๐น ) )
28 27 6 eqtr4di โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( +g โ€˜ ๐‘“ ) = โจฃ )
29 24 fveq2d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( .r โ€˜ ๐‘“ ) = ( .r โ€˜ ๐น ) )
30 29 7 eqtr4di โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( .r โ€˜ ๐‘“ ) = ร— )
31 30 sbceq1d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ ร— / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
32 7 fvexi โŠข ร— โˆˆ V
33 oveq โŠข ( ๐‘ก = ร— โ†’ ( ๐‘ž ๐‘ก ๐‘Ÿ ) = ( ๐‘ž ร— ๐‘Ÿ ) )
34 33 oveq1d โŠข ( ๐‘ก = ร— โ†’ ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) )
35 34 eqeq1d โŠข ( ๐‘ก = ร— โ†’ ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โ†” ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) )
36 35 anbi1d โŠข ( ๐‘ก = ร— โ†’ ( ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) โ†” ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) )
37 36 anbi2d โŠข ( ๐‘ก = ร— โ†’ ( ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
38 37 2ralbidv โŠข ( ๐‘ก = ร— โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
39 38 2ralbidv โŠข ( ๐‘ก = ร— โ†’ ( โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
40 39 anbi2d โŠข ( ๐‘ก = ร— โ†’ ( ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
41 32 40 sbcie โŠข ( [ ร— / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
42 24 eleq1d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ๐‘“ โˆˆ Ring โ†” ๐น โˆˆ Ring ) )
43 simp1 โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ๐‘ฃ = ๐‘‰ )
44 43 eleq2d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โ†” ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ ) )
45 simp2 โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ๐‘Ž = + )
46 45 oveqd โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ๐‘ค ๐‘Ž ๐‘ฅ ) = ( ๐‘ค + ๐‘ฅ ) )
47 46 oveq2d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) )
48 45 oveqd โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) )
49 47 48 eqeq12d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โ†” ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) ) )
50 45 oveqd โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) )
51 50 eqeq2d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โ†” ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) )
52 44 49 51 3anbi123d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โ†” ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) ) )
53 24 fveq2d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( 1r โ€˜ ๐‘“ ) = ( 1r โ€˜ ๐น ) )
54 53 8 eqtr4di โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( 1r โ€˜ ๐‘“ ) = 1 )
55 54 oveq1d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ( 1 ๐‘  ๐‘ค ) )
56 55 eqeq1d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค โ†” ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) )
57 56 anbi2d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) โ†” ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) )
58 52 57 anbi12d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
59 43 58 raleqbidv โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
60 43 59 raleqbidv โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
61 60 2ralbidv โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
62 42 61 anbi12d โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
63 41 62 bitrid โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( [ ร— / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
64 31 63 bitrd โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
65 28 64 sbceqbid โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ โจฃ / ๐‘ ] ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
66 26 65 sbceqbid โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ ๐พ / ๐‘˜ ] [ โจฃ / ๐‘ ] ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
67 66 sbcbidv โŠข ( ( ๐‘ฃ = ๐‘‰ โˆง ๐‘Ž = + โˆง ๐‘“ = ๐น ) โ†’ ( [ ยท / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ ยท / ๐‘  ] [ ๐พ / ๐‘˜ ] [ โจฃ / ๐‘ ] ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) ) )
68 21 22 23 67 sbc3ie โŠข ( [ ๐‘‰ / ๐‘ฃ ] [ + / ๐‘Ž ] [ ๐น / ๐‘“ ] [ ยท / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” [ ยท / ๐‘  ] [ ๐พ / ๐‘˜ ] [ โจฃ / ๐‘ ] ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) )
69 3 fvexi โŠข ยท โˆˆ V
70 5 fvexi โŠข ๐พ โˆˆ V
71 6 fvexi โŠข โจฃ โˆˆ V
72 simp2 โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ๐‘˜ = ๐พ )
73 simp1 โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ๐‘  = ยท )
74 73 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ๐‘Ÿ ๐‘  ๐‘ค ) = ( ๐‘Ÿ ยท ๐‘ค ) )
75 74 eleq1d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โ†” ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ ) )
76 73 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) )
77 73 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ๐‘Ÿ ๐‘  ๐‘ฅ ) = ( ๐‘Ÿ ยท ๐‘ฅ ) )
78 74 77 oveq12d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) )
79 76 78 eqeq12d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โ†” ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) ) )
80 simp3 โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ๐‘ = โจฃ )
81 80 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ๐‘ž ๐‘ ๐‘Ÿ ) = ( ๐‘ž โจฃ ๐‘Ÿ ) )
82 81 oveq1d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž โจฃ ๐‘Ÿ ) ๐‘  ๐‘ค ) )
83 73 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐‘ž โจฃ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) )
84 82 83 eqtrd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) )
85 73 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ๐‘ž ๐‘  ๐‘ค ) = ( ๐‘ž ยท ๐‘ค ) )
86 85 74 oveq12d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) )
87 84 86 eqeq12d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โ†” ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) )
88 75 79 87 3anbi123d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โ†” ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) ) )
89 73 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) )
90 74 oveq2d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ยท ๐‘ค ) ) )
91 73 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ๐‘ž ๐‘  ( ๐‘Ÿ ยท ๐‘ค ) ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) )
92 90 91 eqtrd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) )
93 89 92 eqeq12d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โ†” ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) ) )
94 73 oveqd โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( 1 ๐‘  ๐‘ค ) = ( 1 ยท ๐‘ค ) )
95 94 eqeq1d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( 1 ๐‘  ๐‘ค ) = ๐‘ค โ†” ( 1 ยท ๐‘ค ) = ๐‘ค ) )
96 93 95 anbi12d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) โ†” ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) )
97 88 96 anbi12d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) )
98 97 2ralbidv โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) )
99 72 98 raleqbidv โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) )
100 72 99 raleqbidv โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) โ†” โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) )
101 100 anbi2d โŠข ( ( ๐‘  = ยท โˆง ๐‘˜ = ๐พ โˆง ๐‘ = โจฃ ) โ†’ ( ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) ) )
102 69 70 71 101 sbc3ie โŠข ( [ ยท / ๐‘  ] [ ๐พ / ๐‘˜ ] [ โจฃ / ๐‘ ] ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) + ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( 1 ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) )
103 68 102 bitri โŠข ( [ ๐‘‰ / ๐‘ฃ ] [ + / ๐‘Ž ] [ ๐น / ๐‘“ ] [ ยท / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) )
104 20 103 bitrdi โŠข ( ๐‘” = ๐‘Š โ†’ ( [ ( Base โ€˜ ๐‘” ) / ๐‘ฃ ] [ ( +g โ€˜ ๐‘” ) / ๐‘Ž ] [ ( Scalar โ€˜ ๐‘” ) / ๐‘“ ] [ ( ยท๐‘  โ€˜ ๐‘” ) / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) ) )
105 df-lmod โŠข LMod = { ๐‘” โˆˆ Grp โˆฃ [ ( Base โ€˜ ๐‘” ) / ๐‘ฃ ] [ ( +g โ€˜ ๐‘” ) / ๐‘Ž ] [ ( Scalar โ€˜ ๐‘” ) / ๐‘“ ] [ ( ยท๐‘  โ€˜ ๐‘” ) / ๐‘  ] [ ( Base โ€˜ ๐‘“ ) / ๐‘˜ ] [ ( +g โ€˜ ๐‘“ ) / ๐‘ ] [ ( .r โ€˜ ๐‘“ ) / ๐‘ก ] ( ๐‘“ โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐‘˜ โˆ€ ๐‘Ÿ โˆˆ ๐‘˜ โˆ€ ๐‘ฅ โˆˆ ๐‘ฃ โˆ€ ๐‘ค โˆˆ ๐‘ฃ ( ( ( ๐‘Ÿ ๐‘  ๐‘ค ) โˆˆ ๐‘ฃ โˆง ( ๐‘Ÿ ๐‘  ( ๐‘ค ๐‘Ž ๐‘ฅ ) ) = ( ( ๐‘Ÿ ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ฅ ) ) โˆง ( ( ๐‘ž ๐‘ ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ( ๐‘ž ๐‘  ๐‘ค ) ๐‘Ž ( ๐‘Ÿ ๐‘  ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ๐‘ก ๐‘Ÿ ) ๐‘  ๐‘ค ) = ( ๐‘ž ๐‘  ( ๐‘Ÿ ๐‘  ๐‘ค ) ) โˆง ( ( 1r โ€˜ ๐‘“ ) ๐‘  ๐‘ค ) = ๐‘ค ) ) ) }
106 104 105 elrab2 โŠข ( ๐‘Š โˆˆ LMod โ†” ( ๐‘Š โˆˆ Grp โˆง ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) ) )
107 3anass โŠข ( ( ๐‘Š โˆˆ Grp โˆง ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) โ†” ( ๐‘Š โˆˆ Grp โˆง ( ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) ) )
108 106 107 bitr4i โŠข ( ๐‘Š โˆˆ LMod โ†” ( ๐‘Š โˆˆ Grp โˆง ๐น โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ๐พ โˆ€ ๐‘Ÿ โˆˆ ๐พ โˆ€ ๐‘ฅ โˆˆ ๐‘‰ โˆ€ ๐‘ค โˆˆ ๐‘‰ ( ( ( ๐‘Ÿ ยท ๐‘ค ) โˆˆ ๐‘‰ โˆง ( ๐‘Ÿ ยท ( ๐‘ค + ๐‘ฅ ) ) = ( ( ๐‘Ÿ ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ž โจฃ ๐‘Ÿ ) ยท ๐‘ค ) = ( ( ๐‘ž ยท ๐‘ค ) + ( ๐‘Ÿ ยท ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ร— ๐‘Ÿ ) ยท ๐‘ค ) = ( ๐‘ž ยท ( ๐‘Ÿ ยท ๐‘ค ) ) โˆง ( 1 ยท ๐‘ค ) = ๐‘ค ) ) ) )