Metamath Proof Explorer

Theorem zlmodzxzsub

Description: The subtraction of the ZZ-module ZZ X. ZZ . (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxz.z 
|- Z = ( ZZring freeLMod { 0 , 1 } )
zlmodzxzsub.m 
|- .- = ( -g ` Z )
Assertion zlmodzxzsub 
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } )

Proof

Step Hyp Ref Expression
1 zlmodzxz.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzsub.m 
 |-  .- = ( -g ` Z )
3 zsubcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )
4 simpr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. ZZ )
5 3 4 jca 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A - B ) e. ZZ /\ B e. ZZ ) )
6 zsubcl 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( C - D ) e. ZZ )
7 simpr 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> D e. ZZ )
8 6 7 jca 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( ( C - D ) e. ZZ /\ D e. ZZ ) )
9 eqid 
 |-  ( +g ` Z ) = ( +g ` Z )
10 1 9 zlmodzxzadd 
 |-  ( ( ( ( A - B ) e. ZZ /\ B e. ZZ ) /\ ( ( C - D ) e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } ( +g ` Z ) { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( ( A - B ) + B ) >. , <. 1 , ( ( C - D ) + D ) >. } )
11 5 8 10 syl2an 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } ( +g ` Z ) { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( ( A - B ) + B ) >. , <. 1 , ( ( C - D ) + D ) >. } )
12 zcn 
 |-  ( A e. ZZ -> A e. CC )
13 zcn 
 |-  ( B e. ZZ -> B e. CC )
14 npcan 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + B ) = A )
15 12 13 14 syl2an 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A - B ) + B ) = A )
16 15 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( A - B ) + B ) = A )
17 16 opeq2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> <. 0 , ( ( A - B ) + B ) >. = <. 0 , A >. )
18 zcn 
 |-  ( C e. ZZ -> C e. CC )
19 zcn 
 |-  ( D e. ZZ -> D e. CC )
20 npcan 
 |-  ( ( C e. CC /\ D e. CC ) -> ( ( C - D ) + D ) = C )
21 18 19 20 syl2an 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( ( C - D ) + D ) = C )
22 21 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( C - D ) + D ) = C )
23 22 opeq2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> <. 1 , ( ( C - D ) + D ) >. = <. 1 , C >. )
24 17 23 preq12d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , ( ( A - B ) + B ) >. , <. 1 , ( ( C - D ) + D ) >. } = { <. 0 , A >. , <. 1 , C >. } )
25 11 24 eqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } ( +g ` Z ) { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , A >. , <. 1 , C >. } )
26 1 zlmodzxzlmod 
 |-  ( Z e. LMod /\ ZZring = ( Scalar ` Z ) )
27 lmodgrp 
 |-  ( Z e. LMod -> Z e. Grp )
28 27 adantr 
 |-  ( ( Z e. LMod /\ ZZring = ( Scalar ` Z ) ) -> Z e. Grp )
29 26 28 mp1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> Z e. Grp )
30 1 zlmodzxzel 
 |-  ( ( A e. ZZ /\ C e. ZZ ) -> { <. 0 , A >. , <. 1 , C >. } e. ( Base ` Z ) )
31 30 ad2ant2r 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , A >. , <. 1 , C >. } e. ( Base ` Z ) )
32 1 zlmodzxzel 
 |-  ( ( B e. ZZ /\ D e. ZZ ) -> { <. 0 , B >. , <. 1 , D >. } e. ( Base ` Z ) )
33 4 7 32 syl2an 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , B >. , <. 1 , D >. } e. ( Base ` Z ) )
34 1 zlmodzxzel 
 |-  ( ( ( A - B ) e. ZZ /\ ( C - D ) e. ZZ ) -> { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } e. ( Base ` Z ) )
35 3 6 34 syl2an 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } e. ( Base ` Z ) )
36 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
37 36 9 2 grpsubadd 
 |-  ( ( Z e. Grp /\ ( { <. 0 , A >. , <. 1 , C >. } e. ( Base ` Z ) /\ { <. 0 , B >. , <. 1 , D >. } e. ( Base ` Z ) /\ { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } e. ( Base ` Z ) ) ) -> ( ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } <-> ( { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } ( +g ` Z ) { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , A >. , <. 1 , C >. } ) )
38 29 31 33 35 37 syl13anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } <-> ( { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } ( +g ` Z ) { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , A >. , <. 1 , C >. } ) )
39 25 38 mpbird 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } )