Step | Hyp | Ref
| Expression |
1 | | elncs 6119 |
. . . . 5
⊢ (A ∈ NC ↔ ∃x A = Nc x) |
2 | | elncs 6119 |
. . . . 5
⊢ (B ∈ NC ↔ ∃y B = Nc y) |
3 | 1, 2 | anbi12i 678 |
. . . 4
⊢ ((A ∈ NC ∧ B ∈ NC ) ↔ (∃x A = Nc x ∧ ∃y B = Nc y)) |
4 | | eeanv 1913 |
. . . 4
⊢ (∃x∃y(A = Nc x ∧ B = Nc y) ↔ (∃x A = Nc x ∧ ∃y B = Nc y)) |
5 | 3, 4 | bitr4i 243 |
. . 3
⊢ ((A ∈ NC ∧ B ∈ NC ) ↔ ∃x∃y(A = Nc x ∧ B = Nc y)) |
6 | | vex 2862 |
. . . . . . . 8
⊢ x ∈
V |
7 | | vex 2862 |
. . . . . . . 8
⊢ y ∈
V |
8 | 6, 7 | mucnc 6131 |
. . . . . . 7
⊢ ( Nc x
·c Nc y) = Nc (x × y) |
9 | | df0c2 6137 |
. . . . . . 7
⊢
0c = Nc ∅ |
10 | 8, 9 | eqeq12i 2366 |
. . . . . 6
⊢ (( Nc x
·c Nc y) = 0c ↔ Nc (x ×
y) = Nc ∅) |
11 | 6, 7 | xpex 5115 |
. . . . . . . . 9
⊢ (x × y)
∈ V |
12 | 11 | eqnc 6127 |
. . . . . . . 8
⊢ ( Nc (x ×
y) = Nc ∅ ↔ (x
× y) ≈ ∅) |
13 | | en0 6042 |
. . . . . . . 8
⊢ ((x × y)
≈ ∅ ↔ (x × y) =
∅) |
14 | 12, 13 | bitri 240 |
. . . . . . 7
⊢ ( Nc (x ×
y) = Nc ∅ ↔ (x
× y) = ∅) |
15 | | xpeq0 5046 |
. . . . . . . 8
⊢ ((x × y) =
∅ ↔ (x = ∅ ∨ y = ∅)) |
16 | | nceq 6108 |
. . . . . . . . 9
⊢ (x = ∅ →
Nc x = Nc ∅) |
17 | | nceq 6108 |
. . . . . . . . 9
⊢ (y = ∅ →
Nc y = Nc ∅) |
18 | 16, 17 | orim12i 502 |
. . . . . . . 8
⊢ ((x = ∅ ∨ y = ∅) → ( Nc
x = Nc ∅ ∨ Nc y = Nc ∅)) |
19 | 15, 18 | sylbi 187 |
. . . . . . 7
⊢ ((x × y) =
∅ → ( Nc
x = Nc ∅ ∨ Nc y = Nc ∅)) |
20 | 14, 19 | sylbi 187 |
. . . . . 6
⊢ ( Nc (x ×
y) = Nc ∅ → ( Nc
x = Nc ∅ ∨ Nc y = Nc ∅)) |
21 | 10, 20 | sylbi 187 |
. . . . 5
⊢ (( Nc x
·c Nc y) = 0c → ( Nc x = Nc ∅ ∨ Nc y = Nc ∅)) |
22 | | oveq12 5532 |
. . . . . . 7
⊢ ((A = Nc x ∧ B = Nc y) → (A
·c B) = ( Nc x
·c Nc y)) |
23 | 22 | eqeq1d 2361 |
. . . . . 6
⊢ ((A = Nc x ∧ B = Nc y) → ((A
·c B) =
0c ↔ ( Nc x ·c Nc y) =
0c)) |
24 | | eqeq1 2359 |
. . . . . . . . 9
⊢ (A = Nc x → (A =
0c ↔ Nc x = 0c)) |
25 | 24 | adantr 451 |
. . . . . . . 8
⊢ ((A = Nc x ∧ B = Nc y) → (A =
0c ↔ Nc x = 0c)) |
26 | 9 | eqeq2i 2363 |
. . . . . . . 8
⊢ ( Nc x =
0c ↔ Nc x = Nc ∅) |
27 | 25, 26 | syl6bb 252 |
. . . . . . 7
⊢ ((A = Nc x ∧ B = Nc y) → (A =
0c ↔ Nc x = Nc ∅)) |
28 | | eqeq1 2359 |
. . . . . . . . 9
⊢ (B = Nc y → (B =
0c ↔ Nc y = 0c)) |
29 | 9 | eqeq2i 2363 |
. . . . . . . . 9
⊢ ( Nc y =
0c ↔ Nc y = Nc ∅) |
30 | 28, 29 | syl6bb 252 |
. . . . . . . 8
⊢ (B = Nc y → (B =
0c ↔ Nc y = Nc ∅)) |
31 | 30 | adantl 452 |
. . . . . . 7
⊢ ((A = Nc x ∧ B = Nc y) → (B =
0c ↔ Nc y = Nc ∅)) |
32 | 27, 31 | orbi12d 690 |
. . . . . 6
⊢ ((A = Nc x ∧ B = Nc y) → ((A =
0c ∨ B = 0c) ↔ ( Nc x = Nc ∅ ∨ Nc y = Nc ∅))) |
33 | 23, 32 | imbi12d 311 |
. . . . 5
⊢ ((A = Nc x ∧ B = Nc y) → (((A
·c B) =
0c → (A =
0c ∨ B = 0c)) ↔ (( Nc x
·c Nc y) = 0c → ( Nc x = Nc ∅ ∨ Nc y = Nc ∅)))) |
34 | 21, 33 | mpbiri 224 |
. . . 4
⊢ ((A = Nc x ∧ B = Nc y) → ((A
·c B) =
0c → (A =
0c ∨ B = 0c))) |
35 | 34 | exlimivv 1635 |
. . 3
⊢ (∃x∃y(A = Nc x ∧ B = Nc y) → ((A
·c B) =
0c → (A =
0c ∨ B = 0c))) |
36 | 5, 35 | sylbi 187 |
. 2
⊢ ((A ∈ NC ∧ B ∈ NC ) → ((A
·c B) =
0c → (A =
0c ∨ B = 0c))) |
37 | | 0cnc 6138 |
. . . . . . 7
⊢
0c ∈ NC |
38 | | muccom 6134 |
. . . . . . 7
⊢
((0c ∈ NC ∧ B ∈ NC ) → (0c
·c B) = (B ·c
0c)) |
39 | 37, 38 | mpan 651 |
. . . . . 6
⊢ (B ∈ NC → (0c
·c B) = (B ·c
0c)) |
40 | | muc0 6142 |
. . . . . 6
⊢ (B ∈ NC → (B
·c 0c) =
0c) |
41 | 39, 40 | eqtrd 2385 |
. . . . 5
⊢ (B ∈ NC → (0c
·c B) =
0c) |
42 | | oveq1 5530 |
. . . . . 6
⊢ (A = 0c → (A ·c B) = (0c
·c B)) |
43 | 42 | eqeq1d 2361 |
. . . . 5
⊢ (A = 0c → ((A ·c B) = 0c ↔
(0c ·c B) = 0c)) |
44 | 41, 43 | syl5ibrcom 213 |
. . . 4
⊢ (B ∈ NC → (A =
0c → (A
·c B) =
0c)) |
45 | 44 | adantl 452 |
. . 3
⊢ ((A ∈ NC ∧ B ∈ NC ) → (A =
0c → (A
·c B) =
0c)) |
46 | | muc0 6142 |
. . . . 5
⊢ (A ∈ NC → (A
·c 0c) =
0c) |
47 | | oveq2 5531 |
. . . . . 6
⊢ (B = 0c → (A ·c B) = (A
·c 0c)) |
48 | 47 | eqeq1d 2361 |
. . . . 5
⊢ (B = 0c → ((A ·c B) = 0c ↔ (A ·c 0c)
= 0c)) |
49 | 46, 48 | syl5ibrcom 213 |
. . . 4
⊢ (A ∈ NC → (B =
0c → (A
·c B) =
0c)) |
50 | 49 | adantr 451 |
. . 3
⊢ ((A ∈ NC ∧ B ∈ NC ) → (B =
0c → (A
·c B) =
0c)) |
51 | 45, 50 | jaod 369 |
. 2
⊢ ((A ∈ NC ∧ B ∈ NC ) → ((A =
0c ∨ B = 0c) → (A ·c B) = 0c)) |
52 | 36, 51 | impbid 183 |
1
⊢ ((A ∈ NC ∧ B ∈ NC ) → ((A
·c B) =
0c ↔ (A =
0c ∨ B = 0c))) |