Metamath Proof Explorer

Theorem zlmodzxzsubm

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

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

Proof

Step Hyp Ref Expression
1 zlmodzxz.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzsub.m 
 |-  .- = ( -g ` Z )
3 1 zlmodzxzlmod 
 |-  ( Z e. LMod /\ ZZring = ( Scalar ` Z ) )
4 3 simpli 
 |-  Z e. LMod
5 4 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> Z e. LMod )
6 1 zlmodzxzel 
 |-  ( ( A e. ZZ /\ C e. ZZ ) -> { <. 0 , A >. , <. 1 , C >. } e. ( Base ` Z ) )
7 6 ad2ant2r 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , A >. , <. 1 , C >. } e. ( Base ` Z ) )
8 1 zlmodzxzel 
 |-  ( ( B e. ZZ /\ D e. ZZ ) -> { <. 0 , B >. , <. 1 , D >. } e. ( Base ` Z ) )
9 8 ad2ant2l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , B >. , <. 1 , D >. } e. ( Base ` Z ) )
10 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
11 eqid 
 |-  ( +g ` Z ) = ( +g ` Z )
12 3 simpri 
 |-  ZZring = ( Scalar ` Z )
13 eqid 
 |-  ( .s ` Z ) = ( .s ` Z )
14 eqid 
 |-  ( invg ` ZZring ) = ( invg ` ZZring )
15 zring1 
 |-  1 = ( 1r ` ZZring )
16 10 11 2 12 13 14 15 lmodvsubval2 
 |-  ( ( Z e. LMod /\ { <. 0 , A >. , <. 1 , C >. } e. ( Base ` Z ) /\ { <. 0 , B >. , <. 1 , D >. } e. ( Base ` Z ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = ( { <. 0 , A >. , <. 1 , C >. } ( +g ` Z ) ( ( ( invg ` ZZring ) ` 1 ) ( .s ` Z ) { <. 0 , B >. , <. 1 , D >. } ) ) )
17 5 7 9 16 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = ( { <. 0 , A >. , <. 1 , C >. } ( +g ` Z ) ( ( ( invg ` ZZring ) ` 1 ) ( .s ` Z ) { <. 0 , B >. , <. 1 , D >. } ) ) )
18 1z 
 |-  1 e. ZZ
19 zringinvg 
 |-  ( 1 e. ZZ -> -u 1 = ( ( invg ` ZZring ) ` 1 ) )
20 18 19 mp1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> -u 1 = ( ( invg ` ZZring ) ` 1 ) )
21 20 eqcomd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( invg ` ZZring ) ` 1 ) = -u 1 )
22 21 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( ( invg ` ZZring ) ` 1 ) ( .s ` Z ) { <. 0 , B >. , <. 1 , D >. } ) = ( -u 1 ( .s ` Z ) { <. 0 , B >. , <. 1 , D >. } ) )
23 22 oveq2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } ( +g ` Z ) ( ( ( invg ` ZZring ) ` 1 ) ( .s ` Z ) { <. 0 , B >. , <. 1 , D >. } ) ) = ( { <. 0 , A >. , <. 1 , C >. } ( +g ` Z ) ( -u 1 ( .s ` Z ) { <. 0 , B >. , <. 1 , D >. } ) ) )
24 17 23 eqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = ( { <. 0 , A >. , <. 1 , C >. } ( +g ` Z ) ( -u 1 ( .s ` Z ) { <. 0 , B >. , <. 1 , D >. } ) ) )