Step | Hyp | Ref
| Expression |
1 | | elncs 6119 |
. . . 4
⊢ (A ∈ NC ↔ ∃x A = Nc x) |
2 | | elncs 6119 |
. . . 4
⊢ (B ∈ NC ↔ ∃y B = Nc y) |
3 | | elncs 6119 |
. . . 4
⊢ (C ∈ NC ↔ ∃z C = Nc z) |
4 | 1, 2, 3 | 3anbi123i 1140 |
. . 3
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) ↔ (∃x A = Nc x ∧ ∃y B = Nc y ∧ ∃z C = Nc z)) |
5 | | eeeanv 1914 |
. . 3
⊢ (∃x∃y∃z(A = Nc x ∧ B = Nc y ∧ C = Nc z) ↔ (∃x A = Nc x ∧ ∃y B = Nc y ∧ ∃z C = Nc z)) |
6 | 4, 5 | bitr4i 243 |
. 2
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) ↔ ∃x∃y∃z(A = Nc x ∧ B = Nc y ∧ C = Nc z)) |
7 | | vex 2862 |
. . . . . . . 8
⊢ x ∈
V |
8 | | vex 2862 |
. . . . . . . 8
⊢ y ∈
V |
9 | | vex 2862 |
. . . . . . . 8
⊢ z ∈
V |
10 | 7, 8, 9 | xpassen 6057 |
. . . . . . 7
⊢ ((x × y)
× z) ≈ (x × (y
× z)) |
11 | 7, 8 | xpex 5115 |
. . . . . . . . 9
⊢ (x × y)
∈ V |
12 | 11, 9 | xpex 5115 |
. . . . . . . 8
⊢ ((x × y)
× z) ∈ V |
13 | 12 | eqnc 6127 |
. . . . . . 7
⊢ ( Nc ((x ×
y) × z) = Nc (x × (y
× z)) ↔ ((x × y)
× z) ≈ (x × (y
× z))) |
14 | 10, 13 | mpbir 200 |
. . . . . 6
⊢ Nc ((x ×
y) × z) = Nc (x × (y
× z)) |
15 | 7, 8 | mucnc 6131 |
. . . . . . . 8
⊢ ( Nc x
·c Nc y) = Nc (x × y) |
16 | 15 | oveq1i 5533 |
. . . . . . 7
⊢ (( Nc x
·c Nc y) ·c Nc z) = ( Nc (x ×
y) ·c Nc z) |
17 | 11, 9 | mucnc 6131 |
. . . . . . 7
⊢ ( Nc (x ×
y) ·c Nc z) = Nc ((x ×
y) × z) |
18 | 16, 17 | eqtri 2373 |
. . . . . 6
⊢ (( Nc x
·c Nc y) ·c Nc z) = Nc ((x ×
y) × z) |
19 | 8, 9 | mucnc 6131 |
. . . . . . . 8
⊢ ( Nc y
·c Nc z) = Nc (y × z) |
20 | 19 | oveq2i 5534 |
. . . . . . 7
⊢ ( Nc x
·c ( Nc y ·c Nc z)) = ( Nc x
·c Nc (y × z)) |
21 | 8, 9 | xpex 5115 |
. . . . . . . 8
⊢ (y × z)
∈ V |
22 | 7, 21 | mucnc 6131 |
. . . . . . 7
⊢ ( Nc x
·c Nc (y × z)) =
Nc (x ×
(y × z)) |
23 | 20, 22 | eqtri 2373 |
. . . . . 6
⊢ ( Nc x
·c ( Nc y ·c Nc z)) = Nc (x ×
(y × z)) |
24 | 14, 18, 23 | 3eqtr4i 2383 |
. . . . 5
⊢ (( Nc x
·c Nc y) ·c Nc z) = ( Nc x
·c ( Nc y ·c Nc z)) |
25 | | oveq12 5532 |
. . . . . . 7
⊢ ((A = Nc x ∧ B = Nc y) → (A
·c B) = ( Nc x
·c Nc y)) |
26 | | id 19 |
. . . . . . 7
⊢ (C = Nc z → C =
Nc z) |
27 | 25, 26 | oveqan12d 5541 |
. . . . . 6
⊢ (((A = Nc x ∧ B = Nc y) ∧ C = Nc z) → ((A
·c B)
·c C) = (( Nc x
·c Nc y) ·c Nc z)) |
28 | 27 | 3impa 1146 |
. . . . 5
⊢ ((A = Nc x ∧ B = Nc y ∧ C = Nc z) → ((A
·c B)
·c C) = (( Nc x
·c Nc y) ·c Nc z)) |
29 | | id 19 |
. . . . . . 7
⊢ (A = Nc x → A =
Nc x) |
30 | | oveq12 5532 |
. . . . . . 7
⊢ ((B = Nc y ∧ C = Nc z) → (B
·c C) = ( Nc y
·c Nc z)) |
31 | 29, 30 | oveqan12d 5541 |
. . . . . 6
⊢ ((A = Nc x ∧ (B = Nc y ∧ C = Nc z)) → (A
·c (B
·c C)) = ( Nc x
·c ( Nc y ·c Nc z))) |
32 | 31 | 3impb 1147 |
. . . . 5
⊢ ((A = Nc x ∧ B = Nc y ∧ C = Nc z) → (A
·c (B
·c C)) = ( Nc x
·c ( Nc y ·c Nc z))) |
33 | 24, 28, 32 | 3eqtr4a 2411 |
. . . 4
⊢ ((A = Nc x ∧ B = Nc y ∧ C = Nc z) → ((A
·c B)
·c C) = (A ·c (B ·c C))) |
34 | 33 | exlimiv 1634 |
. . 3
⊢ (∃z(A = Nc x ∧ B = Nc y ∧ C = Nc z) → ((A
·c B)
·c C) = (A ·c (B ·c C))) |
35 | 34 | exlimivv 1635 |
. 2
⊢ (∃x∃y∃z(A = Nc x ∧ B = Nc y ∧ C = Nc z) → ((A
·c B)
·c C) = (A ·c (B ·c C))) |
36 | 6, 35 | sylbi 187 |
1
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) → ((A
·c B)
·c C) = (A ·c (B ·c C))) |