Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. . 3
β’ (π β (Scalarβπ) = (Scalarβπ)) |
2 | | eqidd 2734 |
. . 3
β’ (π β
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ))) |
3 | | lbsext.v |
. . . 4
β’ π = (Baseβπ) |
4 | 3 | a1i 11 |
. . 3
β’ (π β π = (Baseβπ)) |
5 | | eqidd 2734 |
. . 3
β’ (π β (+gβπ) = (+gβπ)) |
6 | | eqidd 2734 |
. . 3
β’ (π β (
Β·π βπ) = ( Β·π
βπ)) |
7 | | lbsext.p |
. . . 4
β’ π = (LSubSpβπ) |
8 | 7 | a1i 11 |
. . 3
β’ (π β π = (LSubSpβπ)) |
9 | | lbsext.t |
. . . 4
β’ π = βͺ π’ β π΄ (πβ(π’ β {π₯})) |
10 | | lbsext.w |
. . . . . . . 8
β’ (π β π β LVec) |
11 | | lveclmod 20611 |
. . . . . . . 8
β’ (π β LVec β π β LMod) |
12 | 10, 11 | syl 17 |
. . . . . . 7
β’ (π β π β LMod) |
13 | | lbsext.a |
. . . . . . . . . . 11
β’ (π β π΄ β π) |
14 | | lbsext.s |
. . . . . . . . . . . 12
β’ π = {π§ β π« π β£ (πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯})))} |
15 | 14 | ssrab3 4044 |
. . . . . . . . . . 11
β’ π β π« π |
16 | 13, 15 | sstrdi 3960 |
. . . . . . . . . 10
β’ (π β π΄ β π« π) |
17 | 16 | sselda 3948 |
. . . . . . . . 9
β’ ((π β§ π’ β π΄) β π’ β π« π) |
18 | 17 | elpwid 4573 |
. . . . . . . 8
β’ ((π β§ π’ β π΄) β π’ β π) |
19 | 18 | ssdifssd 4106 |
. . . . . . 7
β’ ((π β§ π’ β π΄) β (π’ β {π₯}) β π) |
20 | | lbsext.n |
. . . . . . . 8
β’ π = (LSpanβπ) |
21 | 3, 20 | lspssv 20488 |
. . . . . . 7
β’ ((π β LMod β§ (π’ β {π₯}) β π) β (πβ(π’ β {π₯})) β π) |
22 | 12, 19, 21 | syl2an2r 684 |
. . . . . 6
β’ ((π β§ π’ β π΄) β (πβ(π’ β {π₯})) β π) |
23 | 22 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ’ β π΄ (πβ(π’ β {π₯})) β π) |
24 | | iunss 5009 |
. . . . 5
β’ (βͺ π’ β π΄ (πβ(π’ β {π₯})) β π β βπ’ β π΄ (πβ(π’ β {π₯})) β π) |
25 | 23, 24 | sylibr 233 |
. . . 4
β’ (π β βͺ π’ β π΄ (πβ(π’ β {π₯})) β π) |
26 | 9, 25 | eqsstrid 3996 |
. . 3
β’ (π β π β π) |
27 | 9 | a1i 11 |
. . . 4
β’ (π β π = βͺ π’ β π΄ (πβ(π’ β {π₯}))) |
28 | | lbsext.z |
. . . . . 6
β’ (π β π΄ β β
) |
29 | 3, 7, 20 | lspcl 20481 |
. . . . . . . . 9
β’ ((π β LMod β§ (π’ β {π₯}) β π) β (πβ(π’ β {π₯})) β π) |
30 | 12, 19, 29 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ π’ β π΄) β (πβ(π’ β {π₯})) β π) |
31 | 7 | lssn0 20445 |
. . . . . . . 8
β’ ((πβ(π’ β {π₯})) β π β (πβ(π’ β {π₯})) β β
) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’ ((π β§ π’ β π΄) β (πβ(π’ β {π₯})) β β
) |
33 | 32 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ’ β π΄ (πβ(π’ β {π₯})) β β
) |
34 | | r19.2z 4456 |
. . . . . 6
β’ ((π΄ β β
β§
βπ’ β π΄ (πβ(π’ β {π₯})) β β
) β βπ’ β π΄ (πβ(π’ β {π₯})) β β
) |
35 | 28, 33, 34 | syl2anc 585 |
. . . . 5
β’ (π β βπ’ β π΄ (πβ(π’ β {π₯})) β β
) |
36 | | iunn0 5031 |
. . . . 5
β’
(βπ’ β
π΄ (πβ(π’ β {π₯})) β β
β βͺ π’ β π΄ (πβ(π’ β {π₯})) β β
) |
37 | 35, 36 | sylib 217 |
. . . 4
β’ (π β βͺ π’ β π΄ (πβ(π’ β {π₯})) β β
) |
38 | 27, 37 | eqnetrd 3008 |
. . 3
β’ (π β π β β
) |
39 | 9 | eleq2i 2826 |
. . . . . . . . 9
β’ (π£ β π β π£ β βͺ
π’ β π΄ (πβ(π’ β {π₯}))) |
40 | | eliun 4962 |
. . . . . . . . 9
β’ (π£ β βͺ π’ β π΄ (πβ(π’ β {π₯})) β βπ’ β π΄ π£ β (πβ(π’ β {π₯}))) |
41 | | difeq1 4079 |
. . . . . . . . . . . 12
β’ (π’ = π β (π’ β {π₯}) = (π β {π₯})) |
42 | 41 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π’ = π β (πβ(π’ β {π₯})) = (πβ(π β {π₯}))) |
43 | 42 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π’ = π β (π£ β (πβ(π’ β {π₯})) β π£ β (πβ(π β {π₯})))) |
44 | 43 | cbvrexvw 3225 |
. . . . . . . . 9
β’
(βπ’ β
π΄ π£ β (πβ(π’ β {π₯})) β βπ β π΄ π£ β (πβ(π β {π₯}))) |
45 | 39, 40, 44 | 3bitri 297 |
. . . . . . . 8
β’ (π£ β π β βπ β π΄ π£ β (πβ(π β {π₯}))) |
46 | 9 | eleq2i 2826 |
. . . . . . . . 9
β’ (π€ β π β π€ β βͺ
π’ β π΄ (πβ(π’ β {π₯}))) |
47 | | eliun 4962 |
. . . . . . . . 9
β’ (π€ β βͺ π’ β π΄ (πβ(π’ β {π₯})) β βπ’ β π΄ π€ β (πβ(π’ β {π₯}))) |
48 | | difeq1 4079 |
. . . . . . . . . . . 12
β’ (π’ = π β (π’ β {π₯}) = (π β {π₯})) |
49 | 48 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π’ = π β (πβ(π’ β {π₯})) = (πβ(π β {π₯}))) |
50 | 49 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π’ = π β (π€ β (πβ(π’ β {π₯})) β π€ β (πβ(π β {π₯})))) |
51 | 50 | cbvrexvw 3225 |
. . . . . . . . 9
β’
(βπ’ β
π΄ π€ β (πβ(π’ β {π₯})) β βπ β π΄ π€ β (πβ(π β {π₯}))) |
52 | 46, 47, 51 | 3bitri 297 |
. . . . . . . 8
β’ (π€ β π β βπ β π΄ π€ β (πβ(π β {π₯}))) |
53 | 45, 52 | anbi12i 628 |
. . . . . . 7
β’ ((π£ β π β§ π€ β π) β (βπ β π΄ π£ β (πβ(π β {π₯})) β§ βπ β π΄ π€ β (πβ(π β {π₯})))) |
54 | | reeanv 3216 |
. . . . . . 7
β’
(βπ β
π΄ βπ β π΄ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯}))) β (βπ β π΄ π£ β (πβ(π β {π₯})) β§ βπ β π΄ π€ β (πβ(π β {π₯})))) |
55 | 53, 54 | bitr4i 278 |
. . . . . 6
β’ ((π£ β π β§ π€ β π) β βπ β π΄ βπ β π΄ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) |
56 | | simp1l 1198 |
. . . . . . . . . . . 12
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β π) |
57 | | lbsext.r |
. . . . . . . . . . . 12
β’ (π β [β] Or π΄) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β [β] Or π΄) |
59 | | simp2 1138 |
. . . . . . . . . . 11
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (π β π΄ β§ π β π΄)) |
60 | | sorpssun 7671 |
. . . . . . . . . . 11
β’ ((
[β] Or π΄
β§ (π β π΄ β§ π β π΄)) β (π βͺ π) β π΄) |
61 | 58, 59, 60 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (π βͺ π) β π΄) |
62 | 56, 12 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β π β LMod) |
63 | | elssuni 4902 |
. . . . . . . . . . . . . . 15
β’ ((π βͺ π) β π΄ β (π βͺ π) β βͺ π΄) |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (π βͺ π) β βͺ π΄) |
65 | | sspwuni 5064 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β π« π β βͺ π΄
β π) |
66 | 16, 65 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β βͺ π΄
β π) |
67 | 56, 66 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β βͺ
π΄ β π) |
68 | 64, 67 | sstrd 3958 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (π βͺ π) β π) |
69 | 68 | ssdifssd 4106 |
. . . . . . . . . . . 12
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β ((π βͺ π) β {π₯}) β π) |
70 | 3, 7, 20 | lspcl 20481 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ ((π βͺ π) β {π₯}) β π) β (πβ((π βͺ π) β {π₯})) β π) |
71 | 62, 69, 70 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (πβ((π βͺ π) β {π₯})) β π) |
72 | | simp1r 1199 |
. . . . . . . . . . 11
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β π β (Baseβ(Scalarβπ))) |
73 | | ssun1 4136 |
. . . . . . . . . . . . . 14
β’ π β (π βͺ π) |
74 | | ssdif 4103 |
. . . . . . . . . . . . . 14
β’ (π β (π βͺ π) β (π β {π₯}) β ((π βͺ π) β {π₯})) |
75 | 73, 74 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (π β {π₯}) β ((π βͺ π) β {π₯})) |
76 | 3, 20 | lspss 20489 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ ((π βͺ π) β {π₯}) β π β§ (π β {π₯}) β ((π βͺ π) β {π₯})) β (πβ(π β {π₯})) β (πβ((π βͺ π) β {π₯}))) |
77 | 62, 69, 75, 76 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (πβ(π β {π₯})) β (πβ((π βͺ π) β {π₯}))) |
78 | | simp3l 1202 |
. . . . . . . . . . . 12
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β π£ β (πβ(π β {π₯}))) |
79 | 77, 78 | sseldd 3949 |
. . . . . . . . . . 11
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β π£ β (πβ((π βͺ π) β {π₯}))) |
80 | | ssun2 4137 |
. . . . . . . . . . . . . 14
β’ π β (π βͺ π) |
81 | | ssdif 4103 |
. . . . . . . . . . . . . 14
β’ (π β (π βͺ π) β (π β {π₯}) β ((π βͺ π) β {π₯})) |
82 | 80, 81 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (π β {π₯}) β ((π βͺ π) β {π₯})) |
83 | 3, 20 | lspss 20489 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ ((π βͺ π) β {π₯}) β π β§ (π β {π₯}) β ((π βͺ π) β {π₯})) β (πβ(π β {π₯})) β (πβ((π βͺ π) β {π₯}))) |
84 | 62, 69, 82, 83 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β (πβ(π β {π₯})) β (πβ((π βͺ π) β {π₯}))) |
85 | | simp3r 1203 |
. . . . . . . . . . . 12
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β π€ β (πβ(π β {π₯}))) |
86 | 84, 85 | sseldd 3949 |
. . . . . . . . . . 11
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β π€ β (πβ((π βͺ π) β {π₯}))) |
87 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Scalarβπ) =
(Scalarβπ) |
88 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
89 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(+gβπ) = (+gβπ) |
90 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (
Β·π βπ) = ( Β·π
βπ) |
91 | 87, 88, 89, 90, 7 | lsscl 20447 |
. . . . . . . . . . 11
β’ (((πβ((π βͺ π) β {π₯})) β π β§ (π β (Baseβ(Scalarβπ)) β§ π£ β (πβ((π βͺ π) β {π₯})) β§ π€ β (πβ((π βͺ π) β {π₯})))) β ((π( Β·π
βπ)π£)(+gβπ)π€) β (πβ((π βͺ π) β {π₯}))) |
92 | 71, 72, 79, 86, 91 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β ((π( Β·π
βπ)π£)(+gβπ)π€) β (πβ((π βͺ π) β {π₯}))) |
93 | | difeq1 4079 |
. . . . . . . . . . . 12
β’ (π’ = (π βͺ π) β (π’ β {π₯}) = ((π βͺ π) β {π₯})) |
94 | 93 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π’ = (π βͺ π) β (πβ(π’ β {π₯})) = (πβ((π βͺ π) β {π₯}))) |
95 | 94 | eliuni 4964 |
. . . . . . . . . 10
β’ (((π βͺ π) β π΄ β§ ((π( Β·π
βπ)π£)(+gβπ)π€) β (πβ((π βͺ π) β {π₯}))) β ((π( Β·π
βπ)π£)(+gβπ)π€) β βͺ
π’ β π΄ (πβ(π’ β {π₯}))) |
96 | 61, 92, 95 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β ((π( Β·π
βπ)π£)(+gβπ)π€) β βͺ
π’ β π΄ (πβ(π’ β {π₯}))) |
97 | 96, 9 | eleqtrrdi 2845 |
. . . . . . . 8
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄) β§ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯})))) β ((π( Β·π
βπ)π£)(+gβπ)π€) β π) |
98 | 97 | 3expia 1122 |
. . . . . . 7
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π β π΄ β§ π β π΄)) β ((π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯}))) β ((π( Β·π
βπ)π£)(+gβπ)π€) β π)) |
99 | 98 | rexlimdvva 3202 |
. . . . . 6
β’ ((π β§ π β (Baseβ(Scalarβπ))) β (βπ β π΄ βπ β π΄ (π£ β (πβ(π β {π₯})) β§ π€ β (πβ(π β {π₯}))) β ((π( Β·π
βπ)π£)(+gβπ)π€) β π)) |
100 | 55, 99 | biimtrid 241 |
. . . . 5
β’ ((π β§ π β (Baseβ(Scalarβπ))) β ((π£ β π β§ π€ β π) β ((π( Β·π
βπ)π£)(+gβπ)π€) β π)) |
101 | 100 | exp4b 432 |
. . . 4
β’ (π β (π β (Baseβ(Scalarβπ)) β (π£ β π β (π€ β π β ((π( Β·π
βπ)π£)(+gβπ)π€) β π)))) |
102 | 101 | 3imp2 1350 |
. . 3
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π£ β π β§ π€ β π)) β ((π( Β·π
βπ)π£)(+gβπ)π€) β π) |
103 | 1, 2, 4, 5, 6, 8, 26, 38, 102 | islssd 20440 |
. 2
β’ (π β π β π) |
104 | | eldifi 4090 |
. . . . . . 7
β’ (π¦ β (βͺ π΄
β {π₯}) β π¦ β βͺ π΄) |
105 | 104 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ β (βͺ π΄ β {π₯})) β π¦ β βͺ π΄) |
106 | | eldifn 4091 |
. . . . . . . . . 10
β’ (π¦ β (βͺ π΄
β {π₯}) β Β¬
π¦ β {π₯}) |
107 | 106 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π¦ β (βͺ π΄ β {π₯})) β§ π’ β π΄) β Β¬ π¦ β {π₯}) |
108 | | eldif 3924 |
. . . . . . . . . 10
β’ (π¦ β (π’ β {π₯}) β (π¦ β π’ β§ Β¬ π¦ β {π₯})) |
109 | 3, 20 | lspssid 20490 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ (π’ β {π₯}) β π) β (π’ β {π₯}) β (πβ(π’ β {π₯}))) |
110 | 12, 19, 109 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β π΄) β (π’ β {π₯}) β (πβ(π’ β {π₯}))) |
111 | 110 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (βͺ π΄ β {π₯})) β§ π’ β π΄) β (π’ β {π₯}) β (πβ(π’ β {π₯}))) |
112 | 111 | sseld 3947 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (βͺ π΄ β {π₯})) β§ π’ β π΄) β (π¦ β (π’ β {π₯}) β π¦ β (πβ(π’ β {π₯})))) |
113 | 108, 112 | biimtrrid 242 |
. . . . . . . . 9
β’ (((π β§ π¦ β (βͺ π΄ β {π₯})) β§ π’ β π΄) β ((π¦ β π’ β§ Β¬ π¦ β {π₯}) β π¦ β (πβ(π’ β {π₯})))) |
114 | 107, 113 | mpan2d 693 |
. . . . . . . 8
β’ (((π β§ π¦ β (βͺ π΄ β {π₯})) β§ π’ β π΄) β (π¦ β π’ β π¦ β (πβ(π’ β {π₯})))) |
115 | 114 | reximdva 3162 |
. . . . . . 7
β’ ((π β§ π¦ β (βͺ π΄ β {π₯})) β (βπ’ β π΄ π¦ β π’ β βπ’ β π΄ π¦ β (πβ(π’ β {π₯})))) |
116 | | eluni2 4873 |
. . . . . . 7
β’ (π¦ β βͺ π΄
β βπ’ β
π΄ π¦ β π’) |
117 | | eliun 4962 |
. . . . . . 7
β’ (π¦ β βͺ π’ β π΄ (πβ(π’ β {π₯})) β βπ’ β π΄ π¦ β (πβ(π’ β {π₯}))) |
118 | 115, 116,
117 | 3imtr4g 296 |
. . . . . 6
β’ ((π β§ π¦ β (βͺ π΄ β {π₯})) β (π¦ β βͺ π΄ β π¦ β βͺ
π’ β π΄ (πβ(π’ β {π₯})))) |
119 | 105, 118 | mpd 15 |
. . . . 5
β’ ((π β§ π¦ β (βͺ π΄ β {π₯})) β π¦ β βͺ
π’ β π΄ (πβ(π’ β {π₯}))) |
120 | 119 | ex 414 |
. . . 4
β’ (π β (π¦ β (βͺ π΄ β {π₯}) β π¦ β βͺ
π’ β π΄ (πβ(π’ β {π₯})))) |
121 | 120 | ssrdv 3954 |
. . 3
β’ (π β (βͺ π΄
β {π₯}) β
βͺ π’ β π΄ (πβ(π’ β {π₯}))) |
122 | 121, 9 | sseqtrrdi 3999 |
. 2
β’ (π β (βͺ π΄
β {π₯}) β π) |
123 | 103, 122 | jca 513 |
1
β’ (π β (π β π β§ (βͺ π΄ β {π₯}) β π)) |