Metamath Proof Explorer

Theorem qusmnd

Description: Prove that a quotient structure is a monoid. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses qusmnd.u 
|- ( ph -> U = ( R /s .~ ) )
qusmnd.v 
|- ( ph -> V = ( Base ` R ) )
qusmnd.p 
|- .+ = ( +g ` R )
qusmnd.r 
|- ( ph -> .~ Er V )
qusmnd.x 
|- ( ph -> R e. X )
qusmnd.e 
|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )
qusmnd.1 
|- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
qusmnd.2 
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x .+ y ) .+ z ) .~ ( x .+ ( y .+ z ) ) )
qusmnd.3 
|- ( ph -> .0. e. V )
qusmnd.4 
|- ( ( ph /\ x e. V ) -> ( .0. .+ x ) .~ x )
qusmnd.5 
|- ( ( ph /\ x e. V ) -> ( x .+ .0. ) .~ x )
Assertion qusmnd 
|- ( ph -> ( U e. Mnd /\ [ .0. ] .~ = ( 0g ` U ) ) )

Proof

Step Hyp Ref Expression
1 qusmnd.u 
 |-  ( ph -> U = ( R /s .~ ) )
2 qusmnd.v 
 |-  ( ph -> V = ( Base ` R ) )
3 qusmnd.p 
 |-  .+ = ( +g ` R )
4 qusmnd.r 
 |-  ( ph -> .~ Er V )
5 qusmnd.x 
 |-  ( ph -> R e. X )
6 qusmnd.e 
 |-  ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )
7 qusmnd.1 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
8 qusmnd.2 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x .+ y ) .+ z ) .~ ( x .+ ( y .+ z ) ) )
9 qusmnd.3 
 |-  ( ph -> .0. e. V )
10 qusmnd.4 
 |-  ( ( ph /\ x e. V ) -> ( .0. .+ x ) .~ x )
11 qusmnd.5 
 |-  ( ( ph /\ x e. V ) -> ( x .+ .0. ) .~ x )
12 eqid 
 |-  ( u e. V |-> [ u ] .~ ) = ( u e. V |-> [ u ] .~ )
13 fvex 
 |-  ( Base ` R ) e. _V
14 2 13 eqeltrdi 
 |-  ( ph -> V e. _V )
15 erex 
 |-  ( .~ Er V -> ( V e. _V -> .~ e. _V ) )
16 4 14 15 sylc 
 |-  ( ph -> .~ e. _V )
17 1 2 12 16 5 qusval 
 |-  ( ph -> U = ( ( u e. V |-> [ u ] .~ ) "s R ) )
18 1 2 12 16 5 quslem 
 |-  ( ph -> ( u e. V |-> [ u ] .~ ) : V -onto-> ( V /. .~ ) )
19 7 3expb 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. V )
20 4 14 12 19 6 ercpbl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( ( u e. V |-> [ u ] .~ ) ` a ) = ( ( u e. V |-> [ u ] .~ ) ` p ) /\ ( ( u e. V |-> [ u ] .~ ) ` b ) = ( ( u e. V |-> [ u ] .~ ) ` q ) ) -> ( ( u e. V |-> [ u ] .~ ) ` ( a .+ b ) ) = ( ( u e. V |-> [ u ] .~ ) ` ( p .+ q ) ) ) )
21 4 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> .~ Er V )
22 21 8 erthi 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> [ ( ( x .+ y ) .+ z ) ] .~ = [ ( x .+ ( y .+ z ) ) ] .~ )
23 14 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> V e. _V )
24 21 23 12 divsfval 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( u e. V |-> [ u ] .~ ) ` ( ( x .+ y ) .+ z ) ) = [ ( ( x .+ y ) .+ z ) ] .~ )
25 21 23 12 divsfval 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( u e. V |-> [ u ] .~ ) ` ( x .+ ( y .+ z ) ) ) = [ ( x .+ ( y .+ z ) ) ] .~ )
26 22 24 25 3eqtr4d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( u e. V |-> [ u ] .~ ) ` ( ( x .+ y ) .+ z ) ) = ( ( u e. V |-> [ u ] .~ ) ` ( x .+ ( y .+ z ) ) ) )
27 4 adantr 
 |-  ( ( ph /\ x e. V ) -> .~ Er V )
28 27 10 erthi 
 |-  ( ( ph /\ x e. V ) -> [ ( .0. .+ x ) ] .~ = [ x ] .~ )
29 14 adantr 
 |-  ( ( ph /\ x e. V ) -> V e. _V )
30 27 29 12 divsfval 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` ( .0. .+ x ) ) = [ ( .0. .+ x ) ] .~ )
31 27 29 12 divsfval 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` x ) = [ x ] .~ )
32 28 30 31 3eqtr4d 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` ( .0. .+ x ) ) = ( ( u e. V |-> [ u ] .~ ) ` x ) )
33 27 11 erthi 
 |-  ( ( ph /\ x e. V ) -> [ ( x .+ .0. ) ] .~ = [ x ] .~ )
34 27 29 12 divsfval 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` ( x .+ .0. ) ) = [ ( x .+ .0. ) ] .~ )
35 33 34 31 3eqtr4d 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` ( x .+ .0. ) ) = ( ( u e. V |-> [ u ] .~ ) ` x ) )
36 17 2 3 18 20 5 7 26 9 32 35 imasmnd2 
 |-  ( ph -> ( U e. Mnd /\ ( ( u e. V |-> [ u ] .~ ) ` .0. ) = ( 0g ` U ) ) )
37 4 14 12 divsfval 
 |-  ( ph -> ( ( u e. V |-> [ u ] .~ ) ` .0. ) = [ .0. ] .~ )
38 37 eqcomd 
 |-  ( ph -> [ .0. ] .~ = ( ( u e. V |-> [ u ] .~ ) ` .0. ) )
39 38 eqeq1d 
 |-  ( ph -> ( [ .0. ] .~ = ( 0g ` U ) <-> ( ( u e. V |-> [ u ] .~ ) ` .0. ) = ( 0g ` U ) ) )
40 39 anbi2d 
 |-  ( ph -> ( ( U e. Mnd /\ [ .0. ] .~ = ( 0g ` U ) ) <-> ( U e. Mnd /\ ( ( u e. V |-> [ u ] .~ ) ` .0. ) = ( 0g ` U ) ) ) )
41 36 40 mpbird 
 |-  ( ph -> ( U e. Mnd /\ [ .0. ] .~ = ( 0g ` U ) ) )