Metamath Proof Explorer

Theorem axdistr

Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr be used later. Instead, use adddi . (Contributed by NM, 2-Sep-1995) (New usage is discouraged.)

Ref Expression
Assertion axdistr 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )

Proof

Step Hyp Ref Expression
1 dfcnqs 
 |-  CC = ( ( R. X. R. ) /. `' _E )
2 addcnsrec 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( [ <. z , w >. ] `' _E + [ <. v , u >. ] `' _E ) = [ <. ( z +R v ) , ( w +R u ) >. ] `' _E )
3 mulcnsrec 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) ) -> ( [ <. x , y >. ] `' _E x. [ <. ( z +R v ) , ( w +R u ) >. ] `' _E ) = [ <. ( ( x .R ( z +R v ) ) +R ( -1R .R ( y .R ( w +R u ) ) ) ) , ( ( y .R ( z +R v ) ) +R ( x .R ( w +R u ) ) ) >. ] `' _E )
4 mulcnsrec 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( [ <. x , y >. ] `' _E x. [ <. z , w >. ] `' _E ) = [ <. ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) , ( ( y .R z ) +R ( x .R w ) ) >. ] `' _E )
5 mulcnsrec 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( [ <. x , y >. ] `' _E x. [ <. v , u >. ] `' _E ) = [ <. ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) , ( ( y .R v ) +R ( x .R u ) ) >. ] `' _E )
6 addcnsrec 
 |-  ( ( ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. /\ ( ( y .R z ) +R ( x .R w ) ) e. R. ) /\ ( ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. /\ ( ( y .R v ) +R ( x .R u ) ) e. R. ) ) -> ( [ <. ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) , ( ( y .R z ) +R ( x .R w ) ) >. ] `' _E + [ <. ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) , ( ( y .R v ) +R ( x .R u ) ) >. ] `' _E ) = [ <. ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) +R ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) ) , ( ( ( y .R z ) +R ( x .R w ) ) +R ( ( y .R v ) +R ( x .R u ) ) ) >. ] `' _E )
7 addclsr 
 |-  ( ( z e. R. /\ v e. R. ) -> ( z +R v ) e. R. )
8 addclsr 
 |-  ( ( w e. R. /\ u e. R. ) -> ( w +R u ) e. R. )
9 7 8 anim12i 
 |-  ( ( ( z e. R. /\ v e. R. ) /\ ( w e. R. /\ u e. R. ) ) -> ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) )
10 9 an4s 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) )
11 mulclsr 
 |-  ( ( x e. R. /\ z e. R. ) -> ( x .R z ) e. R. )
12 m1r 
 |-  -1R e. R.
13 mulclsr 
 |-  ( ( y e. R. /\ w e. R. ) -> ( y .R w ) e. R. )
14 mulclsr 
 |-  ( ( -1R e. R. /\ ( y .R w ) e. R. ) -> ( -1R .R ( y .R w ) ) e. R. )
15 12 13 14 sylancr 
 |-  ( ( y e. R. /\ w e. R. ) -> ( -1R .R ( y .R w ) ) e. R. )
16 addclsr 
 |-  ( ( ( x .R z ) e. R. /\ ( -1R .R ( y .R w ) ) e. R. ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
17 11 15 16 syl2an 
 |-  ( ( ( x e. R. /\ z e. R. ) /\ ( y e. R. /\ w e. R. ) ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
18 17 an4s 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
19 mulclsr 
 |-  ( ( y e. R. /\ z e. R. ) -> ( y .R z ) e. R. )
20 mulclsr 
 |-  ( ( x e. R. /\ w e. R. ) -> ( x .R w ) e. R. )
21 addclsr 
 |-  ( ( ( y .R z ) e. R. /\ ( x .R w ) e. R. ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
22 19 20 21 syl2anr 
 |-  ( ( ( x e. R. /\ w e. R. ) /\ ( y e. R. /\ z e. R. ) ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
23 22 an42s 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
24 18 23 jca 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. /\ ( ( y .R z ) +R ( x .R w ) ) e. R. ) )
25 mulclsr 
 |-  ( ( x e. R. /\ v e. R. ) -> ( x .R v ) e. R. )
26 mulclsr 
 |-  ( ( y e. R. /\ u e. R. ) -> ( y .R u ) e. R. )
27 mulclsr 
 |-  ( ( -1R e. R. /\ ( y .R u ) e. R. ) -> ( -1R .R ( y .R u ) ) e. R. )
28 12 26 27 sylancr 
 |-  ( ( y e. R. /\ u e. R. ) -> ( -1R .R ( y .R u ) ) e. R. )
29 addclsr 
 |-  ( ( ( x .R v ) e. R. /\ ( -1R .R ( y .R u ) ) e. R. ) -> ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. )
30 25 28 29 syl2an 
 |-  ( ( ( x e. R. /\ v e. R. ) /\ ( y e. R. /\ u e. R. ) ) -> ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. )
31 30 an4s 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. )
32 mulclsr 
 |-  ( ( y e. R. /\ v e. R. ) -> ( y .R v ) e. R. )
33 mulclsr 
 |-  ( ( x e. R. /\ u e. R. ) -> ( x .R u ) e. R. )
34 addclsr 
 |-  ( ( ( y .R v ) e. R. /\ ( x .R u ) e. R. ) -> ( ( y .R v ) +R ( x .R u ) ) e. R. )
35 32 33 34 syl2anr 
 |-  ( ( ( x e. R. /\ u e. R. ) /\ ( y e. R. /\ v e. R. ) ) -> ( ( y .R v ) +R ( x .R u ) ) e. R. )
36 35 an42s 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( y .R v ) +R ( x .R u ) ) e. R. )
37 31 36 jca 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. /\ ( ( y .R v ) +R ( x .R u ) ) e. R. ) )
38 distrsr 
 |-  ( x .R ( z +R v ) ) = ( ( x .R z ) +R ( x .R v ) )
39 distrsr 
 |-  ( y .R ( w +R u ) ) = ( ( y .R w ) +R ( y .R u ) )
40 39 oveq2i 
 |-  ( -1R .R ( y .R ( w +R u ) ) ) = ( -1R .R ( ( y .R w ) +R ( y .R u ) ) )
41 distrsr 
 |-  ( -1R .R ( ( y .R w ) +R ( y .R u ) ) ) = ( ( -1R .R ( y .R w ) ) +R ( -1R .R ( y .R u ) ) )
42 40 41 eqtri 
 |-  ( -1R .R ( y .R ( w +R u ) ) ) = ( ( -1R .R ( y .R w ) ) +R ( -1R .R ( y .R u ) ) )
43 38 42 oveq12i 
 |-  ( ( x .R ( z +R v ) ) +R ( -1R .R ( y .R ( w +R u ) ) ) ) = ( ( ( x .R z ) +R ( x .R v ) ) +R ( ( -1R .R ( y .R w ) ) +R ( -1R .R ( y .R u ) ) ) )
44 ovex 
 |-  ( x .R z ) e. _V
45 ovex 
 |-  ( x .R v ) e. _V
46 ovex 
 |-  ( -1R .R ( y .R w ) ) e. _V
47 addcomsr 
 |-  ( f +R g ) = ( g +R f )
48 addasssr 
 |-  ( ( f +R g ) +R h ) = ( f +R ( g +R h ) )
49 ovex 
 |-  ( -1R .R ( y .R u ) ) e. _V
50 44 45 46 47 48 49 caov4 
 |-  ( ( ( x .R z ) +R ( x .R v ) ) +R ( ( -1R .R ( y .R w ) ) +R ( -1R .R ( y .R u ) ) ) ) = ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) +R ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) )
51 43 50 eqtri 
 |-  ( ( x .R ( z +R v ) ) +R ( -1R .R ( y .R ( w +R u ) ) ) ) = ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) +R ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) )
52 distrsr 
 |-  ( y .R ( z +R v ) ) = ( ( y .R z ) +R ( y .R v ) )
53 distrsr 
 |-  ( x .R ( w +R u ) ) = ( ( x .R w ) +R ( x .R u ) )
54 52 53 oveq12i 
 |-  ( ( y .R ( z +R v ) ) +R ( x .R ( w +R u ) ) ) = ( ( ( y .R z ) +R ( y .R v ) ) +R ( ( x .R w ) +R ( x .R u ) ) )
55 ovex 
 |-  ( y .R z ) e. _V
56 ovex 
 |-  ( y .R v ) e. _V
57 ovex 
 |-  ( x .R w ) e. _V
58 ovex 
 |-  ( x .R u ) e. _V
59 55 56 57 47 48 58 caov4 
 |-  ( ( ( y .R z ) +R ( y .R v ) ) +R ( ( x .R w ) +R ( x .R u ) ) ) = ( ( ( y .R z ) +R ( x .R w ) ) +R ( ( y .R v ) +R ( x .R u ) ) )
60 54 59 eqtri 
 |-  ( ( y .R ( z +R v ) ) +R ( x .R ( w +R u ) ) ) = ( ( ( y .R z ) +R ( x .R w ) ) +R ( ( y .R v ) +R ( x .R u ) ) )
61 1 2 3 4 5 6 10 24 37 51 60 ecovdi 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )