Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π = 0) β π = 0) |
2 | 1 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π = 0) β (β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ) =
(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©β0)) |
3 | | lmat22.a |
. . . . . . . . 9
β’ (π β π΄ β π) |
4 | | lmat22.b |
. . . . . . . . 9
β’ (π β π΅ β π) |
5 | 3, 4 | s2cld 14766 |
. . . . . . . 8
β’ (π β β¨βπ΄π΅ββ© β Word π) |
6 | | s2fv0 14782 |
. . . . . . . 8
β’
(β¨βπ΄π΅ββ© β Word π β
(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©β0) =
β¨βπ΄π΅ββ©) |
7 | 5, 6 | syl 17 |
. . . . . . 7
β’ (π β
(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©β0) =
β¨βπ΄π΅ββ©) |
8 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ π = 0) β (β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©β0) =
β¨βπ΄π΅ββ©) |
9 | 2, 8 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π = 0) β (β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ) = β¨βπ΄π΅ββ©) |
10 | 9 | fveq2d 6847 |
. . . 4
β’ ((π β§ π = 0) β
(β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) =
(β―ββ¨βπ΄π΅ββ©)) |
11 | | s2len 14784 |
. . . 4
β’
(β―ββ¨βπ΄π΅ββ©) = 2 |
12 | 10, 11 | eqtrdi 2789 |
. . 3
β’ ((π β§ π = 0) β
(β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) = 2) |
13 | 12 | adantlr 714 |
. 2
β’ (((π β§ π β (0..^2)) β§ π = 0) β
(β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) = 2) |
14 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π = 1) β π = 1) |
15 | 14 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π = 1) β (β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ) =
(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©β1)) |
16 | | lmat22.c |
. . . . . . . . 9
β’ (π β πΆ β π) |
17 | | lmat22.d |
. . . . . . . . 9
β’ (π β π· β π) |
18 | 16, 17 | s2cld 14766 |
. . . . . . . 8
β’ (π β β¨βπΆπ·ββ© β Word π) |
19 | | s2fv1 14783 |
. . . . . . . 8
β’
(β¨βπΆπ·ββ© β Word π β
(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©β1) =
β¨βπΆπ·ββ©) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (π β
(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©β1) =
β¨βπΆπ·ββ©) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ π = 1) β (β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©β1) =
β¨βπΆπ·ββ©) |
22 | 15, 21 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π = 1) β (β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ) = β¨βπΆπ·ββ©) |
23 | 22 | fveq2d 6847 |
. . . 4
β’ ((π β§ π = 1) β
(β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) =
(β―ββ¨βπΆπ·ββ©)) |
24 | | s2len 14784 |
. . . 4
β’
(β―ββ¨βπΆπ·ββ©) = 2 |
25 | 23, 24 | eqtrdi 2789 |
. . 3
β’ ((π β§ π = 1) β
(β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) = 2) |
26 | 25 | adantlr 714 |
. 2
β’ (((π β§ π β (0..^2)) β§ π = 1) β
(β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) = 2) |
27 | | fzo0to2pr 13663 |
. . . . . 6
β’ (0..^2) =
{0, 1} |
28 | 27 | eleq2i 2826 |
. . . . 5
β’ (π β (0..^2) β π β {0, 1}) |
29 | | vex 3448 |
. . . . . 6
β’ π β V |
30 | 29 | elpr 4610 |
. . . . 5
β’ (π β {0, 1} β (π = 0 β¨ π = 1)) |
31 | 28, 30 | bitri 275 |
. . . 4
β’ (π β (0..^2) β (π = 0 β¨ π = 1)) |
32 | 31 | biimpi 215 |
. . 3
β’ (π β (0..^2) β (π = 0 β¨ π = 1)) |
33 | 32 | adantl 483 |
. 2
β’ ((π β§ π β (0..^2)) β (π = 0 β¨ π = 1)) |
34 | 13, 26, 33 | mpjaodan 958 |
1
β’ ((π β§ π β (0..^2)) β
(β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) = 2) |