RMOD_3

:: RMOD_3 semantic presentation

begin

definition

func W1 + W2 -> ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( ) ( ) 1-sorted ) ) means :: RMOD_3:def 1
the carrier of it : ( ( ) ( ) Element of W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) = { (v : ( ( ) ( ) Vector of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) where v, u is ( ( ) ( ) Vector of ( ( ) ( ) set ) ) : ( v : ( ( ) ( ) Vector of ( ( ) ( non empty ) set ) ) in W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) & u : ( ( ) ( ) Vector of ( ( ) ( non empty ) set ) ) in W2 : ( ( Function-like V18([:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) ) ( Relation-like [:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) -defined W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) -valued Function-like V18([:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) } ;

end;

definition

func W1 /\ W2 -> ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( ) ( ) 1-sorted ) ) means :: RMOD_3:def 2
the carrier of it : ( ( ) ( ) Element of W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) = the carrier of W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) /\ the carrier of W2 : ( ( Function-like V18([:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) ) ( Relation-like [:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) -defined W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) -valued Function-like V18([:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

end;

theorem :: RMOD_3:1

theorem :: RMOD_3:2

theorem :: RMOD_3:3

theorem :: RMOD_3:4

theorem :: RMOD_3:5

theorem :: RMOD_3:6

theorem :: RMOD_3:7

theorem :: RMOD_3:8

theorem :: RMOD_3:9

theorem :: RMOD_3:10

theorem :: RMOD_3:11

for R being ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring)
for V being ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) )
for W being ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) holds
( ((Omega). V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) + W : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) = RightModStr(# the carrier of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the U7 of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( Function-like V18([: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the ZeroF of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) , the rmult of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( Function-like V18([: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RightModStr over b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) & W : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) + ((Omega). V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) = RightModStr(# the carrier of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the U7 of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( Function-like V18([: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the ZeroF of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) , the rmult of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( Function-like V18([: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₂ : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RightModStr over b₁ : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) ;

theorem :: RMOD_3:12

theorem :: RMOD_3:13

theorem :: RMOD_3:14

theorem :: RMOD_3:15

theorem :: RMOD_3:16

theorem :: RMOD_3:17

theorem :: RMOD_3:18

theorem :: RMOD_3:19

theorem :: RMOD_3:20

theorem :: RMOD_3:21

theorem :: RMOD_3:22

theorem :: RMOD_3:23

theorem :: RMOD_3:24

theorem :: RMOD_3:25

theorem :: RMOD_3:26

theorem :: RMOD_3:27

theorem :: RMOD_3:28

theorem :: RMOD_3:29

theorem :: RMOD_3:30

theorem :: RMOD_3:31

theorem :: RMOD_3:32

theorem :: RMOD_3:33

theorem :: RMOD_3:34

theorem :: RMOD_3:35

theorem :: RMOD_3:36

definition

func Submodules V -> ( ( ) ( ) set ) means :: RMOD_3:def 3
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) iff ex W being ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( ) ( ) 1-sorted ) ) st W : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) = x : ( ( ) ( ) set ) );

end;

registration

cluster Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightModStr over R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) L14()) ) : ( ( ) ( ) set ) -> non empty ;

end;

theorem :: RMOD_3:37

definition

pred V is_the_direct_sum_of W1,W2 means :: RMOD_3:def 4
( RightModStr(# the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the U7 of V : ( ( ) ( ) set ) : ( ( Function-like V18([: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) , the ZeroF of V : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) , the rmult of V : ( ( ) ( ) set ) : ( ( Function-like V18([: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RightModStr over R : ( ( ) ( ) set ) ) = W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) + W2 : ( ( Function-like V18([:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) ( Relation-like [:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) -defined W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) -valued Function-like V18([:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) Element of bool [:[:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( ) ( ) set ) ) & W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) /\ W2 : ( ( Function-like V18([:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) ( Relation-like [:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) -defined W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) -valued Function-like V18([:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) Element of bool [:[:W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,W1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( ) ( ) set ) ) = (0). V : ( ( ) ( ) set ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( ) ( ) set ) ) );

end;

theorem :: RMOD_3:38

theorem :: RMOD_3:39

theorem :: RMOD_3:40

theorem :: RMOD_3:41

theorem :: RMOD_3:42

theorem :: RMOD_3:43

theorem :: RMOD_3:44

definition

let R be ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ;
let V be ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ;
let v be ( ( ) ( ) Vector of ( ( ) ( non empty ) set ) ) ;
let W1, W2 be ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) ;
assume V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) is_the_direct_sum_of W1 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) ,W2 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) ;

func v |-- (W1,W2) -> ( ( ) ( ) Element of [: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) means :: RMOD_3:def 5
( v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) = (it : ( ( Function-like V18([: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) ( Relation-like [: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) -defined v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) -valued Function-like V18([: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) Element of bool [:[: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) + (it : ( ( Function-like V18([: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) ( Relation-like [: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) -defined v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) -valued Function-like V18([: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) Element of bool [:[: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & it : ( ( Function-like V18([: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) ( Relation-like [: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) -defined v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) -valued Function-like V18([: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) Element of bool [:[: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) in W1 : ( ( Function-like V18([:v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) ( Relation-like [:v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) -defined v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) -valued Function-like V18([:v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) Element of bool [:[:v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & it : ( ( Function-like V18([: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) ( Relation-like [: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) -defined v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) -valued Function-like V18([: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ) Element of bool [:[: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) in W2 : ( ( ) ( ) Element of v : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) );

end;

theorem :: RMOD_3:45

theorem :: RMOD_3:46

definition

func SubJoin V -> ( ( Function-like V18([:(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like [:(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V18([:(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) BinOp of Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) means :: RMOD_3:def 6
for A1, A2 being ( ( ) ( ) Element of Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) )
for W1, W2 being ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( ) ( ) set ) ) st A1 : ( ( ) ( ) Element of Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) = W1 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) & A2 : ( ( ) ( ) Element of Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) = W2 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) holds
it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) . (A1 : ( ( ) ( ) Element of Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ,A2 : ( ( ) ( ) Element of Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = W1 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) + W2 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( ) ( ) set ) ) ;

end;

definition

func SubMeet V -> ( ( Function-like V18([:(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like [:(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V18([:(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(Submodules V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) BinOp of Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) means :: RMOD_3:def 7
for A1, A2 being ( ( ) ( ) Element of Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) )
for W1, W2 being ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( ) ( ) set ) ) st A1 : ( ( ) ( ) Element of Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) = W1 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) & A2 : ( ( ) ( ) Element of Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) = W2 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) holds
it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) . (A1 : ( ( ) ( ) Element of Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ,A2 : ( ( ) ( ) Element of Submodules V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of Submodules V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = W1 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) /\ W2 : ( ( ) ( non empty V89() V136() V137() V138() RightMod-like ) Submodule of V : ( ( non empty V89() V136() V137() V138() RightMod-like ) ( non empty V89() V136() V137() V138() RightMod-like ) RightMod of R : ( ( non empty V89() V115() V122() V123() V136() V137() V138() ) ( non empty V89() V115() V122() V123() V136() V137() V138() ) Ring) ) ) : ( ( strict ) ( non empty V89() V136() V137() V138() strict RightMod-like ) Submodule of V : ( ( ) ( ) set ) ) ;

end;

theorem :: RMOD_3:47

theorem :: RMOD_3:48

theorem :: RMOD_3:49

theorem :: RMOD_3:50

theorem :: RMOD_3:51